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


KB Term:  Term intersection
English Word: 

  NaturalSubstance

 Sigma KEE - or
or

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


(=>
    (and
        (equal
            (PathWeightFn ?PATH) ?SUM)
        (subGraph ?SUBPATH ?PATH)
        (graphPart ?ARC1 ?PATH)
        (arcWeight ?ARC1 ?NUMBER1)
        (forall (?ARC2)
            (=>
                (graphPart ?ARC2 ?PATH)
                (or
                    (graphPart ?ARC2 ?SUBPATH)
                    (equal ?ARC2 ?ARC1)))))
    (equal ?SUM
        (AdditionFn
            (PathWeightFn ?SUBPATH) ?NUMBER1)))		 Merge.kif 6098-6110 If equal the value of X and Y, Z is a subgraph of X, W is a part of X, the value of W is V, and For all GraphElement U: if U is a part of X, then U is a part of Z or equal U and W, then equal Y and (the value of Z and V)
(=>
    (and
        (equal
            (PathWeightFn ?PATH) ?SUM)
        (graphPart ?ARC1 ?PATH)
        (graphPart ?ARC2 ?PATH)
        (arcWeight ?ARC1 ?NUMBER1)
        (arcWeight ?ARC2 ?NUMBER2)
        (forall (?ARC3)
            (=>
                (graphPart ?ARC3 ?PATH)
                (or
                    (equal ?ARC3 ?ARC1)
                    (equal ?ARC3 ?ARC2)))))
    (equal
        (PathWeightFn ?PATH)
        (AdditionFn ?NUMBER1 ?NUMBER2)))		 Merge.kif 6112-6125 If All of the following hold: (1) equal the value of X and Y (2) Z is a part of X (3) W is a part of X (4) the value of Z is V (5) the value of W is U (6) For all GraphElement T: if T is a part of X, then equal T and Z or equal T and W, then equal the value of X and (V and U)
(=>
    (or
        (before ?POINT1 ?POINT2)
        (equal ?POINT1 ?POINT2))
    (beforeOrEqual ?POINT1 ?POINT2))		 Merge.kif 8353-8357 If X happens before Y or equal X and Y, then X happens before or at Y
(=>
    (and
        (instance ?PROC ChemicalProcess)
        (or
            (resource ?PROC ?STUFF)
            (result ?PROC ?STUFF)))
    (instance ?STUFF PureSubstance))		 Merge.kif 12804-12810 If X is an instance of chemical process and Y is a resource for X or Y is a result of X, then Y is an instance of pure substance
(=>
    (and
        (instance ?X Substance)
        (or
            (attribute ?X Gas)
            (attribute ?X Liquid)
            (attribute ?X Plasma)))
    (attribute ?X Fluid))		 Merge.kif 17951-17958 If X is an instance of substance and At least one of the following holds: (1) gas is an attribute of X (2) liquid is an attribute of X (3) plasma is an attribute of X, then fluid is an attribute of X
(=>
    (or
        (attribute ?AGENT Asleep)
        (attribute ?AGENT Awake))
    (attribute ?AGENT Living))		 Merge.kif 18692-18696 If asleep is an attribute of X or awake is an attribute of X, then living is an attribute of X
(=>
    (and
        (instance ?A Ambulating)
        (subProcess ?S1 ?A)
        (instance ?S1 Stepping)
        (subProcess ?S2 ?A)
        (instance ?S2 Stepping)
        (equal ?S1START
            (BeginFn
                (WhenFn ?S1)))
        (equal ?S2START
            (BeginFn
                (WhenFn ?S2)))
        (not
            (or
                (before ?S1START ?S2START)
                (before ?S2START ?S1START))))
    (equal ?S1 ?S2))		 Mid-level-ontology.kif 484-497 If All of the following hold: (1) X is an instance of ambulating (2) Y is a subprocess of X (3) Y is an instance of stepping (4) Z is a subprocess of X (5) Z is an instance of stepping (6) equal W and the beginning of the time of existence of Y (7) equal V and the beginning of the time of existence of Z (8) ~{ W happens before V } and ~{ V happens before W }, then equal Y and Z
