Browsing Interface : Welcome guest : log in 		[  Home |  Graph |  LogLearn |  Editor |  ]  KB:  Language: 
  Formal Language: 


KB Term:  Term intersection
English Word: 

Sigma KEE - and
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

appearance as argument number 0
-------------------------


(and
    (instance ?YEAR
        (YearFn ?Y))
    (equal
        (ChildrenBornPerWomanFn ?AREA ?YEAR)
        (CardinalityFn
            (KappaFn ?INFANT
                (and
                    (instance ?BIRTH Birth)
                    (experiencer ?BIRTH ?INFANT)
                    (agent ?BIRTH ?WOMAN)
                    (instance ?WOMAN Human)
                    (attribute ?WOMAN Female)
                    (holdsDuring ?YEAR
                        (inhabits ?WOMAN ?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


Show full definition with tree view
Show simplified definition (without tree view)
Show simplified definition (with tree view)


Sigma web home      Suggested Upper Merged Ontology (SUMO) web home
Sigma version 3.0.0-0a80e6c8 (2026-05-12) is open source software produced by Articulate Software and its partners