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
        (connectedBodyPartTypes ?P1 ?P2 ?O)
        (instance ?OC ?O)
        (not
            (attribute ?H DiseaseOrSyndrome)))
    (exists (?PC1 ?PC2)
        (and
            (instance ?PC1 ?P1)
            (instance ?PC2 ?P2)
            (not
                (equal ?PC1 ?PC2))
            (part ?PC1 ?OC)
            (part ?PC2 ?OC)
            (connected ?PC1 ?PC2))))		 Anatomy.kif 32-46 If connected body parts X, Y and Z, W is an instance of Z, and disease or syndrome is not an attribute of V, then All of the following hold: (1) there exist U (2) T such that U is an instance of X (3) T is an instance of Y (4) equal U (5) T (6) U is a part of W (7) T is a part of W (8) U is connected to T
(=>
    (instance ?X XyphiodProcess)
    (material ?X Cartilage))		 Anatomy.kif 278-280 If X is an instance of sternum, then cartilage is made of X
(=>
    (and
        (instance ?R TrueRibBone)
        (part ?R ?H)
        (instance ?H Human)
        (not
            (attribute ?H DiseaseOrSyndrome)))
    (exists (?S)
        (and
            (instance ?S Sternum)
            (part ?S ?H)
            (connected ?S ?R))))		 Anatomy.kif 507-518 If X is an instance of costae verae, X is a part of Y, Y is an instance of human, and disease or syndrome is not an attribute of Y, then there exists Z such that Z is an instance of sternum, Z is a part of Y, and Z is connected to X
(=>
    (and
        (instance ?R FalseRibBone)
        (part ?R ?H)
        (instance ?H Human)
        (not
            (attribute ?H DiseaseOrSyndrome)))
    (not
        (exists (?S)
            (and
                (instance ?S Sternum)
                (part ?S ?H)
                (connected ?S ?R)))))		 Anatomy.kif 520-532 If X is an instance of costae spuriae, X is a part of Y, Y is an instance of human, and disease or syndrome is not an attribute of Y, then there doesn't exist Z such that Z is an instance of sternum, Z is a part of Y, and Z is connected to X
(=>
    (and
        (instance ?R CervicalVertebraBone)
        (part ?R ?H)
        (instance ?H Human)
        (not
            (attribute ?H DiseaseOrSyndrome)))
    (exists (?S)
        (and
            (instance ?S CervicalVertebraBone)
            (not
                (equal ?S ?R))
            (part ?S ?H)
            (connected ?S ?R))))		 Anatomy.kif 576-589 If X is an instance of cervical vertebra bone, X is a part of Y, Y is an instance of human, and disease or syndrome is not an attribute of Y, then there exists Z such that Z is an instance of cervical vertebra bone, equal Z, X, Z is a part of Y, and Z is connected to X
(=>
    (and
        (instance ?R LumbarVertebraBone)
        (part ?R ?H)
        (instance ?H Human)
        (not
            (attribute ?H DiseaseOrSyndrome)))
    (exists (?S)
        (and
            (instance ?S LumbarVertebraBone)
            (not
                (equal ?S ?R))
            (part ?S ?H)
            (connected ?S ?R))))		 Anatomy.kif 616-629 If X is an instance of lumbar vertebra bone, X is a part of Y, Y is an instance of human, and disease or syndrome is not an attribute of Y, then there exists Z such that Z is an instance of lumbar vertebra bone, equal Z, X, Z is a part of Y, and Z is connected to X
(=>
    (and
        (instance ?R ThoracicVertebraBone)
        (part ?R ?H)
        (instance ?H Human)
        (not
            (attribute ?H DiseaseOrSyndrome)))
    (exists (?S)
        (and
            (instance ?S ThoracicVertebraBone)
            (not
                (equal ?S ?R))
            (part ?S ?H)
            (connected ?S ?R))))		 Anatomy.kif 684-697 If X is an instance of thoracic vertebra bone, X is a part of Y, Y is an instance of human, and disease or syndrome is not an attribute of Y, then there exists Z such that Z is an instance of thoracic vertebra bone, equal Z, X, Z is a part of Y, and Z is connected to X
