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


KB Term:  Term intersection
English Word: 

Sigma KEE - not
not

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
(=>
    (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 ?A1 Automobile)
        (instance ?A2 Automobile)
        (instance ?S1 AutomobileShock)
        (part ?S1 ?A1)
        (not
            (exists (?S2)
                (and
                    (instance ?S2 AutomobileShock)
                    (part ?S2 ?A2))))
        (dampingRatio ?A1 ?R1)
        (dampingRatio ?A2 ?R2))
    (greaterThan ?R2 ?R1))		 Cars.kif 853-866 If All of the following hold: (1) X is an instance of automobile (2) Y is an instance of automobile (3) Z is an instance of shock (4) Z is a part of X (5) there doesn't exist W such that W is an instance of shock and W is a part of Y (6) the damping ratio of X is V (7) the damping ratio of Y is U, then U is greater than V
(=>
    (and
        (typicalTemporalPart ?PART ?WHOLE)
        (instance ?X ?PART)
        (equal ?PARTPROB
            (ProbabilityFn
                (exists (?Y)
                    (and
                        (instance ?Y ?WHOLE)
                        (temporalPart ?X ?Y)))))
        (equal ?NOTPARTPROB
            (ProbabilityFn
                (not
                    (exists (?Z)
                        (and
                            (instance ?Z ?WHOLE)
                            (temporalPart ?X ?Z)))))))
    (greaterThan ?PARTPROB ?NOTPARTPROB))		 Cars.kif 1453-1470 If a X is typically a part of a Y, Z is an instance of X, equal W, the probability of there exists V such that V is an instance of Y, and Z is a part of V, and equal U, the probability of there doesn't exist T such that T is an instance of Y, and Z is a part of T, then W is greater than U
(=>
    (and
        (typicallyContainsTemporalPart ?PART ?WHOLE)
        (instance ?Y ?WHOLE)
        (equal ?PARTPROB
            (ProbabilityFn
                (exists (?X1)
                    (and
                        (instance ?X1 ?PART)
                        (temporalPart ?X1 ?Y)))))
        (equal ?NOTPARTPROB
            (ProbabilityFn
                (not
                    (exists (?X2)
                        (and
                            (instance ?X2 ?PART)
                            (temporalPart ?X2 ?Y)))))))
    (greaterThan ?PARTPROB ?NOTPARTPROB))		 Cars.kif 1493-1510 If a X typically contains a Y, Z is an instance of X, equal W, the probability of there exists V such that V is an instance of Y, and V is a part of Z, and equal U, the probability of there doesn't exist T such that T is an instance of Y, and T is a part of Z, then W is greater than U
(=>
    (and
        (instance ?SH1 Shaft)
        (instance ?SH2 Shaft)
        (not
            (equal ?SH1 ?SH2))
        (instance ?R1 Rotating)
        (patient ?R1 ?SH1)
        (instance ?R2 Rotating)
        (patient ?R2 ?SH2)
        (causes ?R1 ?R2)
        (equal
            (WhenFn ?R1)
            (WhenFn ?R2))
        (instance ?CV CVJoint)
        (connectedEngineeringComponents ?SH1 ?CV)
        (connectedEngineeringComponents ?SH2 ?CV)
        (holdsDuring
            (WhenFn ?R1)
            (equal
                (MeasureFn ?N RevolutionsPerMinute)
                (RotationFn ?R1))))
    (holdsDuring
        (WhenFn ?R2)
        (equal
            (MeasureFn ?N RevolutionsPerMinute)
            (RotationFn ?R2))))		 Cars.kif 2097-2123 If All of the following hold: (1) X is an instance of shaft (2) Y is an instance of shaft (3) equal X and Y (4) Z is an instance of rotating (5) X is a patient of Z (6) W is an instance of rotating (7) Y is a patient of W (8) Z causes W (9) equal the time of existence of Z and the time of existence of W (10) V is an instance of C.V. joint (11) X is connected to V (12) Y is connected to V (13) equal U revolutions per minute(s) and the rotation of Z during holds during the time of existence of Z, then equal U revolutions per minute(s) and the rotation of W during holds during the time of existence of W
