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


KB Term:  Term intersection
English Word: 

  Function

 Sigma KEE - instance
instance

appearance as argument number 1
-------------------------


(instance instance BinaryPredicate) Merge.kif 80-80 instance is an instance of binary predicate
(domain instance 1 Entity) Merge.kif 81-81 The number 1 argument of instance is an instance of entity
(domain instance 2 Class) Merge.kif 82-82 The number 2 argument of instance is an instance of class
(documentation instance EnglishLanguage "An object is an instance of a Class if it is included in that Class. An individual may be an instance of many classes, some of which may be subclasses of others. Thus, there is no assumption in the meaning of instance about specificity or uniqueness.") Merge.kif 84-87 The number 2 argument of instance is an instance of class

appearance as argument number 2
-------------------------


(subrelation immediateInstance instance) Merge.kif 89-89 immediate instance is a subrelation of instance
(relatedInternalConcept member instance) Merge.kif 1355-1355 member is internally related to instance
(termFormat EnglishLanguage instance "instance") domainEnglishFormat.kif 30249-30249 member is internally related to instance
(termFormat ChineseTraditionalLanguage instance "例") domainEnglishFormat.kif 30250-30250 member is internally related to instance
(termFormat ChineseLanguage instance "例") domainEnglishFormat.kif 30251-30251 member is internally related to instance
(format EnglishLanguage instance "%1 is %n an instance of %2") english_format.kif 310-310 member is internally related to instance

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 ?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
        (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
        (partition ?SUPER ?SUB1 ?SUB2)
        (instance ?INST ?SUPER)
        (not
            (instance ?INST ?SUB1)))
    (instance ?INST ?SUB2))		 Merge.kif 598-604 If X is exhaustively partitioned into Y and Z, W is an instance of X, and W is not an instance of Y, then W is an instance of Z
(=>
    (and
        (subAttribute ?ATTR1 ?ATTR2)
        (instance ?ATTR2 ?CLASS))
    (instance ?ATTR1 ?CLASS))		 Merge.kif 688-692 If X is a subattribute of Y and Y is an instance of Z, then X is an instance of Z
(=>
    (instance ?CLASS Class)
    (subclass ?CLASS Entity))		 Merge.kif 820-822 If X is an instance of class, then X is a subclass of entity
