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

KB Term:  Term intersection
English Word: 

Sigma KEE - instance
instance

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


(instance instance BinaryPredicate) Merge.kif 80-80
(domain instance 1 Entity) Merge.kif 81-81
(domain instance 2 Class) Merge.kif 82-82
(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

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


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

antecedent
-------------------------


(=>
    (and
        (subclass ?X ?Y)
        (instance ?Z ?X))
    (instance ?Z ?Y))		 Merge.kif 137-141
(=>
    (and
        (subrelation ?REL1 ?REL2)
        (instance ?REL1 Predicate)
        (instance ?REL2 Predicate)
        (?REL1 @ROW))
    (?REL2 @ROW))		 Merge.kif 186-192
(=>
    (and
        (subrelation ?PRED1 ?PRED2)
        (instance ?PRED2 ?CLASS)
        (subclass ?CLASS InheritableRelation))
    (instance ?PRED1 ?CLASS))		 Merge.kif 194-199
(=>
    (and
        (instance ?REL1 Predicate)
        (instance ?REL2 Predicate)
        (disjointRelation ?REL1 ?REL2)
        (?REL1 @ROW2))
    (not
        (?REL2 @ROW2)))		 Merge.kif 439-445
(=>
    (and
        (partition ?SUPER ?SUB1 ?SUB2)
        (instance ?INST ?SUPER)
        (not
            (instance ?INST ?SUB1)))
    (instance ?INST ?SUB2))		 Merge.kif 598-604
(=>
    (and
        (subAttribute ?ATTR1 ?ATTR2)
        (instance ?ATTR2 ?CLASS))
    (instance ?ATTR1 ?CLASS))		 Merge.kif 688-692
(=>
    (instance ?CLASS Class)
    (subclass ?CLASS Entity))		 Merge.kif 820-822
(=>
    (instance ?PHYS Physical)
    (exists (?LOC ?TIME)
        (and
            (located ?PHYS ?LOC)
            (time ?PHYS ?TIME))))		 Merge.kif 831-836
(=>
    (instance ?O Object)
    (capability Translocation origin ?O))		 Merge.kif 846-848
(=>
    (instance ?O Object)
    (capability Translocation destination ?O))		 Merge.kif 850-852
(=>
    (instance ?OBJ SelfConnectedObject)
    (side
        (FrontFn ?OBJ) ?OBJ))		 Merge.kif 883-885
(=>
    (instance ?OBJ SelfConnectedObject)
    (side
        (BackFn ?OBJ) ?OBJ))		 Merge.kif 903-905
(=>
    (instance ?event VolcanicEruption)
    (exists (?volcano)
        (and
            (instance ?volcano Volcano)
            (agent ?event ?volcano))))		 Merge.kif 1030-1035
(=>
    (instance ?ERUPTING VolcanicEruption)
    (exists (?VOLCANO)
        (and
            (instance ?VOLCANO Volcano)
            (eventLocated ?ERUPTING ?VOLCANO))))		 Merge.kif 1041-1046
(=>
    (instance ?ERUPTING VolcanicEruption)
    (exists (?HEATING)
        (and
            (instance ?HEATING Heating)
            (subProcess ?HEATING ?ERUPTING))))		 Merge.kif 1048-1053
(=>
    (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
(=>
    (and
        (subclass ?OBJECTTYPE Substance)
        (instance ?OBJECT ?OBJECTTYPE)
        (piece ?PART ?OBJECT))
    (instance ?PART ?OBJECTTYPE))		 Merge.kif 1126-1131
(=>
    (and
        (instance ?OBJ Substance)
        (attribute ?OBJ ?ATTR)
        (piece ?PART ?OBJ))
    (attribute ?PART ?ATTR))		 Merge.kif 1133-1138
(=>
    (instance ?SUBSTANCE SyntheticSubstance)
    (exists (?PROCESS)
        (and
            (instance ?PROCESS IntentionalProcess)
            (result ?PROCESS ?SUBSTANCE)
            (instance ?SUBSTANCE Substance))))		 Merge.kif 1145-1151
(=>
    (instance ?ATOM Atom)
    (exists (?PROTON ?ELECTRON)
        (and
            (part ?PROTON ?ATOM)
            (part ?ELECTRON ?ATOM)
            (instance ?PROTON Proton)
            (instance ?ELECTRON Electron))))		 Merge.kif 1186-1193
(=>
    (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
(=>
    (instance ?PARTICLE SubatomicParticle)
    (exists (?ATOM)
        (and
            (instance ?ATOM Atom)
            (component ?PARTICLE ?ATOM))))		 Merge.kif 1211-1216
(=>
    (instance ?NUCLEUS AtomicNucleus)
    (exists (?NEUTRON ?PROTON)
        (and
            (component ?NEUTRON ?NUCLEUS)
            (component ?PROTON ?NUCLEUS)
            (instance ?NEUTRON Neutron)
            (instance ?PROTON Proton))))		 Merge.kif 1222-1229
(=>
    (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
(=>
    (and
        (instance ?MIXTURE Mixture)
        (piece ?SUBSTANCE ?MIXTURE)
        (not
            (instance ?SUBSTANCE Mixture)))
    (instance ?SUBSTANCE PureSubstance))		 Merge.kif 1273-1278

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
(=>
    (and
        (subclass ?X ?Y)
        (instance ?Z ?X))
    (instance ?Z ?Y))		 Merge.kif 137-141
(=>
    (and
        (subrelation ?PRED1 ?PRED2)
        (instance ?PRED2 ?CLASS)
        (subclass ?CLASS InheritableRelation))
    (instance ?PRED1 ?CLASS))		 Merge.kif 194-199
(=>
    (equal ?THING1 ?THING2)
    (forall (?CLASS)
        (<=>
            (instance ?THING1 ?CLASS)
            (instance ?THING2 ?CLASS))))		 Merge.kif 268-273
(=>
    (equal ?CLASS1 ?CLASS2)
    (forall (?THING)
        (<=>
            (instance ?THING ?CLASS1)
            (instance ?THING ?CLASS2))))		 Merge.kif 275-280
(=>
    (and
        (range ?FUNCTION ?CLASS)
        (equal
            (AssignmentFn ?FUNCTION @ROW) ?VALUE))
    (instance ?VALUE ?CLASS))		 Merge.kif 305-309
(=>
    (disjoint ?CLASS1 ?CLASS2)
    (not
        (exists (?INST)
            (and
                (instance ?INST ?CLASS1)
                (instance ?INST ?CLASS2)))))		 Merge.kif 393-399
(=>
    (contraryAttribute @ROW)
    (=>
        (inList ?ELEMENT
            (ListFn @ROW))
        (instance ?ELEMENT Attribute)))		 Merge.kif 456-460
(=>
    (and
        (exhaustiveAttribute ?CLASS @ROW)
        (inList ?ATTR
            (ListFn @ROW)))
    (instance ?ATTR Attribute))		 Merge.kif 489-493
(=>
    (and
        (exhaustiveAttribute ?CLASS @ROW)
        (inList ?ATTR
            (ListFn @ROW)))
    (instance ?ATTR ?CLASS))		 Merge.kif 495-499
(=>
    (exhaustiveAttribute ?CLASS @ROW)
    (forall (?ATTR1)
        (=>
            (instance ?ATTR1 ?CLASS)
            (exists (?ATTR2)
                (and
                    (inList ?ATTR2
                        (ListFn @ROW))
                    (equal ?ATTR1 ?ATTR2))))))		 Merge.kif 501-509
(=>
    (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
(=>
    (exhaustiveDecomposition @ROW)
    (=>
        (inList ?ELEMENT
            (ListFn @ROW))
        (instance ?ELEMENT Class)))		 Merge.kif 550-554
(=>
    (disjointDecomposition @ROW)
    (=>
        (inList ?ELEMENT
            (ListFn @ROW))
        (instance ?ELEMENT Class)))		 Merge.kif 566-570
(=>
    (and
        (partition ?SUPER ?SUB1 ?SUB2)
        (instance ?INST ?SUPER)
        (not
            (instance ?INST ?SUB1)))
    (instance ?INST ?SUB2))		 Merge.kif 598-604
(=>
    (and
        (subAttribute ?ATTR1 ?ATTR2)
        (instance ?ATTR2 ?CLASS))
    (instance ?ATTR1 ?CLASS))		 Merge.kif 688-692
(=>
    (piece ?SUBSTANCE1 ?SUBSTANCE2)
    (forall (?CLASS)
        (=>
            (instance ?SUBSTANCE1 ?CLASS)
            (instance ?SUBSTANCE2 ?CLASS))))		 Merge.kif 967-972
(=>
    (instance ?event VolcanicEruption)
    (exists (?volcano)
        (and
            (instance ?volcano Volcano)
            (agent ?event ?volcano))))		 Merge.kif 1030-1035
(=>
    (instance ?ERUPTING VolcanicEruption)
    (exists (?VOLCANO)
        (and
            (instance ?VOLCANO Volcano)
            (eventLocated ?ERUPTING ?VOLCANO))))		 Merge.kif 1041-1046
(=>
    (instance ?ERUPTING VolcanicEruption)
    (exists (?HEATING)
        (and
            (instance ?HEATING Heating)
            (subProcess ?HEATING ?ERUPTING))))		 Merge.kif 1048-1053
(=>
    (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
(=>
    (and
        (subclass ?OBJECTTYPE Substance)
        (instance ?OBJECT ?OBJECTTYPE)
        (piece ?PART ?OBJECT))
    (instance ?PART ?OBJECTTYPE))		 Merge.kif 1126-1131
(=>
    (instance ?SUBSTANCE SyntheticSubstance)
    (exists (?PROCESS)
        (and
            (instance ?PROCESS IntentionalProcess)
            (result ?PROCESS ?SUBSTANCE)
            (instance ?SUBSTANCE Substance))))		 Merge.kif 1145-1151
(=>
    (instance ?ATOM Atom)
    (exists (?PROTON ?ELECTRON)
        (and
            (part ?PROTON ?ATOM)
            (part ?ELECTRON ?ATOM)
            (instance ?PROTON Proton)
            (instance ?ELECTRON Electron))))		 Merge.kif 1186-1193
(=>
    (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

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
(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
(equal
    (PopulationFn ?AREA)
    (CardinalityFn
        (KappaFn ?PERSON
            (and
                (instance ?PERSON Human)
                (inhabits ?PERSON ?AREA)))))		 Mid-level-ontology.kif 34143-34148
(equal
    (OrganismPopulationFn ?O ?AREA)
    (CardinalityFn
        (KappaFn ?OI
            (and
                (instance ?OI ?O)
                (located ?OI ?AREA)))))		 Mid-level-ontology.kif 34167-34172
(not
    (and
        (instance ?CURSOR MouseCursor)
        (hasGUEState ?CURSOR GUE_ActiveState)))		 ComputerInput.kif 1968-1971
(not
    (and
        (hasGUEState ?WINDOW GUE_NonVisibleState)
        (hasGUEState ?WINDOW GUE_ActiveState)
        (instance ?WINDOW InterfaceWindow)))		 ComputerInput.kif 2027-2031
(not
    (and
        (instance ?CURSOR Cursor)
        (hasGUEState ?CURSOR GUE_SelectedState)))		 ComputerInput.kif 2242-2245
(exists (?T)
    (and
        (instance ?T
            (YearFn 2002))
        (holdsDuring ?T
            (coworker SteveJobsOfApple TimCookOfApple))))		 ComputingBrands.kif 2441-2445
(exists (?T)
    (and
        (instance ?T
            (YearFn 1976))
        (holdsDuring ?T
            (coworker SteveJobsOfApple SteveWozniakOfApple))))		 ComputingBrands.kif 2453-2457
(hasPurpose IBookstore
    (exists (?D)
        (and
            (instance ?D DownloadingOverNetwork)
            (instrument ?D IBookstore)
            (instance ?T Text)
            (objectTransferred ?D ?T))))		 ComputingBrands.kif 3216-3222
(exists (?FORMULA)
    (and
        (instance ?FORMULA Formula)
        (containsFormula ImmigrationAndNationalityAct_US ?FORMULA)
        (modalAttribute ?FORMULA Law)))		 Government.kif 2372-2376
(exists (?FORMULA)
    (and
        (instance ?FORMULA Formula)
        (containsFormula ImmigrationAndNationalityAct_Section219_US ?FORMULA)
        (modalAttribute ?FORMULA Law)))		 Government.kif 2379-2383
(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
(exists (?FORMULA)
    (and
        (instance ?FORMULA Formula)
        (containsFormula AntiterrorismAndEffectiveDeathPenaltyAct ?FORMULA)
        (modalAttribute ?FORMULA Law)))		 Government.kif 2395-2399
(holdsDuring
    (ImmediateFutureFn ?TIME)
    (and
        (instance ?TIME
            (YearFn 1996))
        (conventionalLongName "Agency for the French_Speaking Community" AgencyForTheFrenchSpeakingCommunity)))		 Government.kif 2757-2761
(holdsDuring
    (ImmediateFutureFn ?T)
    (and
        (instance ?T
            (DayFn 1
                (MonthFn October
                    (YearFn 1992))))
        (conventionalLongName "Andean Community of Nations" AndeanCommunityOfNations)))		 Government.kif 2783-2786
(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
(holdsDuring
    (FutureFn ?T)
    (and
        (instance Serbia IndependentState)
        (instance ?T
            (DayFn 5
                (MonthFn June
                    (YearFn 2006))))))		 Media.kif 2443-2446
(holdsDuring
    (FutureFn ?T)
    (and
        (instance Serbia EuropeanNation)
        (instance ?T
            (DayFn 5
                (MonthFn June
                    (YearFn 2006))))))		 Media.kif 2448-2451
(holdsDuring
    (FutureFn ?T)
    (and
        (names "Republic of Serbia" Serbia)
        (instance ?T
            (DayFn 5
                (MonthFn June
                    (YearFn 2006))))))		 Media.kif 2453-2456
(holdsDuring
    (FutureFn ?TIME)
    (and
        (instance ?TIME
            (DayFn 3
                (MonthFn June
                    (YearFn 2006))))
        (instance Montenegro IndependentState)))		 Media.kif 2470-2473
(holdsDuring
    (FutureFn ?TIME)
    (and
        (instance ?TIME
            (DayFn 3
                (MonthFn June
                    (YearFn 2006))))
        (instance Montenegro EuropeanNation)))		 Media.kif 2475-2478
(holdsDuring
    (FutureFn ?TIME)
    (and
        (instance ?TIME
            (DayFn 3
                (MonthFn June
                    (YearFn 2006))))
        (names "Montenegro" Montenegro)))		 Media.kif 2480-2483
(holdsDuring
    (FutureFn ?TIME)
    (and
        (instance ?TIME
            (DayFn 3
                (MonthFn June
                    (YearFn 2006))))
        (not
            (instance SerbiaAndMontenegro IndependentState))))		 Media.kif 2493-2497
(exists (?FORMULA)
    (and
        (instance ?FORMULA Formula)
        (containsFormula AmericansWithDisabilitiesAct_US ?FORMULA)
        (modalAttribute ?FORMULA Law)))		 Medicine.kif 3176-3180

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 immediateInstance AsymmetricRelation) Merge.kif 92-92
(instance immediateInstance IntransitiveRelation) Merge.kif 93-93
(instance inverse BinaryPredicate) Merge.kif 106-106
(instance inverse IrreflexiveRelation) Merge.kif 107-107
(instance inverse IntransitiveRelation) Merge.kif 108-108
(instance inverse SymmetricRelation) Merge.kif 109-109
(instance inverse PartialValuedRelation) Merge.kif 110-110
(instance subclass BinaryPredicate) Merge.kif 129-129
(instance subclass PartialOrderingRelation) Merge.kif 130-130
(instance immediateSubclass AsymmetricRelation) Merge.kif 144-144
(instance immediateSubclass IntransitiveRelation) Merge.kif 145-145
(instance immediateSubclass BinaryPredicate) Merge.kif 146-146
(instance subrelation BinaryPredicate) Merge.kif 163-163
(instance subrelation PartialOrderingRelation) Merge.kif 164-164
(instance domain TernaryPredicate) Merge.kif 201-201
(instance domainSubclass TernaryPredicate) Merge.kif 223-223
(instance range BinaryPredicate) Merge.kif 298-298
(instance rangeSubclass BinaryPredicate) Merge.kif 325-325
(instance valence BinaryPredicate) Merge.kif 351-351
(instance valence SingleValuedRelation) Merge.kif 352-352
(instance documentation TernaryPredicate) Merge.kif 360-360
(instance format TernaryPredicate) Merge.kif 371-371
(instance termFormat TernaryPredicate) Merge.kif 378-378
(instance disjoint BinaryPredicate) Merge.kif 385-385

Display limited to 25 items. Show next 25

Display limited to 25 items. Show next 25


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-ac69cf7a (2026-05-13) is open source software produced by Articulate Software and its partners