(=>
    (and
        (instance ?AT AutomobileTransmission)
        (instance ?C Crankshaft)
        (instance ?D Driveshaft)
        (instance ?A Automobile)
        (part ?D ?A)
        (part ?AT ?A)
        (part ?C ?A)
        (connectedEngineeringComponents ?C ?AT)
        (connectedEngineeringComponents ?D ?AT)
        (instance ?G1 Gear)
        (instance ?G2 Gear)
        (part ?G1 ?AT)
        (part ?G2 ?AT)
        (instance ?CR1 Rotating)
        (instance ?CR2 Rotating)
        (instance ?GR1 Rotating)
        (instance ?GR2 Rotating)
        (instance ?DR1 Rotating)
        (instance ?DR2 Rotating)
        (moves ?CR1 ?C)
        (moves ?CR2 ?C)
        (moves ?GR1 ?G1)
        (moves ?GR2 ?G2)
        (moves ?DR1 ?D)
        (moves ?DR2 ?D)
        (causes ?CR1 ?GR1)
        (causes ?GR1 ?DR1)
        (causes ?CR2 ?GR2)
        (causes ?GR2 ?DR2)
        (not
            (equal ?CR1 ?CR2))
        (not
            (equal ?G1 ?G2))
        (equal
            (MeasureFn ?NR1 RevolutionsPerMinute)
            (RotationFn ?CR1))
        (equal
            (MeasureFn ?NR2 RevolutionsPerMinute)
            (RotationFn ?CR2))
        (equal
            (MeasureFn ?ND1 RevolutionsPerMinute)
            (RotationFn ?DR1))
        (equal
            (MeasureFn ?ND2 RevolutionsPerMinute)
            (RotationFn ?DR2))
        (equal ?NR1 ?NR2))
    (not
        (equal ?ND1 ?ND2)))		 Cars.kif 2336-2377 If All of the following hold: (1) X is an instance of transmission (2) Y is an instance of crankshaft (3) Z is an instance of driveshaft (4) W is an instance of automobile (5) Z is a part of W (6) X is a part of W (7) Y is a part of W (8) Y is connected to X (9) Z is connected to X (10) V is an instance of gear (11) U is an instance of gear (12) V is a part of X (13) U is a part of X (14) T is an instance of rotating (15) S is an instance of rotating (16) R is an instance of rotating (17) Q is an instance of rotating (18) P is an instance of rotating (19) O is an instance of rotating (20) Y moves during T (21) Y moves during S (22) V moves during R (23) U moves during Q (24) Z moves during P (25) Z moves during O (26) T causes R (27) R causes P (28) S causes Q (29) Q causes O (30) equal T and S (31) equal V and U (32) equal N revolutions per minute(s) and the rotation of T during (33) equal M revolutions per minute(s) and the rotation of S during (34) equal L revolutions per minute(s) and the rotation of P during (35) equal K revolutions per minute(s) and the rotation of O during (36) equal N and M, then equal L and K
(=>
    (and
        (instance ?EM Electromagnet)
        (not
            (holdsDuring ?T1
                (exists (?T ?E)
                    (and
                        (instance ?T Transfer)
                        (instance ?E Electricity)
                        (objectTransferred ?T ?E)
                        (path ?T ?EM))))))
    (not
        (holdsDuring ?T1
            (exists (?M)
                (and
                    (instance ?M Magnetism)
                    (instrument ?M ?EM))))))		 Cars.kif 3983-3999 If X is an instance of electromagnet and there don't exist Y, Z such that Y is an instance of transfer, Z is an instance of electricity, the object transferred in Y is Z, and X is path along which Y occurs doesn't hold during W, then there doesn't exist V such that V is an instance of magnetism and X is an instrument for V doesn't hold during W