(=>
    (and
        (instance ?E Eyebrow)
        (attribute ?H Healthy)
        (part ?E ?H))
    (exists (?EYE)
        (and
            (instance ?EYE Eye)
            (part ?EYE ?H)
            (orientation ?EYE ?E Near))))		 Anatomy.kif 1472-1481 If X is an instance of eyebrow, healthy is an attribute of Y, and X is a part of Y, then there exists Z such that Z is an instance of eye, Z is a part of Y, and Z is near to X
(=>
    (and
        (instance ?E Eyebrow)
        (attribute ?H Healthy)
        (part ?E ?H)
        (member ?C ?E))
    (memberCount ?E 2))		 Anatomy.kif 1483-1489 If X is an instance of eyebrow, healthy is an attribute of Y, X is a part of Y, and Z is a member of X, then 2 is a member count of X
(=>
    (and
        (instance ?E Eyebrow)
        (attribute ?H Healthy)
        (part ?E ?H)
        (member ?C ?E))
    (exists (?HAIR)
        (and
            (instance ?HAIR Hair)
            (part ?HAIR ?E))))		 Anatomy.kif 1491-1500 If X is an instance of eyebrow, healthy is an attribute of Y, X is a part of Y, and Z is a member of X, then there exists W such that W is an instance of hair and W is a part of X
(=>
    (and
        (instance ?E Eyebrow)
        (holdsDuring ?T
            (and
                (attribute ?H Healthy)
                (attribute ?H Standing)))
        (part ?E ?H))
    (exists (?EYE)
        (and
            (instance ?EYE Eye)
            (part ?EYE ?H)
            (orientation ?E ?EYE Above))))		 Anatomy.kif 1502-1514 If X is an instance of eyebrow, healthy is an attribute of Y and standing is an attribute of Y holds during Z, and X is a part of Y, then there exists W such that W is an instance of eye, W is a part of Y, and X is above to W
(=>
    (and
        (instance ?F Forehead)
        (holdsDuring ?T
            (and
                (attribute ?H Healthy)
                (attribute ?H Standing)))
        (part ?E ?H))
    (exists (?EYE)
        (and
            (instance ?EYE Eye)
            (part ?EYE ?H)
            (orientation ?F ?EYE Above))))		 Anatomy.kif 1521-1533 If X is an instance of forehead, healthy is an attribute of Y and standing is an attribute of Y holds during Z, and W is a part of Y, then there exists V such that V is an instance of eye, V is a part of Y, and X is above to V
(=>
    (and
        (instance ?ET EustachianTube)
        (part ?ET ?H)
        (attribute ?H Healthy)
        (length ?ET
            (MeasureFn ?N Centimeter)))
    (approximateValue ?N 35.0))		 Anatomy.kif 1550-1557 If X is an instance of Eustachian tube, X is a part of Y, healthy is an attribute of Y, and the length of X is Z centimeter(s), then the approximate value of Z is 35.0
(=>
    (and
        (instance ?ET EustachianTube)
        (part ?ET ?H)
        (attribute ?H Healthy)
        (diameter ?ET
            (MeasureFn ?N Millimeter)))
    (approximateValue ?N 3.0))		 Anatomy.kif 1559-1566 If X is an instance of Eustachian tube, X is a part of Y, healthy is an attribute of Y, and the diameter of X is Z millimeter(s), then the approximate value of Z is 3.0
(=>
    (instance ?U Urethra)
    (hasPurpose ?U
        (exists (?UR)
            (and
                (instance ?UR Urination)
                (instrument ?UR ?U)))))		 Anatomy.kif 1583-1589 If X is an instance of urethra, then X has the purpose there exists Y such that Y is an instance of urination and X is an instrument for Y
(=>
    (and
        (instance ?ET AuditoryCanal)
        (part ?ET ?H)
        (attribute ?H Healthy)
        (length ?ET
            (MeasureFn ?N Centimeter)))
    (approximateValue ?N 2.5))		 Anatomy.kif 1600-1607 If X is an instance of auditory canal, X is a part of Y, healthy is an attribute of Y, and the length of X is Z centimeter(s), then the approximate value of Z is 2.5
(=>
    (and
        (instance ?ET AuditoryCanal)
        (part ?ET ?H)
        (attribute ?H Healthy)
        (diameter ?ET
            (MeasureFn ?N Millimeter)))
    (approximateValue ?N 0.7))		 Anatomy.kif 1609-1616 If X is an instance of auditory canal, X is a part of Y, healthy is an attribute of Y, and the diameter of X is Z millimeter(s), then the approximate value of Z is 0.7