(=>
    (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
(=>
    (instance ?O Object)
    (capability Translocation origin ?O))		 Merge.kif 846-848 If X is an instance of object, then X is capable of doing translocation as a origin
(=>
    (instance ?O Object)
    (capability Translocation destination ?O))		 Merge.kif 850-852 If X is an instance of object, then X is capable of doing translocation as a destination
(=>
    (instance ?OBJ SelfConnectedObject)
    (side
        (FrontFn ?OBJ) ?OBJ))		 Merge.kif 883-885 If X is an instance of self connected object, then a side of X is the front of X
(=>
    (instance ?OBJ SelfConnectedObject)
    (side
        (BackFn ?OBJ) ?OBJ))		 Merge.kif 903-905 If X is an instance of self connected object, then a side of X is the back 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
(=>
    (and
        (subclass ?OBJECTTYPE Substance)
        (instance ?OBJECT ?OBJECTTYPE)
        (piece ?PART ?OBJECT))
    (instance ?PART ?OBJECTTYPE))		 Merge.kif 1126-1131 If X is a subclass of substance, Y is an instance of X, and Z is a piece of Y, then Z is an instance of X
(=>
    (and
        (instance ?OBJ Substance)
        (attribute ?OBJ ?ATTR)
        (piece ?PART ?OBJ))
    (attribute ?PART ?ATTR))		 Merge.kif 1133-1138 If X is an instance of substance, Y is an attribute of X, and Z is a piece of X, then Y is an attribute of 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
(=>
    (and
        (instance ?MIXTURE Mixture)
        (piece ?SUBSTANCE ?MIXTURE)
        (not
            (instance ?SUBSTANCE Mixture)))
    (instance ?SUBSTANCE PureSubstance))		 Merge.kif 1273-1278 If X is an instance of mixture, Y is a piece of X, and Y is not an instance of mixture, then Y is an instance of pure substance

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
(=>
    (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)
        (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
(=>
    (equal ?THING1 ?THING2)
    (forall (?CLASS)
        (<=>
            (instance ?THING1 ?CLASS)
            (instance ?THING2 ?CLASS))))		 Merge.kif 268-273 If equal X and Y, then For all Class Z: X is an instance of Z if and only if Y is an instance of Z
(=>
    (equal ?CLASS1 ?CLASS2)
    (forall (?THING)
        (<=>
            (instance ?THING ?CLASS1)
            (instance ?THING ?CLASS2))))		 Merge.kif 275-280 If equal X and Y, then For all Entity Z: Z is an instance of X if and only if Z is an instance of Y
(=>
    (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
(=>
    (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
(=>
    (contraryAttribute @ROW)
    (=>
        (inList ?ELEMENT
            (ListFn @ROW))
        (instance ?ELEMENT Attribute)))		 Merge.kif 456-460 Assuming @ROW is the opposite of, it follows that: if Y is a member of (@ROW), then Y is an instance of attribute
(=>
    (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
(=>
    (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)
(=>
    (exhaustiveDecomposition @ROW)
    (=>
        (inList ?ELEMENT
            (ListFn @ROW))
        (instance ?ELEMENT Class)))		 Merge.kif 550-554 Assuming @ROW is covered by @ROW, it follows that: if Y is a member of (@ROW), then Y is an instance of class
(=>
    (disjointDecomposition @ROW)
    (=>
        (inList ?ELEMENT
            (ListFn @ROW))
        (instance ?ELEMENT Class)))		 Merge.kif 566-570 Assuming @ROW is disjointly decomposed into @ROW, it follows that: if Y is a member of (@ROW), then Y is an instance of class
(=>
    (and
        (partition ?SUPER ?SUB1 ?SUB2)
        (instance ?INST ?SUPER)
        (not
            (instance ?INST ?SUB1)))
    (instance ?INST ?SUB2))		 Merge.kif 598-604 If X is exhaustively partitioned into Y and Z, W is an instance of X, and W is not an instance of Y, then W is an instance of Z
(=>
    (and
        (subAttribute ?ATTR1 ?ATTR2)
        (instance ?ATTR2 ?CLASS))
    (instance ?ATTR1 ?CLASS))		 Merge.kif 688-692 If X is a subattribute of Y and Y is an instance of Z, then X is an instance of Z
(=>
    (piece ?SUBSTANCE1 ?SUBSTANCE2)
    (forall (?CLASS)
        (=>
            (instance ?SUBSTANCE1 ?CLASS)
            (instance ?SUBSTANCE2 ?CLASS))))		 Merge.kif 967-972 If X is a piece of Y, then For all Class Z: if X is an instance of Z, then Y is an instance of Z
(=>
    (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
(=>
    (and
        (subclass ?OBJECTTYPE Substance)
        (instance ?OBJECT ?OBJECTTYPE)
        (piece ?PART ?OBJECT))
    (instance ?PART ?OBJECTTYPE))		 Merge.kif 1126-1131 If X is a subclass of substance, Y is an instance of X, and Z is a piece of Y, then Z is an instance of X
(=>
    (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

Display limited to 25 items. Show next 25

Display limited to 25 items. Show next 25

statement
-------------------------


(exists (?THING)
    (instance ?THING Entity))		 Merge.kif 817-818 There exists X such that X is an instance of entity
(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
(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
-------------------------


(instance instance BinaryPredicate) Merge.kif 80-80 instance is an instance of binary predicate
(instance immediateInstance AsymmetricRelation) Merge.kif 92-92 immediate instance is an instance of asymmetric relation
(instance immediateInstance IntransitiveRelation) Merge.kif 93-93 immediate instance is an instance of intransitive relation
(instance inverse BinaryPredicate) Merge.kif 106-106 inverse is an instance of binary predicate
(instance inverse IrreflexiveRelation) Merge.kif 107-107 inverse is an instance of irreflexive relation
(instance inverse IntransitiveRelation) Merge.kif 108-108 inverse is an instance of intransitive relation
(instance inverse SymmetricRelation) Merge.kif 109-109 inverse is an instance of symmetric relation
(instance inverse PartialValuedRelation) Merge.kif 110-110 inverse is an instance of partial valued relation
(instance subclass BinaryPredicate) Merge.kif 129-129 subclass is an instance of binary predicate
(instance subclass PartialOrderingRelation) Merge.kif 130-130 subclass is an instance of partial ordering relation
(instance immediateSubclass AsymmetricRelation) Merge.kif 144-144 immediate subclass is an instance of asymmetric relation
(instance immediateSubclass IntransitiveRelation) Merge.kif 145-145 immediate subclass is an instance of intransitive relation
(instance immediateSubclass BinaryPredicate) Merge.kif 146-146 immediate subclass is an instance of binary predicate
(instance subrelation BinaryPredicate) Merge.kif 163-163 subrelation is an instance of binary predicate
(instance subrelation PartialOrderingRelation) Merge.kif 164-164 subrelation is an instance of partial ordering relation
(instance domain TernaryPredicate) Merge.kif 201-201 domain is an instance of ternary predicate
(instance domainSubclass TernaryPredicate) Merge.kif 223-223 domain subclass is an instance of ternary predicate
(instance range BinaryPredicate) Merge.kif 298-298 range is an instance of binary predicate
(instance rangeSubclass BinaryPredicate) Merge.kif 325-325 range subclass is an instance of binary predicate
(instance valence BinaryPredicate) Merge.kif 351-351 valence is an instance of binary predicate
(instance valence SingleValuedRelation) Merge.kif 352-352 valence is an instance of single valued relation
(instance documentation TernaryPredicate) Merge.kif 360-360 documentation is an instance of ternary predicate
(instance format TernaryPredicate) Merge.kif 371-371 format is an instance of ternary predicate
(instance termFormat TernaryPredicate) Merge.kif 378-378 term format is an instance of ternary predicate
(instance disjoint BinaryPredicate) Merge.kif 385-385 disjoint is an instance of binary predicate

Display limited to 25 items. Show next 25

Display limited to 25 items. Show next 25


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

Show without tree

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