(=>
    (and
        (instance ?BTS BimetalTemperatureSensor)
        (instance ?M1 Metal)
        (instance ?M2 Metal)
        (not
            (equal ?M1 ?M2))
        (part ?M1 ?BTS)
        (part ?M2 ?BTS)
        (instance ?T1 TemperatureMeasure)
        (instance ?T2 TemperatureMeasure)
        (instance ?L1 LengthMeasure)
        (instance ?L2 LengthMeasure)
        (instance ?L3 LengthMeasure)
        (instance ?L4 LengthMeasure)
        (not
            (equal ?T1 ?T2))
        (not
            (equal ?TM1 ?TM2))
        (holdsDuring ?TM1
            (and
                (measure ?BTS ?T1)
                (measure ?M1 ?L1)
                (measure ?M2 ?L2)))
        (holdsDuring ?TM2
            (and
                (measure ?BTS ?T2)
                (measure ?M1 ?L3)
                (measure ?M2 ?L4))))
    (not
        (equal
            (DivisionFn ?L1 ?L2)
            (DivisionFn ?L3 ?L4))))		 Cars.kif 4159-4191 If All of the following hold: (1) X is an instance of bi_metal temperature sensor (2) Y is an instance of metal (3) Z is an instance of metal (4) equal Y and Z (5) Y is a part of X (6) Z is a part of X (7) W is an instance of temperature measure (8) V is an instance of temperature measure (9) U is an instance of length measure (10) T is an instance of length measure (11) S is an instance of length measure (12) R is an instance of length measure (13) equal W and V (14) equal Q and P (15) the measure of X is W, the measure of Y is U, and the measure of Z is T holds during Q (16) the measure of X is V, the measure of Y is S, and the measure of Z is R holds during P, then equal U, T, S, and R
(=>
    (and
        (instance ?R Ratchet)
        (instance ?A AttachingDevice)
        (instance ?RO1 Rotating)
        (attribute ?RO1 ?DIR1)
        (instance ?RO2 Rotating)
        (attribute ?RO2 ?DIR2)
        (instance ?DIR1 RotationalAttribute)
        (instance ?DIR2 RotationalAttribute)
        (not
            (equal ?RO1 ?RO2))
        (causes ?RO1 ?RO2)
        (patient ?RO1 Ratchet)
        (patient ?RO2 ?A))
    (equal ?DIR1 ?DIR2))		 Cars.kif 5005-5020 If All of the following hold: (1) X is an instance of ratchet (2) Y is an instance of attaching device (3) Z is an instance of rotating (4) W is an attribute of Z (5) V is an instance of rotating (6) U is an attribute of V (7) W is an instance of rotational attribute (8) U is an instance of rotational attribute (9) equal Z and V (10) Z causes V (11) ratchet is a patient of Z (12) Y is a patient of V, then equal W and U
(=>
    (and
        (instance ?WINDOW InterfaceWindow)
        (instance ?GUIE GUIElement)
        (screenOfGUIE ?WINDOW ?SCREEN)
        (screenOfGUIE ?GUIE ?SCREEN)
        (not
            (instance ?GUIE InterfaceWindow))
        (hasGUEState ?WINDOW GUE_ActiveState)
        (hasGUEState ?GUIE GUE_ActiveState))
    (properPart ?GUIE ?WINDOW))		 ComputerInput.kif 1920-1929 If All of the following hold: (1) X is an instance of interface window (2) Y is an instance of GUI element (3) X is displayed on Z (4) Y is displayed on Z (5) Y is not an instance of interface window (6) X has state GUE active state (7) Y has state GUE active state, then Y is a proper part of X
(=>
    (and
        (instance ?GUIE1 GUIElement)
        (instance ?GUIE2 GUIElement)
        (not
            (instance ?GUIE1 InterfaceWindow))
        (not
            (instance ?GUIE2 InterfaceWindow))
        (screenOfGUIE ?GUIE1 ?SCREEN)
        (screenOfGUIE ?GUIE2 ?SCREEN)
        (hasGUEState ?GUIE1 GUE_ActiveState)
        (hasGUEState ?GUIE2 GUE_ActiveState))
    (or
        (properPart ?GUIE1 ?GUIE2)
        (properPart ?GUIE2 ?GUIE1)
        (equal ?GUIE1 ?GUIE2)))		 ComputerInput.kif 1935-1948 If All of the following hold: (1) X is an instance of GUI element (2) Y is an instance of GUI element (3) X is not an instance of interface window (4) Y is not an instance of interface window (5) X is displayed on Z (6) Y is displayed on Z (7) X has state GUE active state (8) Y has state GUE active state, then At least one of the following holds: (1) X is a proper part of Y (2) Y is a proper part of X (3) equal X and Y