(=>
    (and
        (instance ?E Eardrum)
        (part ?E ?H)
        (experiencer ?HEAR ?H)
        (attribute ?H Healthy)
        (instance ?HEAR Hearing))
    (instrument ?HEAR ?E))		 Anatomy.kif 1669-1676 If X is an instance of myringa, X is a part of Y, Y experiences Z, healthy is an attribute of Y, and Z is an instance of hearing, then X is an instrument for Z
(=>
    (and
        (instance ?S Speaking)
        (instance ?J Jaw)
        (agent ?S ?H)
        (part ?J ?H))
    (modalAttribute
        (exists (?M)
            (and
                (instance ?M BodyMotion)
                (objectTransferred ?M ?J)
                (during
                    (WhenFn ?M)
                    (WhenFn ?S)))) Likely))		 Anatomy.kif 1697-1709 If X is an instance of speaking, Y is an instance of jaw, Z is an agent of X, and Y is a part of Z, then the statement there exists W such that W is an instance of body motion, the object transferred in W is Y, and the time of existence of W takes place during the time of existence of X has the modal force of likely
(=>
    (and
        (muscleOrigin ?MC ?BPC)
        (instance ?H Human)
        (attribute ?H Healthy))
    (exists (?M ?BP)
        (and
            (instance ?M ?MC)
            (instance ?BP ?BPC)
            (part ?M ?H)
            (part ?BP ?H)
            (connected ?M ?BP))))		 Anatomy.kif 1728-1739 If the origin of X is Y, Z is an instance of human, and healthy is an attribute of Z, then there exist W, V such that W is an instance of X, V is an instance of Y, W is a part of Z, V is a part of Z, and W is connected to V
(=>
    (and
        (muscleOrigin ?MC ?BPC)
        (instance ?H Human)
        (holdsDuring ?T
            (attribute ?H StandardAnatomicalPosition))
        (attribute ?H Healthy)
        (instance ?C MuscularContraction)
        (during
            (WhenFn ?C) ?T)
        (instance ?M ?MC)
        (part ?M ?H)
        (instrument ?C ?M)
        (physicalEnd ?E ?M)
        (meetsSpatially ?E ?BP)
        (holdsDuring
            (BeginFn ?C)
            (located ?E ?L)))
    (holdsDuring
        (EndFn ?C)
        (located ?E ?L)))		 Anatomy.kif 1741-1762 If All of the following hold: (1) the origin of X is Y (2) Z is an instance of human (3) standard anatomical position is an attribute of Z holds during W (4) healthy is an attribute of Z (5) V is an instance of muscular contraction (6) the time of existence of V takes place during W (7) U is an instance of X (8) U is a part of Z (9) U is an instrument for V (10) one end of U is T (11) T meets S (12) T is located at R holds during the beginning of V, then T is located at R holds during the end of V
(=>
    (and
        (muscleInsertion ?MC ?BPC)
        (instance ?H Human)
        (attribute ?H Healthy))
    (exists (?M ?BP)
        (and
            (instance ?M ?MC)
            (instance ?BP ?BPC)
            (part ?M ?H)
            (part ?BP ?H)
            (connected ?M ?BP))))		 Anatomy.kif 1778-1789 If the insertion point of X is Y, Z is an instance of human, and healthy is an attribute of Z, then there exist W, V such that W is an instance of X, V is an instance of Y, W is a part of Z, V is a part of Z, and W is connected to V
(=>
    (and
        (muscleInsertion ?MC ?BPC)
        (instance ?H Human)
        (holdsDuring ?T
            (attribute ?H StandardAnatomicalPosition))
        (attribute ?H Healthy)
        (instance ?C MuscularContraction)
        (during
            (WhenFn ?C) ?T)
        (instance ?M ?MC)
        (part ?M ?H)
        (instrument ?C ?M)
        (physicalEnd ?E ?M)
        (meetsSpatially ?E ?BP)
        (holdsDuring
            (BeginFn ?C)
            (located ?E ?L)))
    (holdsDuring
        (EndFn ?C)
        (not
            (located ?E ?L))))		 Anatomy.kif 1791-1813 If All of the following hold: (1) the insertion point of X is Y (2) Z is an instance of human (3) standard anatomical position is an attribute of Z holds during W (4) healthy is an attribute of Z (5) V is an instance of muscular contraction (6) the time of existence of V takes place during W (7) U is an instance of X (8) U is a part of Z (9) U is an instrument for V (10) one end of U is T (11) T meets S (12) T is located at R holds during the beginning of V, then T is not located at R holds during the end of V
