Browsing Interface : Welcome guest : log in
|
Browsing Interface : Welcome guest : log in |
[
Home |
Graph |
LogLearn |
Editor |
]
KB:
Language:
Formal Language:
|
| inhabits |
| appearance as argument number 1 |
|
| s__instance(s__inhabits,s__BinaryPredicate)
|
Merge.kif 14681-14681 | inhabits is an instance of binary predicate |
| s__domain(s__inhabits,n__1,s__Organism)
|
Merge.kif 14682-14682 | The number 1 argument of inhabits is an instance of organism |
| s__domain(s__inhabits,n__2,s__Object)
|
Merge.kif 14683-14683 | The number 2 argument of inhabits is an instance of object |
| s__documentation(s__inhabits, s__EnglishLanguage, "A very basic notion of living within something else_ (inhabits ?ORGANISM ?OBJECT) means that ?OBJECT is the residence (either permanent or temporary), nest, etc_ of ?ORGANISM_") | Merge.kif 14684-14686 | The number 2 argument of inhabits is an instance of object |
| appearance as argument number 2 |
|
|
| s__subrelation(s__home,s__inhabits)
|
Merge.kif 14696-14696 | home is a subrelation of inhabits |
| s__subrelation(s__stays,s__inhabits)
|
Merge.kif 14703-14703 | stays is a subrelation of inhabits |
| s__termFormat(s__EnglishLanguage, s__inhabits, "inhabits") | domainEnglishFormat.kif 30075-30075 | stays is a subrelation of inhabits |
| s__termFormat(s__ChineseTraditionalLanguage, s__inhabits, "棲息") | domainEnglishFormat.kif 30076-30076 | stays is a subrelation of inhabits |
| s__termFormat(s__ChineseLanguage, s__inhabits, "栖息") | domainEnglishFormat.kif 30077-30077 | stays is a subrelation of inhabits |
| s__format(s__EnglishLanguage, s__inhabits, "%1 %n{doesnt} live%p{s} in %2") | english_format.kif 526-526 | stays is a subrelation of inhabits |
| antecedent |
|
|
| ! [V__OBJ : $i,V__ORGANISM : $i,V__T1 : $i] : ((s__holdsDuring(V__T1, s__inhabits(V__ORGANISM, V__OBJ)) => ( ? [V__TIME:$i] : ((s__instance(V__TIME, s__TimeInterval) & s__temporalPart(V__TIME, V__T1) & s__holdsDuring(V__TIME, s__located(V__ORGANISM, V__OBJ))))))) | Merge.kif 14688-14694 | If X lives in Y holds during Z, then there exists W such that W is an instance of timeframe, W is a part of Z, and X is located at Y holds during W |
| ! [V__OBJ,V__FUNGUS] : ((s__instance(V__OBJ,s__Object) => ((s__instance(V__FUNGUS,s__Fungus) & s__inhabits(V__FUNGUS,V__OBJ)) => s__instance(V__OBJ,s__Organism))) )
|
Merge.kif 14743-14747 | If X is an instance of fungus and X lives in Y, then Y is an instance of organism |
| ! [V__OBJ,V__BACTERIUM] : ((s__instance(V__OBJ,s__Object) => ((s__instance(V__BACTERIUM,s__Bacterium) & s__inhabits(V__BACTERIUM,V__OBJ)) => s__instance(V__OBJ,s__Organism))) )
|
Merge.kif 14784-14788 | If X is an instance of bacterium and X lives in Y, then Y is an instance of organism |
| ! [V__OBJ,V__VIRUS] : ((s__instance(V__OBJ,s__Object) => ((s__instance(V__VIRUS,s__Virus) & s__inhabits(V__VIRUS,V__OBJ)) => s__instance(V__OBJ,s__Organism))) )
|
Merge.kif 14796-14800 | If X is an instance of virus and X lives in Y, then Y is an instance of organism |
| ! [V__I,V__L] : (((s__instance(V__I,s__Organism) & s__instance(V__L,s__Object)) => ((s__inhabits(V__I,V__L) => s__instance(V__I,s__Inhabitant)) & (s__instance(V__I,s__Inhabitant) => s__inhabits(V__I,V__L)))) )
|
Mid-level-ontology.kif 33059-33061 | X lives in Y if and only if X is an instance of inhabitant |
| ! [V__PERSON : $i,V__PLACE : $i,V__RESIDENCE : $i,V__T1 : $i] : (((s__holdsDuring(V__T1, (s__attribute(V__PERSON, s__DislocatedCivilian) & s__inhabits(V__PERSON, V__RESIDENCE) & s__located(V__RESIDENCE, V__PLACE))) & s__instance(V__PLACE, s__GeographicArea) & s__instance(V__T1, s__TimeInterval)) => ( ? [V__T0:$i, V__PRIOR_PLACE:$i, V__PRIOR_RES:$i] : ((s__instance(V__T0, s__TimeInterval) & s__earlier(V__T0, V__T1) & s__instance(V__PRIOR_RES, s__Object) & s__instance(V__PRIOR_PLACE, s__GeopoliticalArea) & s__located(V__PRIOR_RES, V__PRIOR_PLACE) & ~(V__PLACE = V__PRIOR_PLACE) & ~(V__RESIDENCE = V__PRIOR_RES) & ~(s__geographicSubregion(V__PLACE, V__PRIOR_PLACE)) & ~(s__geographicSubregion(V__PRIOR_PLACE, V__PLACE)) & s__holdsDuring(V__T0, s__inhabits(V__PERSON, V__PRIOR_RES))))))) | MilitaryPersons.kif 26-47 | If dislocated civilian is an attribute of X, X lives in Y, and Y is located at Z holds during W, Z is an instance of geographic area, and W is an instance of timeframe, then All of the following hold: (1) there exist V, ?PRIOR_PLACE (2) ?PRIOR_RES such that V is an instance of timeframe (3) V happens earlier than W (4) ?PRIOR_RES is an instance of object (5) ?PRIOR_PLACE is an instance of geopolitical area (6) ?PRIOR_RES is located at ?PRIOR_PLACE (7) equal Z (8) ?PRIOR_PLACE (9) equal Y (10) ?PRIOR_RES (11) Z is not a geographic subregion of ?PRIOR_PLACE (12) ?PRIOR_PLACE is not a geographic subregion of Z (13) X lives in ?PRIOR_RES holds during V |
| ! [V__NATION : $i,V__P : $i,V__PLACE : $i,V__RES : $i,V__T1 : $i] : ((s__holdsDuring(V__T1, (s__attribute(V__P, s__DisplacedPerson) & s__inhabits(V__P, V__RES) & s__located(V__RES, V__PLACE) & s__citizen(V__P, V__NATION))) => ~(s__partlyLocated(V__PLACE, V__NATION)))) | MilitaryPersons.kif 70-78 | If displaced person is an attribute of X, X lives in Y, Y is located at Z, and X is a citizen of W holds during V, then Z is not partly located in W |
| ! [V__NATION : $i,V__P : $i,V__PLACE : $i,V__RES : $i,V__T1 : $i] : ((s__holdsDuring(V__T1, (s__attribute(V__P, s__InternallyDisplacedPerson) & s__inhabits(V__P, V__RES) & s__located(V__RES, V__PLACE) & s__citizen(V__P, V__NATION))) => s__partlyLocated(V__PLACE, V__NATION))) | MilitaryPersons.kif 92-99 | If internally displaced person is an attribute of X, X lives in Y, Y is located at Z, and X is a citizen of W holds during V, then Z is partly located in W |
| consequent |
|
|
| ! [V__ALGA] : ((s__instance(V__ALGA,s__Alga) => (? [V__WATER] : ((s__inhabits(V__ALGA,V__WATER) & s__instance(V__WATER,s__Water))))) )
|
Merge.kif 14730-14735 | If X is an instance of alga, then there exists Y such that X lives in Y and Y is an instance of water |
| ! [V__FISH] : ((s__instance(V__FISH,s__Fish) => (? [V__WATER] : ((s__inhabits(V__FISH,V__WATER) & s__instance(V__WATER,s__Water))))) )
|
Merge.kif 14885-14890 | If X is an instance of fish, then there exists Y such that X lives in Y and Y is an instance of water |
| ! [V__BUILDING] : ((s__instance(V__BUILDING,s__Building) => (? [V__HUMAN] : ((s__instance(V__HUMAN,s__Human) & (s__inhabits(V__HUMAN,V__BUILDING) | (? [V__ACT] : ((s__instance(V__ACT,s__Process) & (s__agent(V__ACT,V__HUMAN) & s__located(V__ACT,V__BUILDING)))))))))) )
|
Merge.kif 16028-16038 | If X is an instance of building, then there exists Y such that Y is an instance of human, Y lives in X or there exists Z such that Y is an agent of Z, and Z is located at X |
| ! [V__O1,V__O2] : (((s__instance(V__O1,s__Organism) & s__instance(V__O2,s__Organism)) => (s__parasite(V__O1,V__O2) => s__inhabits(V__O1,V__O2))) )
|
Mid-level-ontology.kif 7399-7401 | If X is a parasite of Y, then Y lives in X |
| ! [V__R : $i] : ((s__instance(V__R, s__MobileResidence) => s__hasPurpose(V__R, ( ? [V__H:$i, V__T:$i] : ((s__instance(V__H, s__Human) & s__instance(V__T, s__Translocation) & s__inhabits(V__H, V__R) & s__patient(V__T, V__R))))))) | Mid-level-ontology.kif 7925-7933 | If X is an instance of mobile residence, then X has the purpose there exist Y, Z such that Y is an instance of human, Z is an instance of translocation, Y lives in X, and X is a patient of Z |
| ! [V__RESIDENCE : $i] : ((s__instance(V__RESIDENCE, s__AnimalResidence) => s__hasPurpose(V__RESIDENCE, ( ? [V__ANIMAL:$i] : ((s__instance(V__ANIMAL, s__Animal) & ~(s__instance(V__ANIMAL, s__Human)) & s__inhabits(V__ANIMAL, V__RESIDENCE))))))) | Mid-level-ontology.kif 8313-8320 | If X is an instance of animal residence, then X has the purpose there exists Y such that Y is an instance of animal, Y is not an instance of human, and Y lives in X |
| ! [V__A : $i,V__I : $i] : (((s__instance(V__I, s__Immigrating) & s__agent(V__I, V__A)) => ( ? [V__N1:$i, V__N2:$i] : ((s__instance(V__N1, s__Nation) & s__instance(V__N2, s__Nation) & s__origin(V__I, V__N1) & s__destination(V__I, V__N2) & ~(V__N1 = V__N2) & s__member(V__A, s__CitizenryFn(V__N1)) & ~(s__member(V__A, s__CitizenryFn(V__N2))) & s__hasPurpose(V__I, s__inhabits(V__A, V__N2))))))) | Mid-level-ontology.kif 19191-19207 | If X is an instance of immigrating and Y is an agent of X, then All of the following hold: (1) there exist Z (2) W such that Z is an instance of nation (3) W is an instance of nation (4) X originates at Z (5) X ends up at W (6) equal Z (7) W (8) Y is a member of the citizenry of Z (9) Y is not a member of the citizenry of W (10) X has the purpose Y lives in W |
| ! [V__AGENT : $i,V__DEVICE : $i,V__NUMBER : $i,V__PLACE : $i,V__TIME : $i] : (((s__instance(V__AGENT, s__Human) & s__holdsDuring(V__TIME, (s__deviceTelecomNumber(V__NUMBER, V__DEVICE) & s__telephoneNumber(V__NUMBER, V__AGENT) & s__located(V__DEVICE, V__PLACE) & s__instance(V__PLACE, s__Residence)))) => s__holdsDuring(V__TIME, s__inhabits(V__AGENT, V__PLACE)))) | Mid-level-ontology.kif 27317-27326 | If X is an instance of human and Y has number Z, Z is the telephone number of X, Y is located at W, and W is an instance of residence holds during V, then X lives in W holds during V |
| ! [V__U] : (((s__attribute(V__U,s__Uninhabited) & s__instance(V__U,s__Region)) => ~((? [V__H] : ((s__instance(V__H,s__Human) & s__inhabits(V__H,V__U)))))) )
|
Mid-level-ontology.kif 32712-32720 | If uninhabited is an attribute of X and X is an instance of region, then there doesn't exist Y such that Y is an instance of human and Y lives in X |
| ! [V__I] : (((s__attribute(V__I,s__Inhabited) & s__instance(V__I,s__Region)) => (? [V__H] : ((s__instance(V__H,s__Human) & s__inhabits(V__H,V__I))))) )
|
Mid-level-ontology.kif 32728-32735 | If inhabited is an attribute of X and X is an instance of region, then there exists Y such that Y is an instance of human and Y lives in X |
| ! [V__L : $i,V__O : $i] : ((s__habitatOfOrganism(V__O, V__L) => s__modalAttribute(( ? [V__OI:$i] : ((s__instance(V__OI, V__O) & s__inhabits(V__OI, V__L)))), s__Likely))) | Mid-level-ontology.kif 33034-33041 | If X inhabits Y, then the statement there exists Z such that Z is an instance of X and Z lives in Y has the modal force of likely |
| ! [V__I] : ((s__instance(V__I,s__Inhabitant) => (? [V__L] : ((s__instance(V__L,s__Object) & s__inhabits(V__I,V__L))))) )
|
Mid-level-ontology.kif 33052-33057 | If X is an instance of inhabitant, then there exists Y such that Y is an instance of object and X lives in Y |
| ! [V__P,V__N] : (((s__instance(V__P,s__Animal) & s__instance(V__N,s__GeographicArea)) => (s__instance(V__P,s__DemonymFn(V__N)) => ((? [V__R] : ((s__instance(V__R,s__Object) & (s__located(V__R,V__N) & s__inhabits(V__P,V__R))))) | s__birthplace(V__P,V__N)))) )
|
Mid-level-ontology.kif 33283-33290 | If X is an instance of Y-ian, then there exists Z such that Z is located at Y and X lives in Z or Y is a birthplace of X |
| ! [V__C,V__S] : (((s__instance(V__C,s__Class) & s__subclass(V__C,s__Meat)) => ((s__instance(V__S,V__C) & s__subclass(V__C,s__Seafood)) => (? [V__X,V__SEA,V__ANIMAL] : ((s__instance(V__X,s__Organism) & s__subclass(V__ANIMAL,s__Animal) & s__instance(V__ANIMAL,s__Class) & (s__meatOfAnimal(V__C,V__ANIMAL) & s__instance(V__X,V__ANIMAL) & s__instance(V__SEA,s__BodyOfWater) & s__inhabits(V__X,V__SEA))))))) )
|
Food.kif 1941-1950 | If X is an instance of Y and Y is a subclass of seafood, then there exist Z, W, V such that Y is the meat of V, Z is an instance of V, W is an instance of body of water, and Z lives in W |
| ! [V__B : $i] : ((s__instance(V__B, s__Burrow) => ( ? [V__A:$i] : (s__hasPurpose(V__B, s__inhabits(V__A, V__B)))))) | Geography.kif 7642-7646 | If X is an instance of burrow, then there exists Y such that X has the purpose Y lives in X |
| ! [V__A : $i] : ((s__instance(V__A, s__Attic) => s__hasPurpose(V__A, ~(( ? [V__P:$i] : (s__inhabits(V__P, V__A))))))) | HouseholdAppliances.kif 1127-1132 | If X is an instance of attic, then X has the purpose there doesn't exist Y such that Y lives in X |
| ! [V__PERSON : $i,V__PLACE : $i,V__RESIDENCE : $i,V__T1 : $i] : (((s__holdsDuring(V__T1, (s__attribute(V__PERSON, s__DislocatedCivilian) & s__inhabits(V__PERSON, V__RESIDENCE) & s__located(V__RESIDENCE, V__PLACE))) & s__instance(V__PLACE, s__GeographicArea) & s__instance(V__T1, s__TimeInterval)) => ( ? [V__T0:$i, V__PRIOR_PLACE:$i, V__PRIOR_RES:$i] : ((s__instance(V__T0, s__TimeInterval) & s__earlier(V__T0, V__T1) & s__instance(V__PRIOR_RES, s__Object) & s__instance(V__PRIOR_PLACE, s__GeopoliticalArea) & s__located(V__PRIOR_RES, V__PRIOR_PLACE) & ~(V__PLACE = V__PRIOR_PLACE) & ~(V__RESIDENCE = V__PRIOR_RES) & ~(s__geographicSubregion(V__PLACE, V__PRIOR_PLACE)) & ~(s__geographicSubregion(V__PRIOR_PLACE, V__PLACE)) & s__holdsDuring(V__T0, s__inhabits(V__PERSON, V__PRIOR_RES))))))) | MilitaryPersons.kif 26-47 | If dislocated civilian is an attribute of X, X lives in Y, and Y is located at Z holds during W, Z is an instance of geographic area, and W is an instance of timeframe, then All of the following hold: (1) there exist V, ?PRIOR_PLACE (2) ?PRIOR_RES such that V is an instance of timeframe (3) V happens earlier than W (4) ?PRIOR_RES is an instance of object (5) ?PRIOR_PLACE is an instance of geopolitical area (6) ?PRIOR_RES is located at ?PRIOR_PLACE (7) equal Z (8) ?PRIOR_PLACE (9) equal Y (10) ?PRIOR_RES (11) Z is not a geographic subregion of ?PRIOR_PLACE (12) ?PRIOR_PLACE is not a geographic subregion of Z (13) X lives in ?PRIOR_RES holds during V |
| ! [V__B] : ((s__instance(V__B,s__MilitaryBase) => (? [V__H] : ((s__instance(V__H,s__Human) & s__attribute(V__H,s__MilitaryPerson) & s__inhabits(V__H,V__B))))) )
|
MilitaryProcesses.kif 2799-2805 | If X is an instance of military base, then there exists Y such that Y is an instance of human, military person is an attribute of Y, and Y lives in X |
| ! [V__AREA : $i,V__EMMIGRATION : $int,V__IMMIGRATION : $int,V__MIGRATIONCOUNT : $real,V__PERSON : $i,V__POPULATION : $int,V__PREVIOUSYEAR : $i,V__PY : $int,V__REALNUMBER : $real,V__THOUSANDS : $real,V__Y : $int,V__YEAR : $i] : (((s__instance(V__YEAR, s__YearFn(V__Y)) & s__MigrantsPerThousandFn(V__AREA, V__YEAR) = V__REALNUMBER) => ($difference(V__Y ,V__PY) = 1 & s__instance(V__PREVIOUSYEAR, s__YearFn(V__PY)) & s__holdsDuring(V__YEAR, s__PopulationFn(V__AREA) = V__POPULATION) & s__DivisionFn(V__POPULATION, 1000) = V__THOUSANDS & V__IMMIGRATION = s__CardinalityFn(s__KappaFn(V__PERSON, (s__instance(V__PERSON, s__Human) & s__holdsDuring(V__PREVIOUSYEAR, ~(s__inhabits(V__PERSON, V__AREA))) & s__holdsDuring(V__YEAR, s__inhabits(V__PERSON, V__AREA))))) & V__EMMIGRATION = s__CardinalityFn(s__KappaFn(V__PERSON, (s__instance(V__PERSON, s__Human) & s__holdsDuring(V__PREVIOUSYEAR, s__inhabits(V__PERSON, V__AREA)) & s__holdsDuring(V__YEAR, ~(s__inhabits(V__PERSON, V__AREA)))))) & $difference(V__IMMIGRATION ,V__EMMIGRATION) = V__MIGRATIONCOUNT & s__DivisionFn(V__MIGRATIONCOUNT, V__THOUSANDS) = V__REALNUMBER))) | People.kif 190-221 | If X is an instance of the year Y and equal the migrants per thousand of Z, X, and W, then All of the following hold: (1) equal (Y and V) and 1 (2) U is an instance of the year V (3) equal the population of Z and T holds during X (4) equal T, 1000, and S (5) equal R and the number of instances in the class described by Q (6) equal P and the number of instances in the class described by Q (7) equal (R and P) and O (8) equal O, S, and W |
| ! [V__AREA : $i,V__FEMALE : $i,V__FEMALECOUNT : $int,V__MALE : $i,V__MALECOUNT : $int,V__REALNUMBER : $real] : ((s__MaleToFemaleRatioFn(V__AREA) = V__REALNUMBER => (V__MALECOUNT = s__CardinalityFn(s__KappaFn(V__MALE, (s__instance(V__MALE, s__Human) & s__attribute(V__MALE, s__Male) & s__inhabits(V__MALE, V__AREA)))) & V__FEMALECOUNT = s__CardinalityFn(s__KappaFn(V__FEMALE, (s__instance(V__FEMALE, s__Human) & s__attribute(V__FEMALE, s__Female) & s__inhabits(V__FEMALE, V__AREA)))) & s__DivisionFn(V__MALECOUNT, V__FEMALECOUNT) = V__REALNUMBER))) | People.kif 240-257 | If equal the male to female ratio of X and Y, then equal Z and the number of instances in the class described by W, equal V and the number of instances in the class described by U, and equal Z, V, and Y |
| statement |
|
|
| ! [V__AREA : $i,V__PERSON : $i] : (s__PopulationFn(V__AREA) = s__CardinalityFn(s__KappaFn(V__PERSON, (s__instance(V__PERSON, s__Human) & s__inhabits(V__PERSON, V__AREA))))) | Mid-level-ontology.kif 34143-34148 | equal the population of X and the number of instances in the class described by Y |
| ! [V__AGE : $i,V__AREA : $i,V__MILITARYAGE : $i,V__PERSON : $i] : (s__AvailableForMilitaryServiceMaleFn(V__AREA) = s__CardinalityFn(s__KappaFn(V__PERSON, (s__instance(V__PERSON, s__Human) & s__attribute(V__PERSON, s__Male) & s__militaryAge(V__AREA, V__MILITARYAGE) & s__age(V__PERSON, V__AGE) & ($greatereq(V__AGE,V__MILITARYAGE)) & s__inhabits(V__PERSON, V__AREA))))) | Military.kif 1136-1145 | equal the available for military service male of X and the number of instances in the class described by Y |
| ! [V__AGE : $i,V__AREA : $i,V__MILITARYAGE : $i,V__PERSON : $i,V__PROCESS : $i] : (s__FitForMilitaryServiceMaleFn(V__AREA) = s__CardinalityFn(s__KappaFn(V__PERSON, (s__instance(V__PERSON, s__Human) & s__attribute(V__PERSON, s__Male) & s__subclass(V__PROCESS, s__MilitaryProcess) & s__fitForMilitaryService(V__PERSON, V__PROCESS) & s__militaryAge(V__AREA, V__MILITARYAGE) & s__age(V__PERSON, V__AGE) & ($greatereq(V__AGE,V__MILITARYAGE)) & s__inhabits(V__PERSON, V__AREA))))) | Military.kif 1159-1170 | equal the fit for military service male of X and the number of instances in the class described by Y |
| ! [V__AGE : $i,V__AGEMINUSONE : $i,V__AREA : $i,V__MILITARYAGE : $i,V__PERSON : $i,V__YEAR : $i] : (s__ReachingMilitaryAgeAnnuallyMaleFn(V__AREA, V__YEAR) = s__CardinalityFn(s__KappaFn(V__PERSON, (s__instance(V__PERSON, s__Human) & s__attribute(V__PERSON, s__Male) & s__militaryAge(V__AREA, V__MILITARYAGE) & V__AGEMINUSONE = $difference(V__AGE ,1) & s__holdsDuring(V__YEAR, (s__age(V__PERSON, V__AGEMINUSONE) | s__age(V__PERSON, V__AGE))) & V__AGE = V__MILITARYAGE & s__inhabits(V__PERSON, V__AREA))))) | Military.kif 1197-1210 | equal the reaching military age annually male of X, Y, and the number of instances in the class described by Z |
| ! [V__AREA : $i,V__BIRTH : $i,V__INFANT : $i,V__WOMAN : $i,V__Y : $int,V__YEAR : $i] : ((s__instance(V__YEAR, s__YearFn(V__Y)) & s__ChildrenBornPerWomanFn(V__AREA, V__YEAR) = s__CardinalityFn(s__KappaFn(V__INFANT, (s__instance(V__BIRTH, s__Birth) & s__experiencer(V__BIRTH, V__INFANT) & s__agent(V__BIRTH, V__WOMAN) & s__instance(V__WOMAN, s__Human) & s__attribute(V__WOMAN, s__Female) & s__holdsDuring(V__YEAR, s__inhabits(V__WOMAN, V__AREA))))))) | People.kif 490-503 | X is an instance of the year Y and equal the children born per woman of Z, X, and the number of instances in the class described by W |
|