(=>
    (and
        (instance ?WINDOW_A InterfaceWindow)
        (instance ?WINDOW_P InterfaceWindow)
        (screenOfGUIE ?WINDOW_A ?SCREEN)
        (screenOfGUIE ?WINDOW_P ?SCREEN)
        (hasGUEState ?WINDOW_A GUE_ActiveState)
        (not
            (equal ?WINDOW_A ?WINDOW_P)))
    (hasGUEState ?WINDOW_P GUE_PassiveState))		 ComputerInput.kif 1964-1972 If All of the following hold: (1) ?WINDOW_A is an instance of interface window (2) ?WINDOW_P is an instance of interface window (3) ?WINDOW_A is displayed on Y (4) ?WINDOW_P is displayed on Y (5) ?WINDOW_A has state GUE active state (6) equal ?WINDOW_A and ?WINDOW_P, then ?WINDOW_P has state GUE passive state
(=>
    (and
        (hasGUEState ?WIN1 GUE_UncoveredState)
        (hasGUEState ?WIN1 GUE_MaximizedWindowState)
        (screenOfGUIE ?WIN1 ?SCREEN)
        (instance ?WIN2 InterfaceWindow)
        (screenOfGUIE ?WIN2 ?SCREEN)
        (not
            (equal ?WIN1 ?WIN2)))
    (or
        (hasGUEState ?WIN2 GUE_CoveredState)
        (hasGUEState ?WIN2 GUE_PartiallyCoveredState)
        (hasGUEState ?WIN2 GUE_OffscreenState)))		 ComputerInput.kif 2120-2131 If All of the following hold: (1) X has state GUE uncovered state (2) X has state GUE maximized window state (3) X is displayed on Y (4) Z is an instance of interface window (5) Z is displayed on Y (6) equal X and Z, then At least one of the following holds: (1) Z has state GUE covered state (2) Z has state GUE partially covered state (3) Z has state GUE offscreen state
(=>
    (and
        (instance ?CC ComputerCable)
        (not
            (instance ?C Cable))
        (part ?C ?CC))
    (or
        (instance ?C MaleConnector)
        (instance ?C FemaleConnector)))		 ComputingBrands.kif 2657-2665 If X is an instance of cable, Y is not an instance of cable, and Y is a part of X, then Y is an instance of å…¬ or Y is an instance of female
(=>
    (and
        (measure ?P1
            (MeasureFn ?N1 Lumen))
        (measure ?P2
            (MeasureFn ?N2 Lumen))
        (part ?P1 ?O)
        (part ?P2 ?O)
        (not
            (equal ?P1 ?P2))
        (greaterThan ?N1 ?N2)
        (equal
            (DivisionFn ?N1 ?N2) ?R)
        (contrastRatio ?O ?R))
    (not
        (exists (?P3 ?P4 ?N3 ?N4)
            (and
                (measure ?P3
                    (MeasureFn ?N3 Lumen))
                (measure ?P4
                    (MeasureFn ?N4 Lumen))
                (part ?P3 ?O)
                (part ?P4 ?O)
                (not
                    (equal ?P3 ?P4))
                (greaterThan ?N3 ?N4)
                (greaterThan
                    (DivisionFn ?N3 ?N4) ?R)))))		 ComputingBrands.kif 3641-3662 If All of the following hold: (1) the measure of X is Y lumen(s) (2) the measure of Z is W lumen(s) (3) X is a part of V (4) Z is a part of V (5) equal X and Z (6) Y is greater than W (7) equal Y, W, and U (8) the contrast ratio of V is U, then there don't exist T, S,, , R and Q such that the measure of T is R lumen(s) and the measure of S is Q lumen(s) and T is a part of V and S is a part of V and equal T and S and R is greater than Q and R and Q is greater than U