(=>
    (and
        (holdsDuring ?T
            (and
                (attribute ?H Prone)
                (orientation ?H ?O On)))
        (instance ?C Chest)
        (part ?C ?H))
    (meetsSpatially ?C ?O))		 Anatomy.kif 1832-1840 If prone is an attribute of X and X is on to Y holds during Z, W is an instance of chest, and W is a part of X, then W meets Y
(=>
    (and
        (instance ?C Chest)
        (part ?C ?P)
        (equal ?B
            (BackFn ?P)))
    (not
        (part ?C ?B)))		 Anatomy.kif 1856-1863 If X is an instance of chest, X is a part of Y, and equal Z and the back of Y, then X is not a part of Z

Display limited to 25 items. Show next 25

Display limited to 25 items. Show next 25

consequent
-------------------------


(=>
    (and
        (connectedBodyPartTypes ?P1 ?P2 ?O)
        (instance ?OC ?O)
        (not
            (attribute ?H DiseaseOrSyndrome)))
    (exists (?PC1 ?PC2)
        (and
            (instance ?PC1 ?P1)
            (instance ?PC2 ?P2)
            (not
                (equal ?PC1 ?PC2))
            (part ?PC1 ?OC)
            (part ?PC2 ?OC)
            (connected ?PC1 ?PC2))))		 Anatomy.kif 32-46 If connected body parts X, Y and Z, W is an instance of Z, and disease or syndrome is not an attribute of V, then All of the following hold: (1) there exist U (2) T such that U is an instance of X (3) T is an instance of Y (4) equal U (5) T (6) U is a part of W (7) T is a part of W (8) U is connected to T
(=>
    (and
        (instance ?R TrueRibBone)
        (part ?R ?H)
        (instance ?H Human)
        (not
            (attribute ?H DiseaseOrSyndrome)))
    (exists (?S)
        (and
            (instance ?S Sternum)
            (part ?S ?H)
            (connected ?S ?R))))		 Anatomy.kif 507-518 If X is an instance of costae verae, X is a part of Y, Y is an instance of human, and disease or syndrome is not an attribute of Y, then there exists Z such that Z is an instance of sternum, Z is a part of Y, and Z is connected to X
(=>
    (and
        (instance ?R FalseRibBone)
        (part ?R ?H)
        (instance ?H Human)
        (not
            (attribute ?H DiseaseOrSyndrome)))
    (not
        (exists (?S)
            (and
                (instance ?S Sternum)
                (part ?S ?H)
                (connected ?S ?R)))))		 Anatomy.kif 520-532 If X is an instance of costae spuriae, X is a part of Y, Y is an instance of human, and disease or syndrome is not an attribute of Y, then there doesn't exist Z such that Z is an instance of sternum, Z is a part of Y, and Z is connected to X
(=>
    (and
        (instance ?R CervicalVertebraBone)
        (part ?R ?H)
        (instance ?H Human)
        (not
            (attribute ?H DiseaseOrSyndrome)))
    (exists (?S)
        (and
            (instance ?S CervicalVertebraBone)
            (not
                (equal ?S ?R))
            (part ?S ?H)
            (connected ?S ?R))))		 Anatomy.kif 576-589 If X is an instance of cervical vertebra bone, X is a part of Y, Y is an instance of human, and disease or syndrome is not an attribute of Y, then there exists Z such that Z is an instance of cervical vertebra bone, equal Z, X, Z is a part of Y, and Z is connected to X
(=>
    (and
        (instance ?R LumbarVertebraBone)
        (part ?R ?H)
        (instance ?H Human)
        (not
            (attribute ?H DiseaseOrSyndrome)))
    (exists (?S)
        (and
            (instance ?S LumbarVertebraBone)
            (not
                (equal ?S ?R))
            (part ?S ?H)
            (connected ?S ?R))))		 Anatomy.kif 616-629 If X is an instance of lumbar vertebra bone, X is a part of Y, Y is an instance of human, and disease or syndrome is not an attribute of Y, then there exists Z such that Z is an instance of lumbar vertebra bone, equal Z, X, Z is a part of Y, and Z is connected to X
