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



KB Term:  Term intersection
English Word: 

Sigma KEE - exists
exists

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


(=>
    (and
        (instance ?GUN Gun)
        (instance ?U UnitOfLength)
        (effectiveRange ?GUN
            (MeasureFn ?LM ?U))
        (distance ?GUN ?O
            (MeasureFn ?LM1 ?U))
        (not
            (exists (?O2)
                (between ?O ?O2 ?GUN)))
        (lessThanOrEqualTo ?LM1 ?LM))
    (exists (?DAMAGING)
        (capability
            (KappaFn ?DAMAGING
                (and
                    (instance ?DAMAGING Damaging)
                    (patient ?DAMAGING ?O))) instrument ?GUN)))
Mid-level-ontology.kif 1662-1680 If All of the following hold: (1) X is an instance of gun (2) Y is an instance of unit of length (3) Z Y(s) is an effective range of X (4) the distance between X and W is V Y(s) (5) there doesn't exist U such that U is between W and X (6) V is less than or equal to Z, then there exists T such that X is capable of doing the class described by T as a instrument
(=>
    (and
        (instance ?GUN Gun)
        (instance ?U UnitOfLength)
        (effectiveRange ?GUN
            (MeasureFn ?LM ?U))
        (distance ?GUN ?O
            (MeasureFn ?LM1 ?U))
        (instance ?O Organism)
        (not
            (exists (?O2)
                (between ?O ?O2 ?GUN)))
        (lessThanOrEqualTo ?LM1 ?LM))
    (exists (?KILLING)
        (capability
            (KappaFn ?KILLING
                (and
                    (instance ?KILLING Killing)
                    (patient ?KILLING ?O))) instrument ?GUN)))
Mid-level-ontology.kif 1684-1703 If All of the following hold: (1) X is an instance of gun (2) Y is an instance of unit of length (3) Z Y(s) is an effective range of X (4) the distance between X and W is V Y(s) (5) W is an instance of organism (6) there doesn't exist U such that U is between W and X (7) V is less than or equal to Z, then there exists T such that X is capable of doing the class described by T as a instrument
(=>
    (and
        (instance ?B Bubble)
        (not
            (exists (?X ?S)
                (and
                    (attribute ?X ?S)
                    (not
                        (equal ?X Gas))
                    (meetsSpatially ?X ?B)))))
    (attribute ?B ConvexRoundShape))
Mid-level-ontology.kif 6111-6120 If X is an instance of bubble and there don't exist Y, Z such that Z is an attribute of Y, equal Y, gas, and Y meets X, then convex round shape is an attribute of X
(=>
    (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))
Mid-level-ontology.kif 25115-25132 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
        (typicalAction ?PROCESS ?AGENT)
        (instance ?A ?AGENT)
        (equal ?PPROB
            (ProbabilityFn
                (exists (?X)
                    (and
                        (instance ?X ?PROCESS)
                        (agent ?X ?A)))))
        (equal ?NOTPPROB
            (ProbabilityFn
                (not
                    (exists (?Y)
                        (and
                            (instance ?Y ?PROCESS)
                            (agent ?Y ?A)))))))
    (greaterThan ?PPROB ?NOTPPROB))
Mid-level-ontology.kif 25150-25167 If X is a typical action of a Y, Z is an instance of Y, equal W, the probability of there exists V such that V is an instance of X, and Z is an agent of V, and equal U, the probability of there doesn't exist T such that T is an instance of X, and Z is an agent of T, then W is greater than U
(=>
    (and
        (typicalPart ?PART ?WHOLE)
        (instance ?X ?PART)
        (equal ?PARTPROB
            (ProbabilityFn
                (exists (?Y)
                    (and
                        (instance ?Y ?WHOLE)
                        (part ?X ?Y)))))
        (equal ?NOTPARTPROB
            (ProbabilityFn
                (not
                    (exists (?Z)
                        (and
                            (instance ?Z ?WHOLE)
                            (part ?X ?Z)))))))
    (greaterThan ?PARTPROB ?NOTPARTPROB))