(=>
    (and
        (hasAccount ?U ?AC)
        (password ?P ?AC)
        (deviceAccount ?AC ?D)
        (not
            (knows ?U
                (password ?P ?AC)))
        (knows ?U
            (recoveryKey ?S ?AC))
        (possesses ?U ?D))
    (modalAttribute
        (exists (?C)
            (and
                (instance ?C ChangingPassword)
                (patient ?C ?AC)
                (agent ?C ?U))) Possibility))		 ComputingBrands.kif 4333-4350 If All of the following hold: (1) X has account Y (2) Y has password Z (3) device account Y and W (4) X doesn't know Y has password Z (5) X knows the account Y has recovery key V (6) X possesses W, then the statement there exists U such that U is an instance of change password, Y is a patient of U, and X is an agent of U has the modal force of possibility
(=>
    (and
        (instance ?CITY AmericanCity)
        (part ?CITY California)
        (not
            (equal ?CITY LosAngelesCalifornia)))
    (greaterThan
        (CardinalityFn
            (ResidentFn LosAngelesCalifornia))
        (CardinalityFn
            (ResidentFn ?CITY))))		 CountriesAndRegions.kif 812-817 If X is an instance of american city, X is a part of california, and equal X and los angeles california, then the number of instances in the resident of los angeles california is greater than the number of instances in the resident of X
(=>
    (and
        (instance ?UNIT AreaMeasure)
        (measure Alaska
            (MeasureFn ?NUMBER1 ?UNIT))
        (measure ?STATE
            (MeasureFn ?NUMBER2 ?UNIT))
        (instance ?STATE AmericanState)
        (not
            (equal Alaska ?STATE)))
    (lessThan ?NUMBER2 ?NUMBER1))		 CountriesAndRegions.kif 871-878 If X is an instance of area measure, the measure of alaska is Y X(s), the measure of Z is W X(s), Z is an instance of american state, and equal alaska and Z, then W is less than Y
(=>
    (and
        (instance ?STATE AmericanState)
        (not
            (equal ?STATE California)))
    (greaterThan
        (CardinalityFn
            (ResidentFn California))
        (CardinalityFn
            (ResidentFn ?STATE))))		 CountriesAndRegions.kif 897-901 If X is an instance of american state and equal X and california, then the number of instances in the resident of california is greater than the number of instances in the resident of X