(=>
    (and
        (instance ?R ThoracicVertebraBone)
        (part ?R ?H)
        (instance ?H Human)
        (not
            (attribute ?H DiseaseOrSyndrome)))
    (exists (?S)
        (and
            (instance ?S ThoracicVertebraBone)
            (not
                (equal ?S ?R))
            (part ?S ?H)
            (connected ?S ?R))))		 Anatomy.kif 684-697 If X is an instance of thoracic vertebra bone, X is a part of Y, Y is an instance of human, and disease or syndrome is not an attribute of Y, then there exists Z such that Z is an instance of thoracic vertebra bone, equal Z, X, Z is a part of Y, and Z is connected to X
(=>
    (and
        (instance ?E Eyebrow)
        (attribute ?H Healthy)
        (part ?E ?H))
    (exists (?EYE)
        (and
            (instance ?EYE Eye)
            (part ?EYE ?H)
            (orientation ?EYE ?E Near))))		 Anatomy.kif 1472-1481 If X is an instance of eyebrow, healthy is an attribute of Y, and X is a part of Y, then there exists Z such that Z is an instance of eye, Z is a part of Y, and Z is near to X
(=>
    (and
        (instance ?E Eyebrow)
        (attribute ?H Healthy)
        (part ?E ?H)
        (member ?C ?E))
    (exists (?HAIR)
        (and
            (instance ?HAIR Hair)
            (part ?HAIR ?E))))		 Anatomy.kif 1491-1500 If X is an instance of eyebrow, healthy is an attribute of Y, X is a part of Y, and Z is a member of X, then there exists W such that W is an instance of hair and W is a part of X
(=>
    (and
        (instance ?E Eyebrow)
        (holdsDuring ?T
            (and
                (attribute ?H Healthy)
                (attribute ?H Standing)))
        (part ?E ?H))
    (exists (?EYE)
        (and
            (instance ?EYE Eye)
            (part ?EYE ?H)
            (orientation ?E ?EYE Above))))		 Anatomy.kif 1502-1514 If X is an instance of eyebrow, healthy is an attribute of Y and standing is an attribute of Y holds during Z, and X is a part of Y, then there exists W such that W is an instance of eye, W is a part of Y, and X is above to W
(=>
    (and
        (instance ?F Forehead)
        (holdsDuring ?T
            (and
                (attribute ?H Healthy)
                (attribute ?H Standing)))
        (part ?E ?H))
    (exists (?EYE)
        (and
            (instance ?EYE Eye)
            (part ?EYE ?H)
            (orientation ?F ?EYE Above))))		 Anatomy.kif 1521-1533 If X is an instance of forehead, healthy is an attribute of Y and standing is an attribute of Y holds during Z, and W is a part of Y, then there exists V such that V is an instance of eye, V is a part of Y, and X is above to V
(=>
    (instance ?U Urethra)
    (hasPurpose ?U
        (exists (?UR)
            (and
                (instance ?UR Urination)
                (instrument ?UR ?U)))))		 Anatomy.kif 1583-1589 If X is an instance of urethra, then X has the purpose there exists Y such that Y is an instance of urination and X is an instrument for Y
(=>
    (holdsDuring ?T
        (attribute ?H
            (ImpairedBodyPartFn Eardrum)))
    (modalAttribute
        (not
            (exists (?HEAR)
                (and
                    (instance ?HEAR Hearing)
                    (during
                        (WhenFn ?HEAR) ?T)
                    (experiencer ?HEAR ?H)))) Likely))		 Anatomy.kif 1678-1689 If impaired body part fn myringa is an attribute of X holds during Y, then the statement there doesn't exist Z such that Z is an instance of hearing, the time of existence of Z takes place during Y, and X experiences Z has the modal force of likely
(=>
    (and
        (instance ?S Speaking)
        (instance ?J Jaw)
        (agent ?S ?H)
        (part ?J ?H))
    (modalAttribute
        (exists (?M)
            (and
                (instance ?M BodyMotion)
                (objectTransferred ?M ?J)
                (during
                    (WhenFn ?M)
                    (WhenFn ?S)))) Likely))		 Anatomy.kif 1697-1709 If X is an instance of speaking, Y is an instance of jaw, Z is an agent of X, and Y is a part of Z, then the statement there exists W such that W is an instance of body motion, the object transferred in W is Y, and the time of existence of W takes place during the time of existence of X has the modal force of likely