Mid-level-ontology.kif 25958-25975 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
        (typicallyContainsPart ?PART ?WHOLE)
        (instance ?Y ?WHOLE)
        (equal ?PARTPROB
            (ProbabilityFn
                (exists (?X1)
                    (and
                        (instance ?X1 ?PART)
                        (part ?X1 ?Y)))))
        (equal ?NOTPARTPROB
            (ProbabilityFn
                (not
                    (exists (?X2)
                        (and
                            (instance ?X2 ?PART)
                            (part ?X2 ?Y)))))))
    (greaterThan ?PARTPROB ?NOTPARTPROB))
Mid-level-ontology.kif 25996-26013 If a X typically has a part 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
        (unitNumber ?UNITSTR ?PLACE)
        (not
            (exists (?FLR)
                (floorCode ?FLR ?PLACE))))
    (exists (?UNIT)
        (and
            (instance ?UNIT Room)
            (names ?UNITSTR ?UNIT)
            (located ?UNIT ?PLACE))))
Mid-level-ontology.kif 26927-26937 If the unit number of X is Y and there doesn't exist Z such that Z is the floor of X, then there exists W such that W is an instance of room, W has name Y, and W is located at X
(=>
    (holdsDuring ?T
        (and
            (not
                (exists (?C)
                    (and
                        (instance ?C Clothing)
                        (covers ?C ?F))))
            (instance ?F Foot)
            (part ?F ?A)))
    (holdsDuring ?T
        (attribute ?A Barefoot)))
Mid-level-ontology.kif 32753-32764 If there doesn't exist X such that X is an instance of clothing, X covers Y, Y is an instance of foot, and Y is a part of Z holds during W, then barefoot is an attribute of Z holds during W
(=>
    (holdsDuring ?T
        (not
            (exists (?C)
                (and
                    (instance ?C Clothing)
                    (wears ?A ?C)))))
    (holdsDuring ?T
        (attribute ?A Naked)))
