Browsing Interface : Welcome guest : log in 		[  Home |  Graph |  LogLearn |  ]  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 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 1316-1316 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 440-446 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 599-605 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 689-693 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 821-823 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 832-837 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 847-849 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 851-853 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 884-886 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 904-906 If X is an instance of self connected object, then a side of X is the back 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 1020-1036 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 1088-1093 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 1095-1100 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 1107-1113 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 1148-1155 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 1157-1166 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 1173-1178 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 1184-1191 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 1225-1233 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 1235-1240 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
(=>
    (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 1266-1274 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 ?COLL Collection)
    (exists (?OBJ)
        (member ?OBJ ?COLL)))		 Merge.kif 1305-1308 If X is an instance of collection, then there exists Y such that Y is a member of X
(=>
    (instance ?OBJ ContentBearingPhysical)
    (exists (?THING)
        (represents ?OBJ ?THING)))		 Merge.kif 1346-1349 If X is an instance of content bearing physical, then there exists Y such that X expresses Y

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 306-310 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 394-400 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 457-461 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 490-494 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 496-500 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 502-510 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 512-524 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 551-555 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 567-571 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 599-605 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 689-693 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 968-973 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 ?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 1020-1036 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 1088-1093 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 1107-1113 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 1148-1155 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 1157-1166 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 1173-1178 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 1184-1191 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 1225-1233 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

Display limited to 25 items. Show next 25

Display limited to 25 items. Show next 25

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


(exists (?THING)
    (instance ?THING Entity))		 Merge.kif 818-819 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 6148-6155 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
(decreasesLikelihood
    (exists (?X ?CUT ?PAPER ?CBO ?INFO)
        (and
            (instance ?X PaperShredder)
            (instance ?CUT Cutting)
            (instrument ?CUT ?X)
            (instance ?PAPER Paper)
            (patient ?CUT ?PAPER)
            (located ?CBO ?PAPER)
            (instance ?CBO VisualContentBearingObject)
            (containsInformation ?CBO ?INFO)))
    (exists (?READ)
        (and
            (instance ?READ Interpreting)
            (patient ?READ ?INFO)
            (earlier
                (WhenFn ?CUT)
                (WhenFn ?READ)))))		 Mid-level-ontology.kif 20112-20129 All of the following hold: (1) there exist ?X, ?CUT,, , ?PAPER,, , ?CBO (2) ?INFO such that ?X is an instance of paper shredder (3) ?CUT is an instance of cutting (4) ?X is an instrument for ?CUT (5) ?PAPER is an instance of paper (6) ?PAPER is a patient of ?CUT (7) ?CBO is located at ?PAPER (8) ?CBO is an instance of visual content bearing object (9) ?CBO contains information ?INFO decreases likelihood of there exists ?READ such that ?READ is an instance of interpreting (10) ?INFO is a patient of ?READ (11) the time of existence of ?CUT happens earlier than the time of existence of ?READ