(=>
    (and
        (muscleOrigin ?MC ?BPC)
        (instance ?H Human)
        (attribute ?H Healthy))
    (exists (?M ?BP)
        (and
            (instance ?M ?MC)
            (instance ?BP ?BPC)
            (part ?M ?H)
            (part ?BP ?H)
            (connected ?M ?BP))))		 Anatomy.kif 1728-1739 If the origin of X is Y, Z is an instance of human, and healthy is an attribute of Z, then there exist W, V such that W is an instance of X, V is an instance of Y, W is a part of Z, V is a part of Z, and W is connected to V
(=>
    (and
        (muscleInsertion ?MC ?BPC)
        (instance ?H Human)
        (attribute ?H Healthy))
    (exists (?M ?BP)
        (and
            (instance ?M ?MC)
            (instance ?BP ?BPC)
            (part ?M ?H)
            (part ?BP ?H)
            (connected ?M ?BP))))		 Anatomy.kif 1778-1789 If the insertion point of X is Y, Z is an instance of human, and healthy is an attribute of Z, then there exist W, V such that W is an instance of X, V is an instance of Y, W is a part of Z, V is a part of Z, and W is connected to V
(=>
    (instance ?N Nerve)
    (exists (?NC)
        (and
            (instance ?NC NerveCell)
            (part ?NC ?N))))		 Anatomy.kif 1946-1951 If X is an instance of nerve, then there exists Y such that Y is an instance of nerve cell and Y is a part of X
(=>
    (and
        (ennervates ?NC ?MC)
        (instance ?N ?NC)
        (instance ?M ?MC)
        (part ?N ?H)
        (part ?M ?H)
        (attribute ?H Healthy)
        (instance ?H Human))
    (hasPurpose ?N
        (exists (?NF ?C)
            (and
                (instance ?NF NerveFiring)
                (instrument ?NF ?N)
                (instance ?MC MuscleContraction)
                (instrument ?MV ?M)
                (causes ?NF ?MC)))))		 Anatomy.kif 1961-1977 If All of the following hold: (1) ennervates X and Y (2) Z is an instance of X (3) W is an instance of Y (4) Z is a part of V (5) W is a part of V (6) healthy is an attribute of V (7) V is an instance of human, then Z has the purpose there exist U, T such that U is an instance of nerve firing, Z is an instrument for U, Y is an instance of MuscleContraction, W is an instrument for S, and U causes Y
(=>
    (and
        (suppliesBlood ?AC ?BPC)
        (instance ?A ?AC)
        (instance ?BP ?BPC))
    (hasPurpose ?A
        (exists (?BF ?B)
            (and
                (instance ?BF LiquidMotion)
                (objectTransferred ?BF ?B)
                (instance ?B Blood)
                (destination ?BF ?BP)))))		 Anatomy.kif 1987-1998 If supplies blood X and Y, Z is an instance of X, and W is an instance of Y, then Z has the purpose there exist V, U such that V is an instance of liquid motion, the object transferred in V is U, U is an instance of blood, and V ends up at W
(=>
    (attribute ?D Dorsal)
    (exists (?O)
        (and
            (or
                (instance ?O Organism)
                (instance ?O BodyPart))
            (not
                (and
                    (instance ?O Organism)
                    (instance ?O BodyPart)))
            (part ?D ?O)
            (equal ?B
                (BackFn ?O))
            (meetsSpatially ?B ?D))))		 Anatomy.kif 2005-2019 If dorsal is an attribute of X, then there exists Y such that Y is an instance of organism or Y is an instance of body part and ~{ Y is an instance of organism } or ~{ Y is an instance of body part } and X is a part of Y and equal Z and the back of Y and Z meets X
(=>
    (attribute ?V Ventral)
    (exists (?O ?F)
        (and
            (or
                (instance ?O Organism)
                (instance ?O BodyPart))
            (not
                (and
                    (instance ?O Organism)
                    (instance ?O BodyPart)))
            (part ?V ?O)
            (equal ?F
                (FrontFn ?O))
            (meetsSpatially ?F ?V))))		 Anatomy.kif 2026-2040 If ventral is an attribute of X, then there exist Y and Z such that Y is an instance of organism or Y is an instance of body part and ~{ Y is an instance of organism } or ~{ Y is an instance of body part } and X is a part of Y and equal Z and the front of Y and Z meets X