Mid-level-ontology.kif 32779-32787 If there doesn't exist X such that X is an instance of clothing and Y wears X holds during Z, then naked is an attribute of Y holds during Z
(=>
    (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 790-803 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 1367-1384 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
        (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 3775-3791 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
        (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
(=>
    (and
        (facility ?AGENT ?OBJ)
        (customer ?CUST ?AGENT)
        (instance ?X ?OBJ)
        (desires ?CUST
            (exists (?PROC)
                (and
                    (instance ?PROC IntentionalProcess)
                    (patient ?PROC ?X)
                    (agent ?PROC ?CUST)))))
    (modalAttribute
        (confersRight ?AGENT ?CUST
            (uses ?X ?CUST)) Possibility))
Dining.kif 336-350 If X provides Y, X is a customer of Z, W is an instance of Y, and Z desires there exists V such that V is an instance of intentional process, W is a patient of V, and Z is an agent of V, then the statement Z allows Z uses W to perform task of the type X has the modal force of possibility
(=>
    (and
        (instance ?C CateringService)
        (agent ?C ?AGENT)
        (destination ?C ?CUST)
        (located ?AGENT ?LOC1)
        (customer ?CUST ?AGENT)
        (exists (?S ?FOOD ?E)
            (and
                (instance ?S Cooking)
                (agent ?S ?AGENT)
                (result ?S ?FOOD)
                (patient ?C ?FOOD)
                (instance ?E Eating)
                (agent ?E ?CUST)
                (eventLocated ?E ?LOC2))))
    (not
        (equal ?LOC1 ?LOC2)))
Dining.kif 586-602 If All of the following hold: (1) X is an instance of catering (2) Y is an agent of X (3) X ends up at Z (4) Y is located at W (5) Y is a customer of Z (6) All of the following hold: (1) there exist V, U (2) T such that V is an instance of cooking (3) Y is an agent of V (4) U is a result of V (5) U is a patient of X (6) T is an instance of eating (7) Z is an agent of T (8) T is located at S, then equal W and S
(=>
    (and
        (instance ?AGENT AutonomousAgent)
        (potentialCustomer ?CUST ?AGENT)
        (modalAttribute
            (and
                (instance ?R Reserving)
                (destination ?R ?AGENT)) Necessity)
        (conditionalProbability
            (exists (?RES1)
                (and
                    (instance ?RES1 Reservation)
                    (reservingEntity ?CUST ?RES1)
                    (fulfillingEntity ?AGENT ?RES1)))
            (customer ?CUST ?AGENT) ?NUM1)
        (conditionalProbability
            (not
                (exists (?RES2)
                    (and
                        (instance ?RES2 Reservation)
                        (reservingEntity ?CUST ?RES2)
                        (fulfillingEntity ?AGENT ?RES2))))
            (customer ?CUST ?AGENT) ?NUM2))
    (lessThan ?NUM2 ?NUM1))
Dining.kif 772-795 If X is an instance of agent, Y is a potential customer for X, the statement Z is an instance of reserving and Z ends up at X has the modal force of necessity, probability of there exists W such that W is an instance of reservation, Y reserves W, and X fulfills W provided that X is a customer of Y holds is V, and probability of there doesn't exist U such that U is an instance of reservation, Y reserves U, and X fulfills U provided that X is a customer of Y holds is T, then T is less than V
(<=>
    (exists (?Rate)
        (fixedInterestRate ?Account ?Rate))
    (instance ?Account FixedRateAccount))
FinancialOntology.kif 1003-1006 There exists X such that X is a fixed interest rate of Y if and only if Y is an instance of fixed rate account
(<=>
    (and
        (instance ?Withdrawal Withdrawal)
        (instance ?Account FinancialAccount)
        (origin ?Withdrawal
            (CurrencyFn ?Account))
        (not
            (exists (?Penalty)
                (and
                    (instance ?Penalty Penalty)
                    (destination ?Penalty
                        (CurrencyFn ?Account))
                    (causes ?Withdrawal ?Penalty)))))
    (liquidity ?Account HighLiquidity))
FinancialOntology.kif 1864-1874 All of the following hold: (1) X is an instance of withdrawing from an account (2) Y is an instance of financial account (3) X originates at the currency of Y (4) there doesn't exist Z such that Z is an instance of penalizing (5) Z ends up at the currency of Y (6) X causes Z if (7) only if the liqudity of Y is high liquidity
(<=>
    (exists (?Period)
        (and
            (instance ?Loan Loan)
            (agreementPeriod ?Loan ?Period)
            (interestEarned ?Loan ?Amount ?Period)))
    (loanInterest ?Loan ?Amount))
FinancialOntology.kif 3978-3984 There exists X such that Y is an instance of loan, X is an agreement period of Y, Y is interest earned Z for X if, and only if Z is a loan interest of Y
(=>
    (and
        (instance ?X Pasta)
        (not
            (exists (?Y)
                (and
                    (instance ?Y Pasta)
                    (part ?Y ?X)))))
    (attribute ?X LongAndThin))
Food.kif 2648-2656 If X is an instance of pasta and there doesn't exist Y such that Y is an instance of pasta and Y is a part of X, then long and thin is an attribute of X
(=>
    (and
        (instance ?X Penne)
        (not
            (exists (?Y)
                (and
                    (instance ?Y Penne)
                    (part ?Y ?X)))))
    (and
        (exists (?HOLE2)
            (and
                (instance ?HOLE2 HoleRegion)
                (part ?X ?HOLE2)))
        (attribute ?X Fillable)))
Food.kif 2792-2805 If X is an instance of penne and there doesn't exist Y such that Y is an instance of penne and Y is a part of X, then there exists Z such that Z is an instance of hole and X is a part of Z and fillable is an attribute of X
(=>
    (and
        (instance ?X Spaghetti)
        (not
            (exists (?Y)
                (and
                    (instance ?Y Spaghetti)
                    (part ?Y ?X)))))
    (attribute ?X LongAndThin))
Food.kif 3500-3508 If X is an instance of spaghetti and there doesn't exist Y such that Y is an instance of spaghetti and Y is a part of X, then long and thin is an attribute of X
(=>
    (and
        (instance ?A PointInSpace)
        (instance ?B PointInSpace)
        (located ?A RockyMountains)
        (located ?B RockyMountains)
        (orientation ?A ?B North)
        (not
            (exists (?A1 ?B1)
                (and
                    (instance ?A1 PointInSpace)
                    (located ?A1 RockyMountains)
                    (orientation ?A1 ?A North)
                    (instance ?B1 PointInSpace)
                    (located ?B1 RockyMountains)
                    (orientation ?B1 ?B South))))
        (distance ?A ?B
            (MeasureFn ?X Mile)))
    (approximateValue ?X 3000))
Geography.kif 377-395 If All of the following hold: (1) X is an instance of point in space (2) Y is an instance of point in space (3) X is located at Rocky Mountains (4) Y is located at Rocky Mountains (5) X is north of to Y (6) All of the following hold: (1) there don't exist Z (2) W such that Z is an instance of point in space (3) Z is located at Rocky Mountains (4) Z is north of to X (5) W is an instance of point in space (6) W is located at Rocky Mountains (7) W is south of to Y (7) the distance between X and Y is V mile(s), then the approximate value of V is 3000
(=>
    (and
        (instance ?A PointInSpace)
        (instance ?B PointInSpace)
        (located ?A RockyMountains)
        (located ?B RockyMountains)
        (orientation ?A ?B East)
        (not
            (exists (?A1 ?B1)
                (and
                    (instance ?A1 PointInSpace)
                    (located ?A1 RockyMountains)
                    (orientation ?A1 ?A East)
                    (instance ?B1 PointInSpace)
                    (located ?B1 RockyMountains)
                    (orientation ?B1 ?B West))))
        (distance ?A ?B
            (MeasureFn ?X Mile)))
    (and
        (greaterThan ?X 70)
        (greaterThan 300 ?X)))
Geography.kif 397-417 If All of the following hold: (1) X is an instance of point in space (2) Y is an instance of point in space (3) X is located at Rocky Mountains (4) Y is located at Rocky Mountains (5) X is east of to Y (6) All of the following hold: (1) there don't exist Z (2) W such that Z is an instance of point in space (3) Z is located at Rocky Mountains (4) Z is east of to X (5) W is an instance of point in space (6) W is located at Rocky Mountains (7) W is west of to Y (7) the distance between X and Y is V mile(s), then V is greater than 70 and 300 is greater than V

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
(=>
    (immediateSubclass ?CLASS1 ?CLASS2)
    (not
        (exists (?CLASS3)
            (and
                (subclass ?CLASS3 ?CLASS2)
                (subclass ?CLASS1 ?CLASS3)
                (not
                    (equal ?CLASS2 ?CLASS3))
                (not
                    (equal ?CLASS1 ?CLASS3))))))
Merge.kif 154-161 If X is an immediate subclass of Y, then there doesn't exist Z such that Z is a subclass of Y, X is a subclass of Z, equal Y, Z, equal X, and Z
(=>
    (disjoint ?CLASS1 ?CLASS2)
    (not
        (exists (?INST)
            (and
                (instance ?INST ?CLASS1)
                (instance ?INST ?CLASS2)))))
Merge.kif 393-399 If X is disjoint from Y, then there doesn't exist Z such that Z is an instance of X and Z is an instance of Y
(=>
    (exhaustiveAttribute ?CLASS @ROW)
    (forall (?ATTR1)
        (=>
            (instance ?ATTR1 ?CLASS)
            (exists (?ATTR2)
                (and
                    (inList ?ATTR2
                        (ListFn @ROW))
                    (equal ?ATTR1 ?ATTR2))))))
Merge.kif 501-509 If @ROW are all the attributes of Y, then For all Entity Z: if Z is an instance of Y, then there exists W such that W is a member of (@ROW) and equal Z and W
(=>
    (exhaustiveAttribute ?ATTRCLASS @ROW)
    (not
        (exists (?EL)
            (and
                (instance ?EL ?ATTRCLASS)
                (not
                    (exists (?ATTR ?NUMBER)
                        (and
                            (equal ?EL ?ATTR)
                            (equal ?ATTR
                                (ListOrderFn
                                    (ListFn @ROW) ?NUMBER)))))))))
Merge.kif 511-523 If @ROW are all the attributes of Y, then there doesn't exist Z such that Z is an instance of Y and there don't exist W and V such that equal Z and W and equal W and U element of (@ROW)
(=>
    (instance ?PHYS Physical)
    (exists (?LOC ?TIME)
        (and
            (located ?PHYS ?LOC)
            (time ?PHYS ?TIME))))
Merge.kif 831-836 If X is an instance of physical, then there exist Y, Z such that X is located at Y, and X exists during Z
(=>
    (instance ?event VolcanicEruption)
    (exists (?volcano)
        (and
            (instance ?volcano Volcano)
            (agent ?event ?volcano))))
Merge.kif 1030-1035 If X is an instance of volcanic eruption, then there exists Y such that Y is an instance of volcano and Y is an agent of X
(=>
    (instance ?ERUPTING VolcanicEruption)
    (exists (?VOLCANO)
        (and
            (instance ?VOLCANO Volcano)
            (eventLocated ?ERUPTING ?VOLCANO))))
Merge.kif 1041-1046 If X is an instance of volcanic eruption, then there exists Y such that Y is an instance of volcano and X is located at Y
(=>
    (instance ?ERUPTING VolcanicEruption)
    (exists (?HEATING)
        (and
            (instance ?HEATING Heating)
            (subProcess ?HEATING ?ERUPTING))))
Merge.kif 1048-1053 If X is an instance of volcanic eruption, then there exists Y such that Y is an instance of heating and Y is a subprocess of X
(=>
    (instance ?C Crater)
    (exists (?HOST ?EVENT ?METEOR ?BOMB)
        (and
            (hole ?C ?HOST)
            (superficialPart ?SURF
                (HoleHostFn ?C))
            (or
                (and
                    (instance ?EVENT Impacting)
                    (instrument ?EVENT ?METEOR)
                    (instance ?METEOR Meteorite))
                (and
                    (instance ?EVENT Explosion)
                    (instrument ?EVENT ?BOMB)
                    (instance ?BOMB Bomb))
                (instance ?EVENT VolcanicEruption))
            (result ?EVENT ?C))))
Merge.kif 1059-1075 If X is an instance of crater, then All of the following hold: (1) there exist Y, Z,, , W (2) V such that X is a hole in Y (3) U is a superficial part of the host of the hole X (4) Z is an instance of impacting (5) W is an instrument for Z (6) W is an instance of meteorite or Z is an instance of explosion (7) V is an instrument for Z (8) V is an instance of bomb or Z is an instance of volcanic eruption (9) X is a result of Z
(=>
    (contains ?OBJ1 ?OBJ2)
    (exists (?HOLE)
        (and
            (hole ?HOLE ?OBJ1)
            (properlyFills ?OBJ2 ?HOLE))))
Merge.kif 1101-1106 If X contains Y, then there exists Z such that Z is a hole in X and Y properly fills Z
(=>
    (instance ?SUBSTANCE SyntheticSubstance)
    (exists (?PROCESS)
        (and
            (instance ?PROCESS IntentionalProcess)
            (result ?PROCESS ?SUBSTANCE)
            (instance ?SUBSTANCE Substance))))
Merge.kif 1145-1151 If X is an instance of synthetic substance, then there exists Y such that Y is an instance of intentional process, X is a result of Y, and X is an instance of substance
(=>
    (instance ?ATOM Atom)
    (exists (?PROTON ?ELECTRON)
        (and
            (part ?PROTON ?ATOM)
            (part ?ELECTRON ?ATOM)
            (instance ?PROTON Proton)
            (instance ?ELECTRON Electron))))
Merge.kif 1186-1193 If X is an instance of atom, then there exist Y, Z such that Y is a part of X, Z is a part of X, Y is an instance of proton, and Z is an instance of electron
(=>
    (instance ?PARTICLE SubatomicParticle)
    (exists (?ATOM)
        (and
            (instance ?ATOM Atom)
            (component ?PARTICLE ?ATOM))))
Merge.kif 1211-1216 If X is an instance of subatomic particle, then there exists Y such that Y is an instance of atom and X is a component of Y
(=>
    (instance ?NUCLEUS AtomicNucleus)
    (exists (?NEUTRON ?PROTON)
        (and
            (component ?NEUTRON ?NUCLEUS)
            (component ?PROTON ?NUCLEUS)
            (instance ?NEUTRON Neutron)
            (instance ?PROTON Proton))))
Merge.kif 1222-1229 If X is an instance of atomic nucleus, then there exist Y, Z such that Y is a component of X, Z is a component of X, Y is an instance of neutron, and Z is an instance of proton
(=>
    (instance ?MIXTURE Mixture)
    (exists (?PURE1 ?PURE2)
        (and
            (instance ?PURE1 PureSubstance)
            (instance ?PURE2 PureSubstance)
            (not
                (equal ?PURE1 ?PURE2))
            (piece ?PURE1 ?MIXTURE)
            (piece ?PURE2 ?MIXTURE))))
Merge.kif 1263-1271 If X is an instance of mixture, then All of the following hold: (1) there exist Y (2) Z such that Y is an instance of pure substance (3) Z is an instance of pure substance (4) equal Y (5) Z (6) Y is a piece of X (7) Z is a piece of X
(=>
    (ingredient ?ING ?S)
    (exists (?PROC ?X ?Y)
        (and
            (instance ?PROC Process)
            (instance ?X ?ING)
            (patient ?PROC ?X)
            (instance ?Y ?S)
            (result ?PROC ?Y))))
Merge.kif 1289-1297 If X is an ingredient in Y, then there exist Z, W, V such that Z is an instance of process, W is an instance of X, W is a patient of Z, V is an instance of Y, and V is a result of Z
(=>
    (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 1304-1312 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 1345-1348 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 1401-1404 If X is an instance of content bearing physical, then there exists Y such that X expresses Y
(=>
    (instance ?STRING SymbolicString)
    (exists (?PART)
        (and
            (part ?PART ?STRING)
            (instance ?PART Character))))
Merge.kif 1437-1442 If X is an instance of symbolic string, then there exists Y such that Y is a part of X and Y is an instance of character
(=>
    (instance ?LANG ConstructedLanguage)
    (exists (?PLAN)
        (and
            (instance ?PLAN Planning)
            (result ?PLAN ?LANG))))
Merge.kif 1559-1564 If X is an instance of constructed language, then there exists Y such that Y is an instance of planning and X is a result of Y
(=>
    (instance ?W Writing)
    (exists (?S ?L)
        (and
            (instance ?S Text)
            (instance ?L WrittenHumanLanguage)
            (language ?S ?L))))
Merge.kif 1603-1609 If X is an instance of writing, then there exist Y, Z such that Y is an instance of text, Z is an instance of written human language, and Z is a Language of Y.
(=>
    (instance ?AGENT AutonomousAgent)
    (exists (?PROC)
        (capability ?PROC agent ?AGENT)))
Merge.kif 1656-1659 If X is an instance of agent, then there exists Y such that X is capable of doing Y as a agent
(=>
    (instance ?PROCESS DualObjectProcess)
    (exists (?OBJ1 ?OBJ2)
        (and
            (patient ?PROCESS ?OBJ1)
            (patient ?PROCESS ?OBJ2)
            (not
                (equal ?OBJ1 ?OBJ2)))))
Merge.kif 1731-1737 If X is an instance of dual object process, then there exist Y, Z such that Y is a patient of X, Z is a patient of X, equal Y, and Z

Display limited to 25 items. Show next 25

Display limited to 25 items. Show next 25

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


(not
    (exists (?PATH1 ?PATH2)
        (and
            (instance ?PATH1
                (CutSetFn ?GRAPH))
            (instance ?PATH2
                (MinimalCutSetFn ?GRAPH))
            (pathLength ?PATH1 ?NUMBER1)
            (pathLength ?PATH2 ?NUMBER2)
            (lessThan ?NUMBER1 ?NUMBER2))))
Merge.kif 6218-6225 There don't exist X, Y such that X is an instance of the set of paths that partition Z into two separate graphs, Y is an instance of the set of minimal paths that partition Z into two separate graphs, the length of X is W, the length of Y is V, and W is less than V
(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

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


(exists (?THING)
    (instance ?THING Entity))
Merge.kif 817-818 There exists X such that X is an instance of entity
(exists (?T)
    (and
        (subclass ?T HandToolBox)
        (manufacturer ?T SortimoCorp)))
Cars.kif 5001-5004 There exists X such that X is a subclass of tool box and the maker of X is Sortimo Corporation
(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
(exists (?MEAL ?REGION)
    (attribute ?MEAL
        (MealAttributeFn ?MEAL ?REGION)))
Food.kif 1915-1916 There exist X and Y such that the appropriate meal for X in Y is an attribute of X
(exists (?FORMULA)
    (and
        (instance ?FORMULA Formula)
        (containsFormula ImmigrationAndNationalityAct_US ?FORMULA)
        (modalAttribute ?FORMULA Law)))
Government.kif 2372-2376 There exists X such that X is an instance of formula, immigration and nationality act_US contains the formula X, and the statement X has the modal force of law
(exists (?FORMULA)
    (and
        (instance ?FORMULA Formula)
        (containsFormula ImmigrationAndNationalityAct_Section219_US ?FORMULA)
        (modalAttribute ?FORMULA Law)))
Government.kif 2379-2383 There exists X such that X is an instance of formula, immigration and nationality act- section219-US contains the formula X, and the statement X has the modal force of law
(exists (?FORMULA1 ?FORMULA2)
    (and
        (instance ?FORMULA1 Formula)
        (containsFormula ImmigrationAndNationalityAct_US ?FORMULA1)
        (instance ?FORMULA2 Formula)
        (containsFormula ImmigrationAndNationalityAct_Section219_US ?FORMULA2)
        (entails ?FORMULA1 ?FORMULA2)))
Government.kif 2385-2391 There exist X, Y such that X is an instance of formula, immigration and nationality act_US contains the formula X, Y is an instance of formula, immigration and nationality act- section219-US contains the formula Y, and X entails Y
(exists (?FORMULA)
    (and
        (instance ?FORMULA Formula)
        (containsFormula AntiterrorismAndEffectiveDeathPenaltyAct ?FORMULA)
        (modalAttribute ?FORMULA Law)))
Government.kif 2395-2399 There exists X such that X is an instance of formula, antiterrorism and effective death penalty act contains the formula X, and the statement X has the modal force of law
(exists (?TIME)
    (and
        (instance ?TIME TimeInterval)
        (finishes ?TIME
            (WhenFn JesusOfNazareth))
        (starts ?TIME
            (WhenFn TwelveApostles))
        (forall (?MEM)
            (=>
                (holdsDuring ?TIME
                    (member ?MEM TwelveApostles))
                (holdsDuring ?TIME
                    (friend ?MEM JesusOfNazareth))))))
Media.kif 1917-1925 There exists X such that X is an instance of timeframe, X finishes the time of existence of Jesus of Nazareth, X starts the time of existence of Twelve apostles, and Y Y is a member of Twelve apostles holds during XJesus of Nazareth is a friend of Y holds during X
(exists (?FORMULA)
    (and
        (instance ?FORMULA Formula)
        (containsFormula AmericansWithDisabilitiesAct_US ?FORMULA)
        (modalAttribute ?FORMULA Law)))
Medicine.kif 3176-3180 There exists X such that X is an instance of formula, ADA contains the formula X, and the statement X has the modal force of law
(exists (?D ?M)
    (and
        (instance ?D Disseminating)
        (agent ?D Netflix)
        (patient ?D ?M)
        (instance ?M MotionPicture)))
Medicine.kif 4580-4585 There exist X, Y such that X is an instance of disseminating, Netflix Corp. is an agent of X, Y is a patient of X, and Y is an instance of motion picture
(exists (?FM)
    (and
        (instance ?FM FilmMaking)
        (agent ?FM Netflix)))
Medicine.kif 4587-4590 There exists X such that X is an instance of film making and Netflix Corp. is an agent of X
(exists (?H)
    (and
        (attribute ?H NewReporter)
        (employs ProPublica ?H)))
Medicine.kif 4611-4614 There exists X such that NewReporter is an attribute of X and Pro Publica Inc. employs X


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



Sigma web home      Suggested Upper Merged Ontology (SUMO) web home
Sigma version 3.0.0-0a80e6c8 (2026-05-12) is open source software produced by Articulate Software and its partners