(=>
    (and
        (or
            (instance ?ROLE OccupationalTrade)
            (instance ?ROLE Profession))
        (holdsDuring ?T1
            (attribute ?HUMAN ?ROLE)))
    (exists (?FIELD)
        (and
            (subclass ?FIELD FieldOfStudy)
            (holdsDuring ?T1
                (hasExpertise ?HUMAN ?FIELD)))))		 Mid-level-ontology.kif 9653-9662 If X is an instance of occupational trade or X is an instance of profession and X is an attribute of Y holds during Z, then there exists W such that W is a subclass of field of study and W has an expertise in Y holds during Z
(=>
    (and
        (agreementClause ?PROP ?ATTR ?AGREEMENT ?AGENT)
        (or
            (equal ?ATTR Obligation)
            (equal ?ATTR Promise)))
    (modalAttribute
        (exists (?PROC)
            (and
                (realization ?PROC ?PROP)
                (agent ?PROC ?AGENT))) Likely))		 Mid-level-ontology.kif 15680-15690 If X has the responsibility to make Y Z in W and equal Z and obligation or equal Z and promise, then the statement there exists V such that V expresses the content of Y and X is an agent of V has the modal force of likely
(=>
    (and
        (protonNumber ?SUBSTANCE ?NUMBER)
        (part ?ATOM ?SUBSTANCE)
        (or
            (instance ?ATOM Atom)
            (instance ?ATOM Molecule)))
    (exists (?PROTON)
        (equal ?NUMBER
            (CardinalityFn
                (KappaFn ?PROTON
                    (and
                        (part ?PROTON ?ATOM)
                        (instance ?PROTON Proton)))))))		 Mid-level-ontology.kif 23961-23974 If X is a proton number of Y, Z is a part of Y, and Z is an instance of atom or Z is an instance of molecule, then there exists W such that equal X and the number of instances in the class described by W
(=>
    (and
        (electronNumber ?SUBSTANCE ?NUMBER)
        (part ?ATOM ?SUBSTANCE)
        (or
            (instance ?ATOM Atom)
            (instance ?ATOM Molecule)))
    (exists (?ELECTRON)
        (equal ?NUMBER
            (CardinalityFn
                (KappaFn ?ELECTRON
                    (and
                        (part ?ELECTRON ?ATOM)
                        (instance ?ELECTRON Electron)))))))		 Mid-level-ontology.kif 23984-23997 If X is an electron number of Y, Z is a part of Y, and Z is an instance of atom or Z is an instance of molecule, then there exists W such that equal X and the number of instances in the class described by W
(<=>
    (and
        (located ?PLACE ?GEO)
        (instance ?PLACE PostalPlace)
        (or
            (instance ?GEO Nation)
            (instance ?GEO DependencyOrSpecialSovereigntyArea)))
    (postCountry ?PLACE ?GEO))		 Mid-level-ontology.kif 26995-27002 X is located at Y, X is an instance of postal place, Y is an instance of nation or Y is an instance of dependency or special sovereignty area if, and only if X is in Y
(=>
    (and
        (postCity ?PLACE ?CITY)
        (geographicSubregion ?CITY ?AREA)
        (or
            (instance ?AREA Nation)
            (instance ?AREA DependencyOrSpecialSovereigntyArea)))
    (postCountry ?PLACE ?AREA))		 Mid-level-ontology.kif 27011-27018 If X is in Y, Y is a geographic subregion of Z, and Z is an instance of nation or Z is an instance of dependency or special sovereignty area, then X is in Z
(=>
    (and
        (attribute ?X WheelchairAccessible)
        (or
            (instance ?X Building)
            (instance ?X Room)))
    (modalAttribute
        (exists (?MOTION ?WHEELCHAIR)
            (and
                (instance ?MOTION Motion)
                (instrument ?MOTION ?WHEELCHAIR)
                (instance ?WHEELCHAIR Wheelchair)
                (eventLocated ?MOTION ?X))) Possibility))		 Mid-level-ontology.kif 28729-28741 If wheelchair accessible is an attribute of X and X is an instance of building or X is an instance of room, then the statement there exist Y, Z such that Y is an instance of motion, Z is an instrument for Y, Z is an instance of wheelchair, and Y is located at X has the modal force of possibility