(=>
    (instance ?A Abducting)
    (exists (?BP ?ORGANISM ?TORSO ?MAF)
        (and
            (instance ?BP BodyPart)
            (instance ?ORGANISM Organism)
            (instance ?TORSO Torso)
            (not
                (equal ?BP ?TORSO))
            (subProcess ?MAF MovingAwayFrom)
            (patient ?MAF ?BP)
            (patient ?MAF ?TORSO)
            (part ?BP ?ORGANISM)
            (part ?TORSO ?ORGANISM)
            (experiencer ?A Organism)
            (moves ?A ?BP))))		 Anatomy.kif 2048-2063 If X is an instance of abducting, then All of the following hold: (1) there exist Y, Z,, , W (2) V such that Y is an instance of body part (3) Z is an instance of organism (4) W is an instance of torso (5) equal Y (6) W (7) V is a subprocess of moving away from (8) Y is a patient of V (9) W is a patient of V (10) Y is a part of Z (11) W is a part of Z (12) organism experiences X (13) Y moves during X
(=>
    (instance ?A Adducting)
    (exists (?BP ?ORGANISM ?TORSO ?MT)
        (and
            (instance ?BP BodyPart)
            (instance ?ORGANISM Organism)
            (instance ?TORSO Torso)
            (not
                (equal ?BP ?TORSO))
            (instance ?MT MovingTowards)
            (subProcess ?MT ?A)
            (patient ?MT ?BP)
            (patient ?MT ?TORSO)
            (part ?BP ?ORGANISM)
            (part ?TORSO ?ORGANISM)
            (experiencer ?A Organism)
            (moves ?A ?BP))))		 Anatomy.kif 2072-2088 If X is an instance of adducting, then All of the following hold: (1) there exist Y, Z,, , W (2) V such that Y is an instance of body part (3) Z is an instance of organism (4) W is an instance of torso (5) equal Y (6) W (7) V is an instance of moving towards (8) V is a subprocess of X (9) Y is a patient of V (10) W is a patient of V (11) Y is a part of Z (12) W is a part of Z (13) organism experiences X (14) Y moves during X
(=>
    (instance ?X Suhur)
    (exists (?R ?S ?D)
        (and
            (instance ?S Sunrise)
            (instance ?R Ramadan)
            (instance ?D Day)
            (during ?D ?R)
            (during
                (WhenFn ?X) ?D)
            (during ?S ?D)
            (before
                (WhenFn ?X) ?S))))		 ArabicCulture.kif 36-46 If X is an instance of suhur, then All of the following hold: (1) there exist Y, Z (2) W such that Z is an instance of sunrise (3) Y is an instance of ramadan (4) W is an instance of day (5) W takes place during Y (6) the time of existence of X takes place during W (7) Z takes place during W (8) the time of existence of X happens before Z
(=>
    (and
        (instance ?H Man)
        (attribute ?H Mausaharati)
        (instance ?D Drumming)
        (agent ?D ?H)
        (instance ?DAY Day)
        (instance ?S Sunrise)
        (during ?S ?DAY)
        (earlier
            (WhenFn ?D) ?S))
    (hasPurpose ?D
        (exists (?P ?SUHUR ?WU)
            (and
                (instance ?WU WakingUp)
                (experiencer ?WU ?P)
                (instance ?SUHUR Suhur)
                (agent ?SUHUR ?P)
                (earlier
                    (WhenFn ?WU)
                    (WhenFn ?SUHUR))
                (during
                    (WhenFn ?WU) ?DAY)
                (during
                    (WhenFn ?SUHUR) ?DAY)))))		 ArabicCulture.kif 65-84 If All of the following hold: (1) X is an instance of man (2) mausaharati is an attribute of X (3) Y is an instance of drumming (4) X is an agent of Y (5) Z is an instance of day (6) W is an instance of sunrise (7) W takes place during Z (8) the time of existence of Y happens earlier than W, then All of the following hold: (1) Y has the purpose there exist V, U (2) T such that T is an instance of waking up (3) V experiences T (4) U is an instance of suhur (5) V is an agent of U (6) the time of existence of T happens earlier than the time of existence of U (7) the time of existence of T takes place during Z (8) the time of existence of U takes place during Z