(equal
    (PopulationFn ?AREA)
    (CardinalityFn
        (KappaFn ?PERSON
            (and
                (instance ?PERSON Human)
                (inhabits ?PERSON ?AREA)))))		 Mid-level-ontology.kif 34439-34444 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 34463-34468 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 1952-1955 ~{ 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 2011-2015 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 2226-2229 ~{ 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
(agreementEffectiveDate AntarcticTreaty
    (instance ?D
        (DayFn 23
            (MonthFn June
                (YearFn 1961)))))		 Geography.kif 4648-4648 ?D is an instance of the day 23 of month the month June is an agreement effective date of antarctic treaty
(containsInformation
    (forall (?COUNTRY ?ELECTION ?VOTING ?VOTER)
        (=>
            (and
                (instance ?COUNTRY Nation)
                (instance ?ELECTION
                    (ElectionFn ?COUNTRY))
                (instance ?VOTING
                    (VotingFn ?ELECTION))
                (agent ?VOTING ?VOTER))
            (citizen ?VOTER ?COUNTRY))) VoterCitizenshipRequirement)		 Government.kif 885-893 For all : if ?COUNTRY is an instance of nation, ?ELECTION is an instance of the election of ?COUNTRY, ?VOTING is an instance of the voting of ?ELECTION, and ?VOTER is an agent of ?VOTING, then ?VOTER is a citizen of ?COUNTRY
(containsInformation
    (forall (?POLITY ?AGENT ?ELECTION ?VOTINGAGE ?AGE)
        (=>
            (and
                (citizen ?AGENT ?POLITY)
                (suffrageAgeMinimum ?POLITY
                    (MeasureFn ?VOTINGAGE YearDuration))
                (age ?AGENT
                    (MeasureFn ?AGE YearDuration))
                (greaterThanOrEqualTo ?AGE ?VOTINGAGE)
                (instance ?ELECTION
                    (ElectionFn ?POLITY)))
            (capability
                (VotingFn ?ELECTION) agent ?AGENT))) UniversalSuffrageLaw)		 Government.kif 1054-1065 For all : if ?AGENT is a citizen of ?POLITY, ?VOTINGAGE year duration(s) is a suffrage age minimum of ?POLITY, the age of ?AGENT is ?AGE year duration(s), ?AGE is greater than or equal to ?VOTINGAGE, and ?ELECTION is an instance of the election of ?POLITY, then ?AGENT is capable of doing the voting of ?ELECTION as a agent
(containsInformation
    (forall (?POLITY ?VOTER ?ELECTION ?VOTINGAGE ?AGE)
        (=>
            (and
                (citizen ?VOTER ?POLITY)
                (suffrageAgeMinimum ?POLITY
                    (MeasureFn ?VOTINGAGE YearDuration))
                (age ?VOTER
                    (MeasureFn ?AGE YearDuration))
                (greaterThanOrEqualTo ?AGE ?VOTINGAGE)
                (instance ?ELECTION
                    (ElectionFn ?POLITY)))
            (exists (?VOTING)
                (and
                    (instance ?VOTING
                        (VotingFn ?ELECTION))
                    (agent ?VOTING ?VOTER))))) CompulsorySuffrageLaw)		 Government.kif 1122-1136 For all : if ?VOTER is a citizen of ?POLITY, ?VOTINGAGE year duration(s) is a suffrage age minimum of ?POLITY, the age of ?VOTER is ?AGE year duration(s), ?AGE is greater than or equal to ?VOTINGAGE, and ?ELECTION is an instance of the election of ?POLITY, then there exists ?VOTING such that ?VOTING is an instance of the voting of ?ELECTION and ?VOTER is an agent of ?VOTING
(containsInformation
    (forall (?AGENT ?VOTER ?ELECTION ?VOTING)
        (=>
            (and
                (instance ?ELECTION
                    (ElectionFn ?AGENT))
                (instance ?VOTING
                    (VotingFn ?ELECTION))
                (agent ?VOTING ?VOTER))
            (attribute ?VOTER Male))) ExclusiveMaleSuffrage)		 Government.kif 1203-1210 For all : if ?ELECTION is an instance of the election of ?AGENT, ?VOTING is an instance of the voting of ?ELECTION, and ?VOTER is an agent of ?VOTING, then male is an attribute of ?VOTER
(exists (?FORMULA)
    (and
        (instance ?FORMULA Formula)
        (containsInformation ?FORMULA ImmigrationAndNationalityAct_US)
        (modalAttribute ?FORMULA Law)))		 Government.kif 2363-2367 There exists X such that X is an instance of formula, X contains information immigration and nationality act_US, and the statement X has the modal force of law
(exists (?FORMULA)
    (and
        (instance ?FORMULA Formula)
        (containsInformation ?FORMULA ImmigrationAndNationalityAct_Section219_US)
        (modalAttribute ?FORMULA Law)))		 Government.kif 2370-2374 There exists X such that X is an instance of formula, X contains information immigration and nationality act- section219-US, and the statement X has the modal force of law
(exists (?FORMULA1 ?FORMULA2)
    (and
        (instance ?FORMULA1 Formula)
        (containsInformation ?FORMULA1 ImmigrationAndNationalityAct_US)
        (instance ?FORMULA2 Formula)
        (containsInformation ?FORMULA2 ImmigrationAndNationalityAct_Section219_US)
        (subsumesContentInstance ?FORMULA1 ?FORMULA2)))		 Government.kif 2376-2382 There exist X, Y such that X is an instance of formula, X contains information immigration and nationality act_US, Y is an instance of formula, Y contains information immigration and nationality act- section219-US, and X subsumes the content of Y
(exists (?FORMULA)
    (and
        (instance ?FORMULA Formula)
        (containsInformation ?FORMULA AntiterrorismAndEffectiveDeathPenaltyAct)
        (modalAttribute ?FORMULA Law)))		 Government.kif 2384-2388 There exists X such that X is an instance of formula, X contains information antiterrorism and effective death penalty act, 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 2746-2750 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 2772-2775 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 1972-1980 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 2498-2501 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 2503-2506 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

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 range AsymmetricRelation) Merge.kif 299-299 range is an instance of asymmetric relation
(instance rangeSubclass BinaryPredicate) Merge.kif 326-326 range subclass is an instance of binary predicate
(instance valence BinaryPredicate) Merge.kif 352-352 valence is an instance of binary predicate
(instance valence SingleValuedRelation) Merge.kif 353-353 valence is an instance of single valued relation
(instance documentation TernaryPredicate) Merge.kif 361-361 documentation is an instance of ternary predicate
(instance format TernaryPredicate) Merge.kif 372-372 format is an instance of ternary predicate
(instance termFormat TernaryPredicate) Merge.kif 379-379 term format is an instance of ternary predicate

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 is open source software produced by Articulate Software and its partners