  LastFn
|
|
Sigma KEE - and
|
antecedent
|
|
|
(=>
(and
(subclass ?X ?Y)
(instance ?Z ?X))
(instance ?Z ?Y)) |
Merge.kif 137-141 |
If X is a subclass of Y and Z is an instance of X, then Z is an instance of Y |
(=>
(and
(subrelation ?PRED1 ?PRED2)
(valence ?PRED1 ?NUMBER))
(valence ?PRED2 ?NUMBER)) |
Merge.kif 174-178 |
If X is a subrelation of Y and X has Z argument(s), then Y has Z argument(s) |
(=>
(and
(subrelation ?PRED1 ?PRED2)
(domain ?PRED2 ?NUMBER ?CLASS1))
(domain ?PRED1 ?NUMBER ?CLASS1)) |
Merge.kif 180-184 |
If X is a subrelation of Y and the number Z argument of Y is an instance of W, then the number Z argument of X is an instance of W |
(=>
(and
(subrelation ?REL1 ?REL2)
(instance ?REL1 Predicate)
(instance ?REL2 Predicate)
(?REL1 @ROW))
(?REL2 @ROW)) |
Merge.kif 186-192 |
If X is a subrelation of Y, X is an instance of predicate, Y is an instance of predicate, and X @ROW, then Y @ROW |
(=>
(and
(subrelation ?PRED1 ?PRED2)
(instance ?PRED2 ?CLASS)
(subclass ?CLASS InheritableRelation))
(instance ?PRED1 ?CLASS)) |
Merge.kif 194-199 |
If X is a subrelation of Y, Y is an instance of Z, and Z is a subclass of inheritable relation, then X is an instance of Z |
(=>
(and
(domain ?REL ?NUMBER ?CLASS1)
(domain ?REL ?NUMBER ?CLASS2))
(or
(subclass ?CLASS1 ?CLASS2)
(subclass ?CLASS2 ?CLASS1))) |
Merge.kif 215-221 |
If the number X argument of Y is an instance of Z and the number X argument of Y is an instance of W, then Z is a subclass of W or W is a subclass of Z |
(=>
(and
(subrelation ?REL1 ?REL2)
(domainSubclass ?REL2 ?NUMBER ?CLASS1))
(domainSubclass ?REL1 ?NUMBER ?CLASS1)) |
Merge.kif 232-236 |
If X is a subrelation of Y and the number Z argument of Y is a subclass of W, then the number Z argument of X is a subclass of W |
(=>
(and
(domainSubclass ?REL ?NUMBER ?CLASS1)
(domainSubclass ?REL ?NUMBER ?CLASS2))
(or
(subclass ?CLASS1 ?CLASS2)
(subclass ?CLASS2 ?CLASS1))) |
Merge.kif 238-244 |
If the number X argument of Y is a subclass of Z and the number X argument of Y is a subclass of W, then Z is a subclass of W or W is a subclass of Z |
(=>
(and
(equal ?LIST1 ?LIST2)
(equal ?LIST1
(ListFn @ROW1))
(equal ?LIST2
(ListFn @ROW2)))
(equal
(ListOrderFn
(ListFn @ROW1) ?NUMBER)
(ListOrderFn
(ListFn @ROW2) ?NUMBER))) |
Merge.kif 289-296 |
If equal X and Y, equal X and (@ROW1), and equal Y and (@ROW2), then equal V element of (@ROW1) and V element of (@ROW2) |
(=>
(and
(range ?FUNCTION ?CLASS)
(equal
(AssignmentFn ?FUNCTION @ROW) ?VALUE))
(instance ?VALUE ?CLASS)) |
Merge.kif 305-309 |
If the range of X is an instance of Y and equal X(@ROW) and W, then W is an instance of Y |
(=>
(and
(subrelation ?REL1 ?REL2)
(range ?REL2 ?CLASS1))
(range ?REL1 ?CLASS1)) |
Merge.kif 311-315 |
If X is a subrelation of Y and the range of Y is an instance of Z, then the range of X is an instance of Z |
(=>
(and
(range ?REL ?CLASS1)
(range ?REL ?CLASS2))
(or
(subclass ?CLASS1 ?CLASS2)
(subclass ?CLASS2 ?CLASS1))) |
Merge.kif 317-323 |
If the range of X is an instance of Y and the range of X is an instance of Z, then Y is a subclass of Z or Z is a subclass of Y |
(=>
(and
(rangeSubclass ?FUNCTION ?CLASS)
(equal
(AssignmentFn ?FUNCTION @ROW) ?VALUE))
(subclass ?VALUE ?CLASS)) |
Merge.kif 331-335 |
If the values returned by X are subclasses of Y and equal X(@ROW) and W, then W is a subclass of Y |
(=>
(and
(subrelation ?REL1 ?REL2)
(rangeSubclass ?REL2 ?CLASS1))
(rangeSubclass ?REL1 ?CLASS1)) |
Merge.kif 337-341 |
If X is a subrelation of Y and the values returned by Y are subclasses of Z, then the values returned by X are subclasses of Z |
(=>
(and
(rangeSubclass ?REL ?CLASS1)
(rangeSubclass ?REL ?CLASS2))
(or
(subclass ?CLASS1 ?CLASS2)
(subclass ?CLASS2 ?CLASS1))) |
Merge.kif 343-349 |
If the values returned by X are subclasses of Y and the values returned by X are subclasses of Z, then Y is a subclass of Z or Z is a subclass of Y |
(=>
(and
(domain ?REL1 ?NUMBER ?CLASS1)
(domain ?REL2 ?NUMBER ?CLASS2)
(disjoint ?CLASS1 ?CLASS2))
(disjointRelation ?REL1 ?REL2)) |
Merge.kif 411-416 |
If the number X argument of Y is an instance of Z, the number X argument of W is an instance of V, and Z is disjoint from V, then Y and W are disjoint |
(=>
(and
(domainSubclass ?REL1 ?NUMBER ?CLASS1)
(domainSubclass ?REL2 ?NUMBER ?CLASS2)
(disjoint ?CLASS1 ?CLASS2))
(disjointRelation ?REL1 ?REL2)) |
Merge.kif 418-423 |
If the number X argument of Y is a subclass of Z, the number X argument of W is a subclass of V, and Z is disjoint from V, then Y and W are disjoint |
(=>
(and
(range ?REL1 ?CLASS1)
(range ?REL2 ?CLASS2)
(disjoint ?CLASS1 ?CLASS2))
(disjointRelation ?REL1 ?REL2)) |
Merge.kif 425-430 |
If the range of X is an instance of Y, the range of Z is an instance of W, and Y is disjoint from W, then X and Z are disjoint |
(=>
(and
(rangeSubclass ?REL1 ?CLASS1)
(rangeSubclass ?REL2 ?CLASS2)
(disjoint ?CLASS1 ?CLASS2))
(disjointRelation ?REL1 ?REL2)) |
Merge.kif 432-437 |
If the values returned by X are subclasses of Y, the values returned by Z are subclasses of W, and Y is disjoint from W, then X and Z are disjoint |
(=>
(and
(instance ?REL1 Predicate)
(instance ?REL2 Predicate)
(disjointRelation ?REL1 ?REL2)
(?REL1 @ROW2))
(not
(?REL2 @ROW2))) |
Merge.kif 439-445 |
If X is an instance of predicate, Y is an instance of predicate, X and Y are disjoint, and X @ROW2, then Y @ROW2 |
(=>
(and
(contraryAttribute @ROW1)
(identicalListItems
(ListFn @ROW1)
(ListFn @ROW2)))
(contraryAttribute @ROW2)) |
Merge.kif 462-466 |
If @ROW1 is the opposite of and (@ROW2) is an identical list items of (@ROW1), then @ROW2 is the opposite of |
(=>
(and
(contraryAttribute @ROW)
(equal ?ATTR1
(ListOrderFn
(ListFn @ROW) ?NUMBER1))
(equal ?ATTR2
(ListOrderFn
(ListFn @ROW) ?NUMBER2))
(not
(equal ?NUMBER1 ?NUMBER2))
(property ?OBJ ?ATTR1))
(not
(property ?OBJ ?ATTR2))) |
Merge.kif 468-476 |
If @ROW is the opposite of, equal Y and Z element of (@ROW), equal W and V element of (@ROW), equal U and T, and S the attribute Y, then S does not have the attribute W |
(=>
(and
(exhaustiveAttribute ?CLASS @ROW)
(inList ?ATTR
(ListFn @ROW)))
(instance ?ATTR Attribute)) |
Merge.kif 489-493 |
If @ROW are all the attributes of Y and Z is a member of (@ROW), then Z is an instance of attribute |
(=>
(and
(exhaustiveAttribute ?CLASS @ROW)
(inList ?ATTR
(ListFn @ROW)))
(instance ?ATTR ?CLASS)) |
Merge.kif 495-499 |
If @ROW are all the attributes of Y and Z is a member of (@ROW), then Z is an instance of Y |
(=>
(and
(exhaustiveDecomposition @ROW)
(disjointDecomposition @ROW))
(partition @ROW)) |
Merge.kif 588-592 |
If @ROW is covered by @ROW and @ROW is disjointly decomposed into @ROW, then @ROW is exhaustively partitioned into @ROW |
| | Display limited to 25 items. Show next 25 |
| | Display limited to 25 items. Show next 25 |
|
consequent
|
|
|
(=>
(immediateInstance ?ENTITY ?CLASS)
(not
(exists (?SUBCLASS)
(and
(subclass ?SUBCLASS ?CLASS)
(not
(equal ?SUBCLASS ?CLASS))
(instance ?ENTITY ?SUBCLASS))))) |
Merge.kif 98-104 |
If X is an immediate instance of Y, then there doesn't exist Z such that Z is a subclass of Y, equal Z, Y, and X is an instance of Z |
(=>
(immediateSubclass ?CLASS1 ?CLASS2)
(not
(exists (?CLASS3)
(and
(subclass ?CLASS3 ?CLASS2)
(subclass ?CLASS1 ?CLASS3)
(not
(equal ?CLASS2 ?CLASS3))
(not
(equal ?CLASS1 ?CLASS3)))))) |
Merge.kif 154-161 |
If X is an immediate subclass of Y, then there doesn't exist Z such that Z is a subclass of Y, X is a subclass of Z, equal Y, Z, equal X, and Z |
(=>
(disjoint ?CLASS1 ?CLASS2)
(not
(exists (?INST)
(and
(instance ?INST ?CLASS1)
(instance ?INST ?CLASS2))))) |
Merge.kif 393-399 |
If X is disjoint from Y, then there doesn't exist Z such that Z is an instance of X and Z is an instance of Y |
(=>
(exhaustiveAttribute ?CLASS @ROW)
(forall (?ATTR1)
(=>
(instance ?ATTR1 ?CLASS)
(exists (?ATTR2)
(and
(inList ?ATTR2
(ListFn @ROW))
(equal ?ATTR1 ?ATTR2)))))) |
Merge.kif 501-509 |
If @ROW are all the attributes of Y, then For all Entity Z: if Z is an instance of Y, then there exists W such that W is a member of (@ROW) and equal Z and W |
(=>
(exhaustiveAttribute ?ATTRCLASS @ROW)
(not
(exists (?EL)
(and
(instance ?EL ?ATTRCLASS)
(not
(exists (?ATTR ?NUMBER)
(and
(equal ?EL ?ATTR)
(equal ?ATTR
(ListOrderFn
(ListFn @ROW) ?NUMBER))))))))) |
Merge.kif 511-523 |
If @ROW are all the attributes of Y, then there doesn't exist Z such that Z is an instance of Y and there don't exist W and V such that equal Z and W and equal W and U element of (@ROW) |
(=>
(partition @ROW)
(and
(exhaustiveDecomposition @ROW)
(disjointDecomposition @ROW))) |
Merge.kif 582-586 |
If @ROW is exhaustively partitioned into @ROW, then @ROW is covered by @ROW and @ROW is disjointly decomposed into @ROW |
(=>
(instance ?PHYS Physical)
(exists (?LOC ?TIME)
(and
(located ?PHYS ?LOC)
(time ?PHYS ?TIME)))) |
Merge.kif 831-836 |
If X is an instance of physical, then there exist Y, Z such that X is located at Y, and X exists during Z |
(=>
(properPart ?OBJ1 ?OBJ2)
(and
(part ?OBJ1 ?OBJ2)
(not
(part ?OBJ2 ?OBJ1)))) |
Merge.kif 944-949 |
If X is a proper part of Y, then X is a part of Y and Y is not a part of X |
(=>
(instance ?event VolcanicEruption)
(exists (?volcano)
(and
(instance ?volcano Volcano)
(agent ?event ?volcano)))) |
Merge.kif 1030-1035 |
If X is an instance of volcanic eruption, then there exists Y such that Y is an instance of volcano and Y is an agent of X |
(=>
(instance ?ERUPTING VolcanicEruption)
(exists (?VOLCANO)
(and
(instance ?VOLCANO Volcano)
(eventLocated ?ERUPTING ?VOLCANO)))) |
Merge.kif 1041-1046 |
If X is an instance of volcanic eruption, then there exists Y such that Y is an instance of volcano and X is located at Y |
(=>
(instance ?ERUPTING VolcanicEruption)
(exists (?HEATING)
(and
(instance ?HEATING Heating)
(subProcess ?HEATING ?ERUPTING)))) |
Merge.kif 1048-1053 |
If X is an instance of volcanic eruption, then there exists Y such that Y is an instance of heating and Y is a subprocess of X |
(=>
(instance ?C Crater)
(exists (?HOST ?EVENT ?METEOR ?BOMB)
(and
(hole ?C ?HOST)
(superficialPart ?SURF
(HoleHostFn ?C))
(or
(and
(instance ?EVENT Impacting)
(instrument ?EVENT ?METEOR)
(instance ?METEOR Meteorite))
(and
(instance ?EVENT Explosion)
(instrument ?EVENT ?BOMB)
(instance ?BOMB Bomb))
(instance ?EVENT VolcanicEruption))
(result ?EVENT ?C)))) |
Merge.kif 1059-1075 |
If X is an instance of crater, then All of the following hold: (1) there exist Y, Z,, , W (2) V such that X is a hole in Y (3) U is a superficial part of the host of the hole X (4) Z is an instance of impacting (5) W is an instrument for Z (6) W is an instance of meteorite or Z is an instance of explosion (7) V is an instrument for Z (8) V is an instance of bomb or Z is an instance of volcanic eruption (9) X is a result of Z |
(=>
(contains ?OBJ1 ?OBJ2)
(exists (?HOLE)
(and
(hole ?HOLE ?OBJ1)
(properlyFills ?OBJ2 ?HOLE)))) |
Merge.kif 1101-1106 |
If X contains Y, then there exists Z such that Z is a hole in X and Y properly fills Z |
(=>
(instance ?SUBSTANCE SyntheticSubstance)
(exists (?PROCESS)
(and
(instance ?PROCESS IntentionalProcess)
(result ?PROCESS ?SUBSTANCE)
(instance ?SUBSTANCE Substance)))) |
Merge.kif 1145-1151 |
If X is an instance of synthetic substance, then there exists Y such that Y is an instance of intentional process, X is a result of Y, and X is an instance of substance |
(=>
(instance ?ATOM Atom)
(exists (?PROTON ?ELECTRON)
(and
(part ?PROTON ?ATOM)
(part ?ELECTRON ?ATOM)
(instance ?PROTON Proton)
(instance ?ELECTRON Electron)))) |
Merge.kif 1186-1193 |
If X is an instance of atom, then there exist Y, Z such that Y is a part of X, Z is a part of X, Y is an instance of proton, and Z is an instance of electron |
(=>
(instance ?ATOM Atom)
(forall (?NUCLEUS1 ?NUCLEUS2)
(=>
(and
(part ?NUCLEUS1 ?ATOM)
(part ?NUCLEUS2 ?ATOM)
(instance ?NUCLEUS1 AtomicNucleus)
(instance ?NUCLEUS2 AtomicNucleus))
(equal ?NUCLEUS1 ?NUCLEUS2)))) |
Merge.kif 1195-1204 |
If X is an instance of atom, then For all Objects Y and Z: if Y is a part of X, Z is a part of X, Y is an instance of atomic nucleus, and Z is an instance of atomic nucleus, then equal Y and Z |
(=>
(instance ?PARTICLE SubatomicParticle)
(exists (?ATOM)
(and
(instance ?ATOM Atom)
(component ?PARTICLE ?ATOM)))) |
Merge.kif 1211-1216 |
If X is an instance of subatomic particle, then there exists Y such that Y is an instance of atom and X is a component of Y |
(=>
(instance ?NUCLEUS AtomicNucleus)
(exists (?NEUTRON ?PROTON)
(and
(component ?NEUTRON ?NUCLEUS)
(component ?PROTON ?NUCLEUS)
(instance ?NEUTRON Neutron)
(instance ?PROTON Proton)))) |
Merge.kif 1222-1229 |
If X is an instance of atomic nucleus, then there exist Y, Z such that Y is a component of X, Z is a component of X, Y is an instance of neutron, and Z is an instance of proton |
(=>
(instance ?MIXTURE Mixture)
(exists (?PURE1 ?PURE2)
(and
(instance ?PURE1 PureSubstance)
(instance ?PURE2 PureSubstance)
(not
(equal ?PURE1 ?PURE2))
(piece ?PURE1 ?MIXTURE)
(piece ?PURE2 ?MIXTURE)))) |
Merge.kif 1263-1271 |
If X is an instance of mixture, then All of the following hold: (1) there exist Y (2) Z such that Y is an instance of pure substance (3) Z is an instance of pure substance (4) equal Y (5) Z (6) Y is a piece of X (7) Z is a piece of X |
(=>
(ingredient ?ING ?S)
(exists (?PROC ?X ?Y)
(and
(instance ?PROC Process)
(instance ?X ?ING)
(patient ?PROC ?X)
(instance ?Y ?S)
(result ?PROC ?Y)))) |
Merge.kif 1289-1297 |
If X is an ingredient in Y, then there exist Z, W, V such that Z is an instance of process, W is an instance of X, W is a patient of Z, V is an instance of Y, and V is a result of Z |
(=>
(instance ?OBJ CorpuscularObject)
(exists (?SUBSTANCE1 ?SUBSTANCE2)
(and
(subclass ?SUBSTANCE1 Substance)
(subclass ?SUBSTANCE2 Substance)
(material ?SUBSTANCE1 ?OBJ)
(material ?SUBSTANCE2 ?OBJ)
(not
(equal ?SUBSTANCE1 ?SUBSTANCE2))))) |
Merge.kif 1304-1312 |
If X is an instance of corpuscular object, then All of the following hold: (1) there exist Y (2) Z such that Y is a subclass of substance (3) Z is a subclass of substance (4) X is made of Y (5) X is made of Z (6) equal Y (7) Z |
(=>
(instance ?STRING SymbolicString)
(exists (?PART)
(and
(part ?PART ?STRING)
(instance ?PART Character)))) |
Merge.kif 1437-1442 |
If X is an instance of symbolic string, then there exists Y such that Y is a part of X and Y is an instance of character |
(=>
(and
(instance ?LANG AnimalLanguage)
(agent ?PROC ?AGENT)
(instrument ?PROC ?LANG))
(and
(instance ?AGENT Animal)
(not
(instance ?AGENT Human)))) |
Merge.kif 1509-1516 |
If X is an instance of animal language, Y is an agent of Z, and X is an instrument for Z, then Y is an instance of animal and Y is not an instance of human |
(=>
(instance ?LANG ConstructedLanguage)
(exists (?PLAN)
(and
(instance ?PLAN Planning)
(result ?PLAN ?LANG)))) |
Merge.kif 1559-1564 |
If X is an instance of constructed language, then there exists Y such that Y is an instance of planning and X is a result of Y |
(=>
(instance ?W Writing)
(exists (?S ?L)
(and
(instance ?S Text)
(instance ?L WrittenHumanLanguage)
(language ?S ?L)))) |
Merge.kif 1603-1609 |
If X is an instance of writing, then there exist Y, Z such that Y is an instance of text, Z is an instance of written human language, and Z is a Language of Y. |
| | Display limited to 25 items. Show next 25 |
| | Display limited to 25 items. Show next 25 |
|
statement
|
|
|
(not
(exists (?PATH1 ?PATH2)
(and
(instance ?PATH1
(CutSetFn ?GRAPH))
(instance ?PATH2
(MinimalCutSetFn ?GRAPH))
(pathLength ?PATH1 ?NUMBER1)
(pathLength ?PATH2 ?NUMBER2)
(lessThan ?NUMBER1 ?NUMBER2)))) |
Merge.kif 6218-6225 |
There don't exist X, Y such that X is an instance of the set of paths that partition Z into two separate graphs, Y is an instance of the set of minimal paths that partition Z into two separate graphs, the length of X is W, the length of Y is V, and W is less than V |
(equal
(PopulationFn ?AREA)
(CardinalityFn
(KappaFn ?PERSON
(and
(instance ?PERSON Human)
(inhabits ?PERSON ?AREA))))) |
Mid-level-ontology.kif 34143-34148 |
equal the population of X and the number of instances in the class described by Y |
(equal
(OrganismPopulationFn ?O ?AREA)
(CardinalityFn
(KappaFn ?OI
(and
(instance ?OI ?O)
(located ?OI ?AREA))))) |
Mid-level-ontology.kif 34167-34172 |
equal individuals of type X in Y. and the number of instances in the class described by Z |
(exists (?T)
(and
(subclass ?T HandToolBox)
(manufacturer ?T SortimoCorp))) |
Cars.kif 5001-5004 |
There exists X such that X is a subclass of tool box and the maker of X is Sortimo Corporation |
(not
(and
(instance ?CURSOR MouseCursor)
(hasGUEState ?CURSOR GUE_ActiveState))) |
ComputerInput.kif 1968-1971 |
~{ X is an instance of mouse cursor } or ~{ X has state GUE active state } |
(not
(and
(hasGUEState ?WINDOW GUE_NonVisibleState)
(hasGUEState ?WINDOW GUE_ActiveState)
(instance ?WINDOW InterfaceWindow))) |
ComputerInput.kif 2027-2031 |
At least one of the following holds: (1) ~{ X has state GUE non visible state } (2) ~{ X has state GUE active state } (3) ~{ X is an instance of interface window } |
(not
(and
(instance ?CURSOR Cursor)
(hasGUEState ?CURSOR GUE_SelectedState))) |
ComputerInput.kif 2242-2245 |
~{ X is an instance of cursor } or ~{ X has state GUE selected state } |
(exists (?T)
(and
(instance ?T
(YearFn 2002))
(holdsDuring ?T
(coworker SteveJobsOfApple TimCookOfApple)))) |
ComputingBrands.kif 2441-2445 |
There exists X such that X is an instance of the year 2002 and Tim Cook is a coworker of Steve Jobs holds during X |
(exists (?T)
(and
(instance ?T
(YearFn 1976))
(holdsDuring ?T
(coworker SteveJobsOfApple SteveWozniakOfApple)))) |
ComputingBrands.kif 2453-2457 |
There exists X such that X is an instance of the year 1976 and Steve Wozniak is a coworker of Steve Jobs holds during X |
(hasPurpose IBookstore
(exists (?D)
(and
(instance ?D DownloadingOverNetwork)
(instrument ?D IBookstore)
(instance ?T Text)
(objectTransferred ?D ?T)))) |
ComputingBrands.kif 3216-3222 |
IBookstore has the purpose there exists ?D such that ?D is an instance of downloading, iBookstore is an instrument for ?D, ?T is an instance of text, and the object transferred in ?D is ?T |
(exists (?FORMULA)
(and
(instance ?FORMULA Formula)
(containsFormula ImmigrationAndNationalityAct_US ?FORMULA)
(modalAttribute ?FORMULA Law))) |
Government.kif 2372-2376 |
There exists X such that X is an instance of formula, immigration and nationality act_US contains the formula X, and the statement X has the modal force of law |
(exists (?FORMULA)
(and
(instance ?FORMULA Formula)
(containsFormula ImmigrationAndNationalityAct_Section219_US ?FORMULA)
(modalAttribute ?FORMULA Law))) |
Government.kif 2379-2383 |
There exists X such that X is an instance of formula, immigration and nationality act- section219-US contains the formula X, and the statement X has the modal force of law |
(exists (?FORMULA1 ?FORMULA2)
(and
(instance ?FORMULA1 Formula)
(containsFormula ImmigrationAndNationalityAct_US ?FORMULA1)
(instance ?FORMULA2 Formula)
(containsFormula ImmigrationAndNationalityAct_Section219_US ?FORMULA2)
(entails ?FORMULA1 ?FORMULA2))) |
Government.kif 2385-2391 |
There exist X, Y such that X is an instance of formula, immigration and nationality act_US contains the formula X, Y is an instance of formula, immigration and nationality act- section219-US contains the formula Y, and X entails Y |
(exists (?FORMULA)
(and
(instance ?FORMULA Formula)
(containsFormula AntiterrorismAndEffectiveDeathPenaltyAct ?FORMULA)
(modalAttribute ?FORMULA Law))) |
Government.kif 2395-2399 |
There exists X such that X is an instance of formula, antiterrorism and effective death penalty act contains the formula X, and the statement X has the modal force of law |
(holdsDuring
(ImmediateFutureFn ?TIME)
(and
(instance ?TIME
(YearFn 1996))
(conventionalLongName "Agency for the French_Speaking Community" AgencyForTheFrenchSpeakingCommunity))) |
Government.kif 2757-2761 |
X is an instance of the year 1996 and agency for the french speaking community is a conventional long name of "Agency for the French_Speaking Community" holds during immediately after X |
(holdsDuring
(ImmediateFutureFn ?T)
(and
(instance ?T
(DayFn 1
(MonthFn October
(YearFn 1992))))
(conventionalLongName "Andean Community of Nations" AndeanCommunityOfNations))) |
Government.kif 2783-2786 |
X is an instance of the day 1 of month the month October and andean community of nations is a conventional long name of "Andean Community of Nations" holds during immediately after X |
(exists (?TIME)
(and
(instance ?TIME TimeInterval)
(finishes ?TIME
(WhenFn JesusOfNazareth))
(starts ?TIME
(WhenFn TwelveApostles))
(forall (?MEM)
(=>
(holdsDuring ?TIME
(member ?MEM TwelveApostles))
(holdsDuring ?TIME
(friend ?MEM JesusOfNazareth)))))) |
Media.kif 1917-1925 |
There exists X such that X is an instance of timeframe, X finishes the time of existence of Jesus of Nazareth, X starts the time of existence of Twelve apostles, and Y Y is a member of Twelve apostles holds during XJesus of Nazareth is a friend of Y holds during X |
(holdsDuring
(FutureFn ?T)
(and
(instance Serbia IndependentState)
(instance ?T
(DayFn 5
(MonthFn June
(YearFn 2006)))))) |
Media.kif 2443-2446 |
Serbia is an instance of independent state and X is an instance of the day 5 of month the month June holds during after X |
(holdsDuring
(FutureFn ?T)
(and
(instance Serbia EuropeanNation)
(instance ?T
(DayFn 5
(MonthFn June
(YearFn 2006)))))) |
Media.kif 2448-2451 |
Serbia is an instance of european nation and X is an instance of the day 5 of month the month June holds during after X |
(holdsDuring
(FutureFn ?T)
(and
(names "Republic of Serbia" Serbia)
(instance ?T
(DayFn 5
(MonthFn June
(YearFn 2006)))))) |
Media.kif 2453-2456 |
Serbia has name "Republic of Serbia" and X is an instance of the day 5 of month the month June holds during after X |
(holdsDuring
(FutureFn ?TIME)
(and
(instance ?TIME
(DayFn 3
(MonthFn June
(YearFn 2006))))
(instance Montenegro IndependentState))) |
Media.kif 2470-2473 |
X is an instance of the day 3 of month the month June and Montenegro is an instance of independent state holds during after X |
(holdsDuring
(FutureFn ?TIME)
(and
(instance ?TIME
(DayFn 3
(MonthFn June
(YearFn 2006))))
(instance Montenegro EuropeanNation))) |
Media.kif 2475-2478 |
X is an instance of the day 3 of month the month June and Montenegro is an instance of european nation holds during after X |
(holdsDuring
(FutureFn ?TIME)
(and
(instance ?TIME
(DayFn 3
(MonthFn June
(YearFn 2006))))
(names "Montenegro" Montenegro))) |
Media.kif 2480-2483 |
X is an instance of the day 3 of month the month June and Montenegro has name "Montenegro" holds during after X |
(holdsDuring
(FutureFn ?TIME)
(and
(instance ?TIME
(DayFn 3
(MonthFn June
(YearFn 2006))))
(not
(instance SerbiaAndMontenegro IndependentState)))) |
Media.kif 2493-2497 |
X is an instance of the day 3 of month the month June and serbia and montenegro is not an instance of independent state holds during after X |
(exists (?FORMULA)
(and
(instance ?FORMULA Formula)
(containsFormula AmericansWithDisabilitiesAct_US ?FORMULA)
(modalAttribute ?FORMULA Law))) |
Medicine.kif 3176-3180 |
There exists X such that X is an instance of formula, ADA contains the formula X, and the statement X has the modal force of law |
| | Display limited to 25 items. Show next 25 |
| | Display limited to 25 items. Show next 25 |
|