(=>
    (instance ?X Iftar)
    (exists (?R ?S ?D)
        (and
            (instance ?S Sunset)
            (instance ?R Ramadan)
            (instance ?D Day)
            (during ?D ?R)
            (during
                (WhenFn ?X) ?D)
            (during ?S ?D)
            (before ?S
                (WhenFn ?X)))))		 ArabicCulture.kif 91-101 If X is an instance of iftar, then All of the following hold: (1) there exist Y, Z (2) W such that Z is an instance of sunset (3) Y is an instance of ramadan (4) W is an instance of day (5) W takes place during Y (6) the time of existence of X takes place during W (7) Z takes place during W (8) Z happens before the time of existence of X

Display limited to 25 items. Show next 25

Display limited to 25 items. Show next 25

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


(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
(holdsDuring
    (FutureFn ?T)
    (and
        (names "Republic of Serbia" Serbia)
        (instance ?T
            (DayFn 5
                (MonthFn June
                    (YearFn 2006))))))		 Media.kif 2508-2511 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 2525-2528 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 2530-2533 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 2535-2538 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 2548-2552 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

Display limited to 25 items. Show next 25

Display limited to 25 items. Show next 25

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


(instance connectedBodyPartTypes TernaryPredicate) Anatomy.kif 23-23 connected body parts is an instance of ternary predicate
(instance muscleOrigin BinaryPredicate) Anatomy.kif 1718-1718 muscle origin is an instance of binary predicate
(instance muscleInsertion BinaryPredicate) Anatomy.kif 1768-1768 muscle insertion is an instance of binary predicate
(instance LateralRecumbant BodyPosition) Anatomy.kif 1865-1865 Lateral recumbant is an instance of body position
(instance ennervates BinaryPredicate) Anatomy.kif 1953-1953 ennervates is an instance of binary predicate
(instance suppliesBlood BinaryPredicate) Anatomy.kif 1979-1979 supplies blood is an instance of binary predicate
(instance Dorsal Attribute) Anatomy.kif 2003-2003 Dorsal is an instance of attribute
(instance Ventral Attribute) Anatomy.kif 2024-2024 Ventral is an instance of attribute
(instance Mausaharati SocialRole) ArabicCulture.kif 51-51 Mausaharati is an instance of social role
(instance Udhiyah RelationalAttribute) ArabicCulture.kif 258-258 Udhiyah is an instance of relational attribute
(instance paternalUncle BinaryPredicate) ArabicCulture.kif 558-558 paternal uncle is an instance of binary predicate
(instance maternalUncle BinaryPredicate) ArabicCulture.kif 571-571 maternal uncle is an instance of binary predicate
(instance paternalAunt BinaryPredicate) ArabicCulture.kif 584-584 paternal aunt is an instance of binary predicate
(instance maternalAunt BinaryPredicate) ArabicCulture.kif 597-597 maternal aunt is an instance of binary predicate
(instance fathersBrothersWife BinaryPredicate) ArabicCulture.kif 610-610 fathers brothers wife is an instance of binary predicate
(instance mothersBrothersWife BinaryPredicate) ArabicCulture.kif 624-624 mothers brothers wife is an instance of binary predicate
(instance fathersSistersHusband BinaryPredicate) ArabicCulture.kif 638-638 fathers sisters husband is an instance of binary predicate
(instance mothersSistersHusband BinaryPredicate) ArabicCulture.kif 652-652 mothers sisters husband is an instance of binary predicate
(instance fathersBrothersSon BinaryPredicate) ArabicCulture.kif 666-666 fathers brothers son is an instance of binary predicate
(instance fathersBrothersDaughter BinaryPredicate) ArabicCulture.kif 680-680 fathers brothers daughter is an instance of binary predicate
(instance mothersBrothersSon BinaryPredicate) ArabicCulture.kif 694-694 mothers brothers son is an instance of binary predicate
(instance mothersBrothersDaughter BinaryPredicate) ArabicCulture.kif 708-708 mothers brothers daughter is an instance of binary predicate
(instance fathersSistersSon BinaryPredicate) ArabicCulture.kif 722-722 fathers sisters son is an instance of binary predicate
(instance fathersSistersDaughter BinaryPredicate) ArabicCulture.kif 736-736 fathers sisters daughter is an instance of binary predicate
(instance mothersSistersSon BinaryPredicate) ArabicCulture.kif 750-750 mothers sisters son is an instance of binary 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