(=>
    (and
        (customer ?CUST ?AGENT)
        (corkageFee ?AMT ?ITEM ?AGENT)
        (instance ?X ?ITEM)
        (not
            (exists (?B)
                (and
                    (instance ?B Buying)
                    (patient ?B ?X)
                    (destination ?B ?CUST)
                    (origin ?B ?AGENT))))
        (instance ?D Drinking)
        (agent ?D ?CUST)
        (resource ?D ?X))
    (exists (?C)
        (and
            (instance ?C Corkage)
            (agent ?C ?CUST)
            (refers ?C ?X)
            (destination ?C ?AGENT))))		 Dining.kif 130-150 If All of the following hold: (1) X is a customer of Y (2) X charges Z in corkage for W (3) V is an instance of W (4) there doesn't exist U such that U is an instance of buying, V is a patient of U, U ends up at Y, and U originates at X (5) T is an instance of drinking (6) Y is an agent of T (7) V is a resource for T, then there exists S such that S is an instance of corkage, Y is an agent of S, S includes a reference to V, and S ends up at X

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 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
(=>
    (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
        (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
        (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
(=>
    (and
        (holdsDuring ?T
            (and
                (attribute ?H LateralRecumbant)
                (orientation ?H ?O On)))
        (instance ?LA LeftArm)
        (part ?LA ?H)
        (instance ?RA RightArm)
        (part ?RA ?H)
        (instance ?LL LeftLeg)
        (part ?LL ?H)
        (instance ?RL RightLeg)
        (part ?RL ?H)
        (or
            (meetsSpatially ?LA ?O)
            (meetsSpatially ?LL ?O)))
    (holdsDuring ?T
        (and
            (not
                (meetsSpatially ?RA ?O))
            (not
                (meetsSpatially ?RL ?O)))))		 Anatomy.kif 1871-1893 If All of the following hold: (1) lateral recumbant is an attribute of X and X is on to Y holds during Z (2) W is an instance of left arm (3) W is a part of X (4) V is an instance of right arm (5) V is a part of X (6) U is an instance of left leg (7) U is a part of X (8) T is an instance of right leg (9) T is a part of X (10) W meets Y or U meets Y, then V doesn't meet Y and T doesn't meet Y holds during Z
(=>
    (and
        (holdsDuring ?T
            (and
                (attribute ?H LateralRecumbant)
                (orientation ?H ?O On)))
        (instance ?LA LeftArm)
        (part ?LA ?H)
        (instance ?RA RightArm)
        (part ?RA ?H)
        (instance ?LL LeftLeg)
        (part ?LL ?H)
        (instance ?RL RightLeg)
        (part ?RL ?H)
        (or
            (meetsSpatially ?RA ?O)
            (meetsSpatially ?RL ?O)))
    (holdsDuring ?T
        (and
            (not
                (meetsSpatially ?LA ?O))
            (not
                (meetsSpatially ?LL ?O)))))		 Anatomy.kif 1895-1917 If All of the following hold: (1) lateral recumbant is an attribute of X and X is on to Y holds during Z (2) W is an instance of left arm (3) W is a part of X (4) V is an instance of right arm (5) V is a part of X (6) U is an instance of left leg (7) U is a part of X (8) T is an instance of right leg (9) T is a part of X (10) V meets Y or T meets Y, then W doesn't meet Y and U doesn't meet Y holds during Z
(=>
    (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 ?MS MuakharSadaq)
    (exists (?H ?W ?T1 ?T2)
        (and
            (agent ?MS ?H)
            (origin ?MS ?H)
            (destination ?MS ?W)
            (holdsDuring ?T1
                (wife ?W ?H))
            (not
                (holdsDuring ?T2
                    (wife ?W ?H)))
            (finishes ?T1 ?MS)
            (before ?T1 ?T2)
            (starts ?T2 ?MS))))		 ArabicCulture.kif 285-299 If X is an instance of muakhar sadaq, then All of the following hold: (1) there exist Y, Z,, , W (2) V such that Y is an agent of X (3) X originates at Y (4) X ends up at Z (5) Z is the wife of Y holds during W (6) Z is the wife of Y doesn't hold during V (7) W finishes X (8) W happens before V (9) V starts X
(=>
    (instance ?MS MuqaddamSadaq)
    (exists (?H ?W ?T1 ?T2)
        (and
            (agent ?MS ?H)
            (origin ?MS ?H)
            (destination ?MS ?W)
            (not
                (holdsDuring ?T1
                    (wife ?W ?H)))
            (holdsDuring ?T2
                (wife ?W ?H))
            (finishes ?T1 ?MS)
            (before ?T1 ?T2)
            (starts ?T2 ?MS))))		 ArabicCulture.kif 305-319 If X is an instance of muqaddam sadaq, then All of the following hold: (1) there exist Y, Z,, , W (2) V such that Y is an agent of X (3) X originates at Y (4) X ends up at Z (5) Z is the wife of Y doesn't hold during W (6) Z is the wife of Y holds during V (7) W finishes X (8) W happens before V (9) V starts X
(=>
    (instance ?TEXT MarriageCertificate)
    (exists (?S ?W ?A ?B)
        (and
            (instance ?S SigningAnAgreement)
            (patient ?S ?TEXT)
            (instance ?W Wedding)
            (represents ?TEXT ?W)
            (subProcess ?S ?W)
            (patient ?W ?A)
            (instance ?A Human)
            (patient ?W ?B)
            (instance ?B Human)
            (not
                (equal ?A ?B))
            (agent ?S ?A)
            (agent ?S ?B))))		 Biography.kif 327-343 If X is an instance of marriage certificate, then All of the following hold: (1) there exist Y, Z,, , W (2) V such that Y is an instance of signing an agreement (3) X is a patient of Y (4) Z is an instance of wedding (5) X expresses Z (6) Y is a subprocess of Z (7) W is a patient of Z (8) W is an instance of human (9) V is a patient of Z (10) V is an instance of human (11) equal W (12) V (13) W is an agent of Y (14) V is an agent of Y
(=>
    (and
        (attribute ?ACTOR VoiceActor)
        (instance ?DRAMA DramaticActing)
        (agent ?DRAMA ?ACTOR)
        (instance ?SPEAK LinguisticCommunication)
        (agent ?SPEAK ?ACTOR)
        (subProcess ?SPEAK ?DRAMA))
    (and
        (not
            (exists (?S ?VIEWER)
                (and
                    (instance ?S Seeing)
                    (patient ?S ?ACTOR)
                    (agent ?S ?VIEWER))))
        (exists (?H ?VIEWER)
            (and
                (instance ?H Hearing)
                (patient ?H ?ACTOR)
                (agent ?H ?VIEWER)))))		 Biography.kif 765-784 If All of the following hold: (1) voice actor is an attribute of X (2) Y is an instance of dramatic acting (3) X is an agent of Y (4) Z is an instance of linguistic communication (5) X is an agent of Z (6) Z is a subprocess of Y, then there don't exist W, V such that W is an instance of seeing, X is a patient of W, and V is an agent of W and there exist U, V such that U is an instance of hearing, X is a patient of U, and V is an agent of U
(=>
    (and
        (instance ?X Region)
        (attribute ?X Vacuum))
    (not
        (exists (?O)
            (and
                (instance ?O Object)
                (located ?O ?X)))))		 Cars.kif 368-376 If X is an instance of region and vacuum is an attribute of X, then there doesn't exist Y such that Y is an instance of object and Y is located at X
(=>
    (attribute ?X PartialVacuum)
    (exists (?O ?G ?P1 ?P2 ?PM)
        (and
            (instance ?O SelfConnectedObject)
            (instance ?G Region)
            (not
                (equal ?G ?X))
            (connected ?X ?O)
            (connected ?G ?O)
            (measure ?G
                (MeasureFn ?P1 ?PM))
            (measure ?X
                (MeasureFn ?P2 ?PM))
            (instance ?PM UnitOfAtmosphericPressure)
            (greaterThan ?P1 ?P2))))		 Cars.kif 383-396 If partial vacuum is an attribute of X, then there exist Y, Z,, , W,, , V and U such that Y is an instance of self connected object and Z is an instance of region and equal Z and X and X is connected to Y and Z is connected to Y and the measure of Z is W U(s) and the measure of X is V U(s) and U is an instance of unit of atmospheric pressure and W is greater than V
(=>
    (attribute ?X Pressurized)
    (exists (?O ?G ?P1 ?P2 ?PM)
        (and
            (instance ?O SelfConnectedObject)
            (instance ?G Region)
            (not
                (equal ?G ?X))
            (connected ?X ?O)
            (connected ?G ?O)
            (measure ?G
                (MeasureFn ?P1 ?PM))
            (measure ?X
                (MeasureFn ?P2 ?PM))
            (instance ?PM UnitOfAtmosphericPressure)
            (greaterThan ?P2 ?P1))))		 Cars.kif 403-416 If pressurized is an attribute of X, then there exist Y, Z,, , W,, , V and U such that Y is an instance of self connected object and Z is an instance of region and equal Z and X and X is connected to Y and Z is connected to Y and the measure of Z is W U(s) and the measure of X is V U(s) and U is an instance of unit of atmospheric pressure and V is greater than W
(=>
    (and
        (instance ?P ParkingBrake)
        (instance ?V Vehicle)
        (holdsDuring ?T1
            (attribute ?P DeviceOn))
        (part ?P ?V))
    (hasPurpose ?P
        (holdsDuring ?T1
            (not
                (exists (?T)
                    (and
                        (instance ?T Translocation)
                        (patient ?T ?V)))))))		 Cars.kif 567-580 If X is an instance of parking brake, Y is an instance of vehicle, device on is an attribute of X holds during Z, and X is a part of Y, then X has the purpose there doesn't exist W such that W is an instance of translocation and Y is a patient of W holds during Z
(=>
    (and
        (instance ?BP BrakePad)
        (instance ?BR BrakeRotor)
        (instance ?R Rotating)
        (patient ?R ?BR)
        (instance ?F Friction)
        (resource ?F ?BP)
        (patient ?F ?BR))
    (not
        (patient ?R ?BP)))		 Cars.kif 617-627 If All of the following hold: (1) X is an instance of brake pad (2) Y is an instance of brake rotor (3) Z is an instance of rotating (4) Y is a patient of Z (5) W is an instance of friction (6) X is a resource for W (7) Y is a patient of W, then X is not a patient of Z
(=>
    (and
        (instance ?BS BrakeShoe)
        (instance ?BD BrakeDrum)
        (instance ?R Rotating)
        (patient ?R ?BD)
        (instance ?F Friction)
        (resource ?F ?BS)
        (patient ?F ?BD))
    (not
        (patient ?R ?BS)))		 Cars.kif 639-649 If All of the following hold: (1) X is an instance of brake shoe (2) Y is an instance of brake drum (3) Z is an instance of rotating (4) Y is a patient of Z (5) W is an instance of friction (6) X is a resource for W (7) Y is a patient of W, then X is not a patient of Z
(=>
    (and
        (physicalAmplitude ?T
            (MeasureFn ?L ?U))
        (instance ?U UnitOfLength)
        (patient ?T ?O))
    (not
        (exists (?P1 ?P2 ?T1 ?T2 ?L2)
            (and
                (during ?T1
                    (WhenFn ?T))
                (during ?T2
                    (WhenFn ?T))
                (holdsDuring ?T1
                    (located ?O ?P1))
                (holdsDuring ?T2
                    (located ?O ?P2))
                (distance ?P1 ?P2
                    (MeasureFn ?L2 ?U))
                (greaterThan ?L2 ?L)))))		 Cars.kif 751-768 If the amplitude X is Y Z(s), Z is an instance of unit of length, and W is a patient of X, then there don't exist V, U,, , T,, , S and R such that T takes place during the time of existence of X and S takes place during the time of existence of X and W is located at V holds during T and W is located at U holds during S and the distance between V and U is R Z(s) and R is greater than Y

Display limited to 25 items. Show next 25

Display limited to 25 items. Show next 25

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


(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
(forall (?A ?COURSE)
    (not
        (classmate ?A ?A ?COURSE)))		 Mid-level-ontology.kif 18368-18369 For all Human X and EducationalCourse Y: X and X were taught in the same EducationalProcess Y together
(forall (?A ?ORG)
    (not
        (colleague ?A ?A ?ORG)))		 Mid-level-ontology.kif 18387-18388 For all Human X and Organization Y: X and X were employs by the same organization Y

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


(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 }
(not
    (vegetationType ArcticRegion BotanicalTree))		 Geography.kif 5040-5040 Botanical tree is found in arctic region
(not
    (equal BigSix GroupOf6))		 Government.kif 2896-2896 equal big six and group of6
(not
    (member Denmark EuropeanMonetaryUnion))		 Government.kif 3200-3200 Denmark is not a member of european monetary union
(not
    (member Sweden EuropeanMonetaryUnion))		 Government.kif 3201-3201 Sweden is not a member of european monetary union
(not
    (member UnitedKingdom EuropeanMonetaryUnion))		 Government.kif 3202-3202 United kingdom is not a member of european monetary union
(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
(not
    (overlapsTemporally CommonEra BeforeCommonEra))		 Mid-level-ontology.kif 9098-9098 Before common era doesn't overlap common era


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