(=>
    (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 1860-1882 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 1884-1906 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
(=>
    (and
        (attribute ?X Writer)
        (instance ?TEXT ?CLASS)
        (or
            (subclass ?CLASS Text)
            (subclass ?CLASS Document))
        (instance ?WRITE Writing)
        (agent ?WRITE ?X)
        (result ?WRITE ?TEXT))
    (authors ?X ?CLASS))		 Biography.kif 733-743 If All of the following hold: (1) writer is an attribute of X (2) Y is an instance of Z (3) Z is a subclass of text or Z is a subclass of document (4) W is an instance of writing (5) X is an agent of W (6) Y is a result of W, then X is the author of Z
(=>
    (and
        (instance ?PERSON Human)
        (instance ?WRITE Writing)
        (or
            (instance ?TEXT Text)
            (instance ?TEXT Document))
        (result ?WRITE ?TEXT)
        (agent ?WRITE ?PERSON))
    (attribute ?PERSON Writer))		 Biography.kif 745-754 If X is an instance of human, Y is an instance of writing, Z is an instance of text or Z is an instance of document, Z is a result of Y, and X is an agent of Y, then writer is an attribute of X
(=>
    (and
        (instance ?B Buying)
        (patient ?B ?ITEM)
        (origin ?B ?AGENT)
        (or
            (publishedPrice ?ENT ?PRICE ?AGENT ?PS)
            (unitPrice ?ENT ?QUANT ?AGENT ?PS))
        (subclass ?ENT Physical)
        (immediateInstance ?ITEM ?ENT)
        (validPaymentType ?PS ?PAY))
    (modalAttribute
        (exists (?PAYMENT)
            (and
                (instance ?PAYMENT ?PAY)
                (subProcess ?PAYMENT ?B))) Likely))		 Catalog.kif 337-352 If All of the following hold: (1) X is an instance of buying (2) Y is a patient of X (3) X originates at Z (4) the price of W from Z according to V is U or the unit price charged Z under V for T is W (5) W is a subclass of physical (6) Y is an immediate instance of W (7) S is a valid payment under V, then the statement there exists R such that R is an instance of S and R is a subprocess of X has the modal force of likely
(=>
    (and
        (or
            (publishedPrice ?ENT ?PRICE ?AGENT ?PS)
            (unitPrice ?ENT ?QUANT ?AGENT ?PS))
        (subclass ?ENT Physical)
        (immediateInstance ?ITEM ?ENT)
        (validFor ?PS ?CUSTCLASS)
        (instance ?CUSTOMER ?CUSTCLASS))
    (modalAttribute
        (=>
            (and
                (instance ?B Buying)
                (agent ?B ?CUSTOMER)
                (origin ?B ?AGENT)
                (patient ?B ?ITEM))
            (transactionAmount ?B ?PRICE)) Likely))		 Catalog.kif 354-370 If the price of X from Y according to Z is W or the unit price charged Y under Z for V is X, X is a subclass of physical, U is an immediate instance of X, Z is valid for T, and S is an instance of T, then the statement R is an instance of buying, S is an agent of R, R originates at Y, and U is a patient of RW is a transaction amount of R has the modal force of likely
(=>
    (and
        (or
            (publishedPrice ?ENT ?PRICE ?AGENT ?PS)
            (unitPrice ?ENT ?QUANT ?AGENT ?PS))
        (subclass ?ENT Physical)
        (immediateInstance ?ITEM ?ENT)
        (validityPeriod ?PS ?TIMEINT))
    (holdsDuring ?TIMEINT
        (modalAttribute
            (=>
                (and
                    (instance ?S Selling)
                    (agent ?S ?AGENT)
                    (patient ?S ?ITEM))
                (transactionAmount ?S ?PRICE)) Likely)))		 Catalog.kif 372-387 If the price of X from Y according to Z is W or the unit price charged Y under Z for V is X, X is a subclass of physical, U is an immediate instance of X, and Z is valid during T, then the statement S is an instance of selling, Y is an agent of S, and U is a patient of SW is a transaction amount of S has the modal force of likely holds during T
(=>
    (and
        (electricityProductionInPeriod ?AREA ?AMOUNT ?PERIOD)
        (or
            (subclass ?PERIOD Year)
            (subclass ?PERIOD
                (FiscalYearFn ?AREA))))
    (exists (?YEAR)
        (and
            (instance ?YEAR ?PERIOD)
            (holdsDuring ?YEAR
                (annualElectricityProduction ?AREA ?AMOUNT)))))		 Economy.kif 2215-2224 If X is electricity production in period Y for Z and Z is a subclass of year or Z is a subclass of the fiscal year of X, then there exists W such that W is an instance of Z and Y is an annual electricity production of X holds during W
(=>
    (and
        (holdsDuring ?YEAR
            (annualElectricityProduction ?AREA ?AMOUNT))
        (instance ?YEAR ?PERIOD)
        (or
            (subclass ?PERIOD Year)
            (subclass ?PERIOD
                (FiscalYearFn ?AREA))))
    (electricityProductionInPeriod ?AREA ?AMOUNT ?PERIOD))		 Economy.kif 2226-2233 If X is an annual electricity production of Y holds during Z, Z is an instance of W, and W is a subclass of year or W is a subclass of the fiscal year of Y, then Y is electricity production in period X for W
(=>
    (and
        (electricityConsumptionInPeriod ?AREA ?AMOUNT ?PERIOD)
        (or
            (subclass ?PERIOD Year)
            (subclass ?PERIOD
                (FiscalYearFn ?AREA))))
    (exists (?YEAR)
        (and
            (instance ?YEAR ?PERIOD)
            (holdsDuring ?YEAR
                (annualElectricityConsumption ?AREA ?AMOUNT)))))		 Economy.kif 2347-2356 If X is electricity consumption in period Y for Z and Z is a subclass of year or Z is a subclass of the fiscal year of X, then there exists W such that W is an instance of Z and Y is an annual electricity consumption of X holds during W
(=>
    (and
        (holdsDuring ?YEAR
            (annualElectricityConsumption ?AREA ?AMOUNT))
        (instance ?YEAR ?PERIOD)
        (or
            (subclass ?PERIOD Year)
            (subclass ?PERIOD
                (FiscalYearFn ?AREA))))
    (electricityConsumptionInPeriod ?AREA ?AMOUNT ?PERIOD))		 Economy.kif 2358-2365 If X is an annual electricity consumption of Y holds during Z, Z is an instance of W, and W is a subclass of year or W is a subclass of the fiscal year of Y, then Y is electricity consumption in period X for W

Display limited to 25 items. Show next 25

Display limited to 25 items. Show next 25

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


(=>
    (and
        (domain ?REL ?NUMBER ?CLASS1)
        (domain ?REL ?NUMBER ?CLASS2))
    (or
        (subclass ?CLASS1 ?CLASS2)
        (subclass ?CLASS2 ?CLASS1)))		 Merge.kif 215-221 If the number X argument of Y is an instance of Z and the number X argument of Y is an instance of W, then Z is a subclass of W or W is a subclass of Z
(=>
    (and
        (domainSubclass ?REL ?NUMBER ?CLASS1)
        (domainSubclass ?REL ?NUMBER ?CLASS2))
    (or
        (subclass ?CLASS1 ?CLASS2)
        (subclass ?CLASS2 ?CLASS1)))		 Merge.kif 238-244 If the number X argument of Y is a subclass of Z and the number X argument of Y is a subclass of W, then Z is a subclass of W or W is a subclass of Z
(=>
    (and
        (range ?REL ?CLASS1)
        (range ?REL ?CLASS2))
    (or
        (subclass ?CLASS1 ?CLASS2)
        (subclass ?CLASS2 ?CLASS1)))		 Merge.kif 317-323 If the range of X is an instance of Y and the range of X is an instance of Z, then Y is a subclass of Z or Z is a subclass of Y
(=>
    (and
        (rangeSubclass ?REL ?CLASS1)
        (rangeSubclass ?REL ?CLASS2))
    (or
        (subclass ?CLASS1 ?CLASS2)
        (subclass ?CLASS2 ?CLASS1)))		 Merge.kif 343-349 If the values returned by X are subclasses of Y and the values returned by X are subclasses of Z, then Y is a subclass of Z or Z is a subclass of Y
(=>
    (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
(<=>
    (holdsDuring ?TIME
        (attribute ?AGENT LegalPersonhood))
    (holdsDuring ?TIME
        (or
            (capability LegalAction agent ?AGENT)
            (capability LegalAction patient ?AGENT))))		 Merge.kif 1695-1701 Legal personhood is an attribute of X holds during Y if and only if X is capable of doing legal action as a agent or X is capable of doing legal action as a patient holds during Y
(<=>
    (lessThanOrEqualTo ?NUMBER1 ?NUMBER2)
    (or
        (equal ?NUMBER1 ?NUMBER2)
        (lessThan ?NUMBER1 ?NUMBER2)))		 Merge.kif 1970-1974 X is less than, equal to Y if, only if equal X, and Y, or X is less than Y
(=>
    (instance ?NUM BinaryNumber)
    (or
        (equal ?NUM 1)
        (equal ?NUM 0)))		 Merge.kif 2112-2116 If X is an instance of binary number, then equal X and 1 or equal X and 0
(=>
    (instance ?REL TrichotomizingRelation)
    (forall (?INST1 ?INST2)
        (or
            (and
                (?REL ?INST1 ?INST2)
                (not
                    (equal ?INST1 ?INST2))
                (not
                    (?REL ?INST2 ?INST1)))
            (and
                (not
                    (?REL ?INST1 ?INST2))
                (equal ?INST1 ?INST2)
                (not
                    (?REL ?INST2 ?INST1)))
            (and
                (not
                    (?REL ?INST1 ?INST2))
                (not
                    (equal ?INST1 ?INST2))
                (?REL ?INST2 ?INST1)))))		 Merge.kif 2426-2441 If X is an instance of trichotomizing relation, then For all Entities Y and Z: At least one of the following holds: (1) X Y and Z, equal Y and Z, and X Z and Y (2) X Y and Z, equal Y and Z, and X Z and Y (3) X Y and Z, equal Y and Z, and X Z and Y
(=>
    (instance ?REL TotalOrderingRelation)
    (forall (?INST1 ?INST2)
        (and
            (or
                (?REL ?INST1 ?INST2)
                (?REL ?INST2 ?INST1))
            (or
                (not
                    (?REL ?INST1 ?INST2))
                (not
                    (?REL ?INST2 ?INST1))))))		 Merge.kif 2491-2500 If X is an instance of total ordering relation, then For all Entities Y and Z: X Y and Z or X Z and Y and X Y and Z or X Z and Y
(=>
    (and
        (instance ?FORMULA1 Formula)
        (instance ?FORMULA2 Formula))
    (or
        (increasesLikelihood ?FORMULA1 ?FORMULA2)
        (decreasesLikelihood ?FORMULA1 ?FORMULA2)
        (independentProbability ?FORMULA1 ?FORMULA2)))		 Merge.kif 2756-2763 If X is an instance of formula and Y is an instance of formula, then At least one of the following holds: (1) X increases likelihood of Y (2) X decreases likelihood of Y (3) probability of X and Y is independent
(=>
    (and
        (trichotomizingOn ?RELATION ?CLASS)
        (instance ?RELATION RelationExtendedToQuantities))
    (forall (?INST1 ?INST2)
        (=>
            (and
                (instance ?INST1 ?CLASS)
                (instance ?INST2 ?CLASS))
            (or
                (?RELATION ?INST1 ?INST2)
                (?RELATION ?INST2 ?INST1)
                (equal ?INST1 ?INST2)))))		 Merge.kif 3796-3808 If X is trichotomizing on Y and X is an instance of relation extended to quantities, then For all Entities Z and W: if Z is an instance of Y and W is an instance of Y, then At least one of the following holds: (1) X Z and W (2) X W and Z (3) equal Z and W
(=>
    (traverses ?OBJ1 ?OBJ2)
    (or
        (crosses ?OBJ1 ?OBJ2)
        (penetrates ?OBJ1 ?OBJ2)))		 Merge.kif 4301-4305 If X traverses Y, then X crosses Y or X penetrates Y
(<=>
    (and
        (equal
            (AbsoluteValueFn ?NUMBER1) ?NUMBER2)
        (instance ?NUMBER1 RealNumber)
        (instance ?NUMBER2 RealNumber))
    (or
        (and
            (instance ?NUMBER1 NonnegativeRealNumber)
            (equal ?NUMBER1 ?NUMBER2))
        (and
            (instance ?NUMBER1 NegativeRealNumber)
            (equal ?NUMBER2
                (SubtractionFn 0.0 ?NUMBER1)))))		 Merge.kif 4880-4891 equal the absolute value of X and Y and X is an instance of real number and Y is an instance of real number if and only if X is an instance of nonnegative real number and equal X and Y or X is an instance of negative real number and equal Y and (0.0 and X)
(=>
    (equal
        (MaxFn ?NUMBER1 ?NUMBER2) ?NUMBER)
    (or
        (and
            (equal ?NUMBER ?NUMBER1)
            (greaterThan ?NUMBER1 ?NUMBER2))
        (and
            (equal ?NUMBER ?NUMBER2)
            (greaterThan ?NUMBER2 ?NUMBER1))
        (and
            (equal ?NUMBER ?NUMBER1)
            (equal ?NUMBER ?NUMBER2))))		 Merge.kif 5107-5118 If equal the larger of X, Y, and Z, then At least one of the following holds: (1) equal Z and X and X is greater than Y (2) equal Z and Y and Y is greater than X (3) equal Z and X and equal Z and Y
(=>
    (equal
        (MinFn ?NUMBER1 ?NUMBER2) ?NUMBER)
    (or
        (and
            (equal ?NUMBER ?NUMBER1)
            (lessThan ?NUMBER1 ?NUMBER2))
        (and
            (equal ?NUMBER ?NUMBER2)
            (lessThan ?NUMBER2 ?NUMBER1))
        (and
            (equal ?NUMBER ?NUMBER1)
            (equal ?NUMBER ?NUMBER2))))		 Merge.kif 5133-5144 If equal the smaller of X, Y, and Z, then At least one of the following holds: (1) equal Z and X and X is less than Y (2) equal Z and Y and Y is less than X (3) equal Z and X and equal Z and Y
(=>
    (instance ?PRIME PrimeNumber)
    (forall (?NUMBER)
        (=>
            (and
                (equal
                    (RemainderFn ?PRIME ?NUMBER) 0)
                (not
                    (equal ?NUMBER 0)))
            (or
                (equal ?NUMBER 1)
                (equal ?NUMBER ?PRIME)))))		 Merge.kif 5266-5277 If X is an instance of prime number, then For all Integer Y: if equal X mod Y and 0 and equal Y and 0, then equal Y and 1 or equal Y and X
(=>
    (instance ?NUMBER NonnegativeRealNumber)
    (or
        (equal
            (SignumFn ?NUMBER) 1)
        (equal
            (SignumFn ?NUMBER) 0)))		 Merge.kif 5307-5311 If X is an instance of nonnegative real number, then equal the sign of X and 1 or equal the sign of X and 0
(=>
    (and
        (instance ?GRAPH Graph)
        (instance ?NODE1 GraphNode)
        (instance ?NODE2 GraphNode)
        (graphPart ?NODE1 ?GRAPH)
        (graphPart ?NODE2 ?GRAPH)
        (not
            (equal ?NODE1 ?NODE2)))
    (exists (?ARC ?PATH)
        (or
            (links ?NODE1 ?NODE2 ?ARC)
            (and
                (subGraph ?PATH ?GRAPH)
                (instance ?PATH GraphPath)
                (or
                    (and
                        (equal
                            (BeginNodeFn ?PATH) ?NODE1)
                        (equal
                            (EndNodeFn ?PATH) ?NODE2))
                    (and
                        (equal
                            (BeginNodeFn ?PATH) ?NODE2)
                        (equal
                            (EndNodeFn ?PATH) ?NODE1)))))))		 Merge.kif 5750-5770 If All of the following hold: (1) X is an instance of graph (2) Y is an instance of graph node (3) Z is an instance of graph node (4) Y is a part of X (5) Z is a part of X (6) equal Y and Z, then All of the following hold: (1) there exist W (2) V such that W links Y (3) Z, V is a subgraph of X (4) V is an instance of graph path (5) equal the beginning of V (6) Y (7) equal the end of V (8) Z, or equal the beginning of V (9) Z (10) equal the end of V (11) Y
(=>
    (beforeOrEqual ?POINT1 ?POINT2)
    (or
        (before ?POINT1 ?POINT2)
        (equal ?POINT1 ?POINT2)))		 Merge.kif 8347-8351 If X happens before or at Y, then X happens before Y or equal X and Y
(=>
    (and
        (instance ?LEAP LeapYear)
        (instance ?LEAP
            (YearFn ?NUMBER)))
    (or
        (and
            (equal
                (RemainderFn ?NUMBER 4) 0)
            (not
                (equal
                    (RemainderFn ?NUMBER 100) 0)))
        (equal
            (RemainderFn ?NUMBER 400) 0)))		 Merge.kif 9203-9211 If X is an instance of leap year and X is an instance of the year Y, then equal Y mod 4 and 0 and equal Y mod 100 and 0 or equal Y mod 400 and 0
(=>
    (equal
        (TemporalCompositionFn ?INTERVAL ?INTERVALTYPE) ?CLASS)
    (forall (?TIME1 ?TIME2)
        (=>
            (and
                (instance ?TIME1 ?CLASS)
                (instance ?TIME2 ?CLASS)
                (not
                    (equal ?TIME1 ?TIME2)))
            (or
                (meetsTemporally ?TIME1 ?TIME2)
                (meetsTemporally ?TIME2 ?TIME1)
                (earlier ?TIME1 ?TIME2)
                (earlier ?TIME2 ?TIME1)))))		 Merge.kif 9620-9632 If equal decomposition of X into Y and Z, then For all TimeIntervals W and V: if equal W and V, then At least one of the following holds: (1) W meets V (2) V meets W (3) W happens earlier than V (4) V happens earlier than W
(=>
    (connected ?OBJ1 ?OBJ2)
    (or
        (meetsSpatially ?OBJ1 ?OBJ2)
        (overlapsSpatially ?OBJ1 ?OBJ2)))		 Merge.kif 9734-9738 If X is connected to Y, then X meets Y or X and Y overlapsSpatially
(=>
    (equal ?OBJ3
        (MereologicalSumFn ?OBJ1 ?OBJ2))
    (forall (?PART)
        (<=>
            (part ?PART ?OBJ3)
            (or
                (part ?PART ?OBJ1)
                (part ?PART ?OBJ2)))))		 Merge.kif 10023-10030 If equal X, the union of the parts of Y, and Z, then For all Object W: W is a part of X if and only if W is a part of Y or W is a part of Z
(=>
    (and
        (hole ?HOLE ?OBJ1)
        (part ?OBJ1 ?OBJ2))
    (or
        (overlapsSpatially ?HOLE ?OBJ2)
        (hole ?HOLE ?OBJ2)))		 Merge.kif 10130-10136 If X is a hole in Y and Y is a part of Z, then X and Z overlapsSpatially or X is a hole in Z

Display limited to 25 items. Show next 25

Display limited to 25 items. Show next 25

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


(equal
    (ReachingMilitaryAgeAnnuallyMaleFn ?AREA ?YEAR)
    (CardinalityFn
        (KappaFn ?PERSON
            (and
                (instance ?PERSON Human)
                (attribute ?PERSON Male)
                (militaryAge ?AREA ?MILITARYAGE)
                (equal ?AGEMINUSONE
                    (SubtractionFn ?AGE 1))
                (holdsDuring ?YEAR
                    (or
                        (age ?PERSON ?AGEMINUSONE)
                        (age ?PERSON ?AGE)))
                (equal ?AGE ?MILITARYAGE)
                (inhabits ?PERSON ?AREA)))))		 Military.kif 1197-1210 equal the reaching military age annually male of X, Y, and the number of instances in the class described by Z


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

Show without tree

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