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


KB Term:  Term intersection
English Word: 

  RealNumberFn

 Sigma KEE - not
not

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


(=>
    (and
        (contraryAttribute @ROW)
        (equal ?ATTR1
            (ListOrderFn
                (ListFn @ROW) ?NUMBER1))
        (equal ?ATTR2
            (ListOrderFn
                (ListFn @ROW) ?NUMBER2))
        (not
            (equal ?NUMBER1 ?NUMBER2))
        (property ?OBJ ?ATTR1))
    (not
        (property ?OBJ ?ATTR2)))		 Merge.kif 468-476 If @ROW is the opposite of, equal Y and Z element of (@ROW), equal W and V element of (@ROW), equal U and T, and S the attribute Y, then S does not have the attribute W
(=>
    (and
        (partition ?SUPER ?SUB1 ?SUB2)
        (instance ?INST ?SUPER)
        (not
            (instance ?INST ?SUB1)))
    (instance ?INST ?SUB2))		 Merge.kif 598-604 If X is exhaustively partitioned into Y and Z, W is an instance of X, and W is not an instance of Y, then W is an instance of Z
(=>
    (and
        (part ?OBJ1 ?OBJ2)
        (not
            (part ?OBJ2 ?OBJ1)))
    (properPart ?OBJ1 ?OBJ2))		 Merge.kif 951-956 If X is a part of Y and Y is not a part of X, then X is a proper part of Y
(=>
    (and
        (instance ?MIXTURE Mixture)
        (piece ?SUBSTANCE ?MIXTURE)
        (not
            (instance ?SUBSTANCE Mixture)))
    (instance ?SUBSTANCE PureSubstance))		 Merge.kif 1273-1278 If X is an instance of mixture, Y is a piece of X, and Y is not an instance of mixture, then Y is an instance of pure substance
(=>
    (and
        (equal ?LIST3
            (ListConcatenateFn ?LIST1 ?LIST2))
        (not
            (equal ?LIST1 NullList))
        (not
            (equal ?LIST2 NullList))
        (lessThanOrEqualTo ?NUMBER1
            (ListLengthFn ?LIST1))
        (lessThanOrEqualTo ?NUMBER2
            (ListLengthFn ?LIST2))
        (instance ?NUMBER1 PositiveInteger)
        (instance ?NUMBER2 PositiveInteger))
    (and
        (equal
            (ListOrderFn ?LIST3 ?NUMBER1)
            (ListOrderFn ?LIST1 ?NUMBER1))
        (equal
            (ListOrderFn ?LIST3
                (AdditionFn
                    (ListLengthFn ?LIST1) ?NUMBER2))
            (ListOrderFn ?LIST2 ?NUMBER2))))		 Merge.kif 3194-3213 If All of the following hold: (1) equal X, the list composed of Y, and Z (2) equal Y and null list (3) equal Z and null list (4) W is less than or equal to length of Y (5) V is less than or equal to length of Z (6) W is an instance of positive integer (7) V is an instance of positive integer, then equal U element of X and U element of Y and equal (length of Y and V)th element of X and T element of Z
(=>
    (and
        (instance ?LIST List)
        (not
            (equal ?LIST NullList)))
    (equal
        (FirstFn ?LIST)
        (ListOrderFn ?LIST 1)))		 Merge.kif 3343-3348 If X is an instance of list and equal X and null list, then equal the first of X and 1th element of X
(=>
    (holdsDuring ?TIME
        (not ?SITUATION))
    (not
        (holdsDuring ?TIME ?SITUATION)))		 Merge.kif 3997-4001 If X holds during Y, then X doesn't hold during Y
(=>
    (and
        (capability ?PROCESS ?ROLE ?OBJ)
        (instance ?OBJ Device)
        (not
            (attribute ?OBJ DeviceDamaged)))
    (modalAttribute
        (exists (?P)
            (and
                (instance ?P ?PROCESS)
                (?ROLE ?P ?OBJ))) Possibility))		 Merge.kif 4020-4030 If X is capable of doing Y as a Z, X is an instance of device, and device damaged is not an attribute of X, then the statement there exists W such that W is an instance of Y, Z W, and X has the modal force of possibility
(=>
    (and
        (equal
            (GreatestCommonDivisorFn @ROW) ?NUMBER)
        (not
            (equal ?NUMBER 0)))
    (forall (?ELEMENT)
        (=>
            (inList ?ELEMENT
                (ListFn @ROW))
            (equal
                (RemainderFn ?ELEMENT ?NUMBER) 0))))		 Merge.kif 4973-4984 If equal the greatest common divisor of @ROW and Y and equal Y and 0, then For all Integer Z: if Z is a member of (@ROW), then equal Z mod Y and 0
(=>
    (and
        (equal
            (GreatestCommonDivisorFn @ROW) ?NUMBER)
        (not
            (equal ?NUMBER 0)))
    (not
        (exists (?GREATER)
            (and
                (greaterThan ?GREATER ?NUMBER)
                (forall (?ELEMENT)
                    (=>
                        (inList ?ELEMENT
                            (ListFn @ROW))
                        (equal
                            (RemainderFn ?ELEMENT ?GREATER) 0)))))))		 Merge.kif 4986-5000 If equal the greatest common divisor of @ROW and Y and equal Y and 0, then there doesn't exist Z such that Z is greater than Y and W W is a member of (@ROW)equal W mod Z and 0
(=>
    (and
        (equal
            (LeastCommonMultipleFn @ROW) ?NUMBER)
        (not
            (equal ?NUMBER 0)))
    (forall (?ELEMENT)
        (=>
            (inList ?ELEMENT
                (ListFn @ROW))
            (equal
                (RemainderFn ?NUMBER ?ELEMENT) 0))))		 Merge.kif 5058-5068 If equal the least common multiple of @ROW and Y and equal Y and 0, then For all Integer Z: if Z is a member of (@ROW), then equal Y mod Z and 0
(=>
    (and
        (equal
            (LeastCommonMultipleFn @ROW) ?NUMBER)
        (not
            (equal ?NUMBER 0)))
    (not
        (exists (?LESS)
            (and
                (lessThan ?LESS ?NUMBER)
                (forall (?ELEMENT)
                    (=>
                        (inList ?ELEMENT
                            (ListFn @ROW))
                        (equal
                            (RemainderFn ?LESS ?ELEMENT) 0)))))))		 Merge.kif 5070-5084 If equal the least common multiple of @ROW and Y and equal Y and 0, then there doesn't exist Z such that Z is less than Y and W W is a member of (@ROW)equal Z mod W and 0
(=>
    (and
        (instance ?NUMBER Integer)
        (not
            (equal ?NUMBER 0)))
    (equal 1
        (MultiplicationFn ?NUMBER
            (ReciprocalFn ?NUMBER))))		 Merge.kif 5198-5203 If X is an instance of integer and equal X and 0, then equal 1, X, and the reciprocal of X
(=>
    (and
        (equal
            (RemainderFn ?NUMBER1 ?NUMBER2) ?NUMBER)
        (not
            (equal ?NUMBER2 0)))
    (equal
        (AdditionFn
            (MultiplicationFn
                (FloorFn
                    (DivisionFn ?NUMBER1 ?NUMBER2)) ?NUMBER2) ?NUMBER) ?NUMBER1))		 Merge.kif 5216-5227 If equal X mod Y and Z and equal Y and 0, then equal (the largest integer less than or equal to X and Y and Y and Z) and X
(=>
    (and
        (not
            (equal ?NUMBER2 0))
        (equal
            (AdditionFn
                (MultiplicationFn
                    (FloorFn
                        (DivisionFn ?NUMBER1 ?NUMBER2)) ?NUMBER2) ?NUMBER) ?NUMBER1))
    (equal
        (RemainderFn ?NUMBER1 ?NUMBER2) ?NUMBER))		 Merge.kif 5229-5240 If equal X and 0 and equal (the largest integer less than or equal to Y and X and X and Z) and Y, then equal Y mod X and Z
(=>
    (and
        (equal
            (RemainderFn ?NUMBER1 ?NUMBER2) ?NUMBER)
        (not
            (equal ?NUMBER 0))
        (not
            (equal ?NUMBER1 0))
        (not
            (equal ?NUMBER2 0)))
    (equal
        (SignumFn ?NUMBER2)
        (SignumFn ?NUMBER)))		 Merge.kif 5242-5254 If equal X mod Y and Z, equal Z and 0, equal X and 0, and equal Y and 0, then equal the sign of Y and the sign of Z
(=>
    (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
(=>
    (and
        (graphPart ?ARC1 ?GRAPH)
        (graphPart ?ARC2 ?GRAPH)
        (graphPart ?NODE1 ?GRAPH)
        (graphPart ?NODE2 ?GRAPH)
        (links ?NODE1 ?NODE2 ?ARC1)
        (links ?NODE1 ?NODE2 ?ARC2)
        (not
            (equal ?ARC1 ?ARC2)))
    (instance ?GRAPH MultiGraph))		 Merge.kif 5910-5919 If All of the following hold: (1) X is a part of Y (2) Z is a part of Y (3) W is a part of Y (4) V is a part of Y (5) X links W and V (6) Z links W and V (7) equal X and Z, then Y is an instance of multi graph
(=>
    (and
        (graphPart ?PATH ?GRAPH)
        (not
            (instance ?GRAPH DirectedGraph)))
    (<=>
        (instance ?PATH
            (GraphPathFn ?NODE1 ?NODE2))
        (instance ?PATH
            (GraphPathFn ?NODE2 ?NODE1))))		 Merge.kif 6181-6187 If X is a part of Y and Y is not an instance of directed graph, then X is an instance of the set of paths between Z, W if, only if X is an instance of the set of paths between W, and Z
(=>
    (and
        (instance ?POINT TimePoint)
        (not
            (equal ?POINT PositiveInfinity)))
    (before ?POINT PositiveInfinity))		 Merge.kif 8043-8047 If X is an instance of time point and equal X and positive infinity, then X happens before positive infinity
(=>
    (and
        (instance ?POINT TimePoint)
        (not
            (equal ?POINT PositiveInfinity)))
    (exists (?OTHERPOINT)
        (temporallyBetween ?POINT ?OTHERPOINT PositiveInfinity)))		 Merge.kif 8049-8054 If X is an instance of time point and equal X and positive infinity, then there exists Y such that Y is between X and positive infinity
(=>
    (and
        (instance ?POINT TimePoint)
        (not
            (equal ?POINT NegativeInfinity)))
    (before NegativeInfinity ?POINT))		 Merge.kif 8061-8065 If X is an instance of time point and equal X and negative infinity, then negative infinity happens before X
(=>
    (and
        (instance ?POINT TimePoint)
        (not
            (equal ?POINT NegativeInfinity)))
    (exists (?OTHERPOINT)
        (temporallyBetween NegativeInfinity ?OTHERPOINT ?POINT)))		 Merge.kif 8067-8072 If X is an instance of time point and equal X and negative infinity, then there exists Y such that Y is between negative infinity and X
(=>
    (and
        (instance ?MONTH
            (MonthFn February ?YEAR))
        (instance ?Y ?YEAR)
        (not
            (instance ?Y LeapYear)))
    (duration ?MONTH
        (MeasureFn 28 DayDuration)))		 Merge.kif 9268-9273 If X is an instance of the month February, Y is an instance of Z, and Y is not an instance of leap year, then duration of X is 28 day duration(s)
(=>
    (and
        (connected ?OBJ1 ?OBJ2)
        (connected ?OBJ1 ?OBJ3)
        (not
            (connected ?OBJ2 ?OBJ3)))
    (connects ?OBJ1 ?OBJ2 ?OBJ3))		 Merge.kif 9779-9785 If X is connected to Y, X is connected to Z, and Y is not connected to Z, then X connects Y and Z

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
(=>
    (and
        (instance ?REL1 Predicate)
        (instance ?REL2 Predicate)
        (disjointRelation ?REL1 ?REL2)
        (?REL1 @ROW2))
    (not
        (?REL2 @ROW2)))		 Merge.kif 439-445 If X is an instance of predicate, Y is an instance of predicate, X and Y are disjoint, and X @ROW2, then Y @ROW2
(=>
    (and
        (contraryAttribute @ROW)
        (equal ?ATTR1
            (ListOrderFn
                (ListFn @ROW) ?NUMBER1))
        (equal ?ATTR2
            (ListOrderFn
                (ListFn @ROW) ?NUMBER2))
        (not
            (equal ?NUMBER1 ?NUMBER2))
        (property ?OBJ ?ATTR1))
    (not
        (property ?OBJ ?ATTR2)))		 Merge.kif 468-476 If @ROW is the opposite of, equal Y and Z element of (@ROW), equal W and V element of (@ROW), equal U and T, and S the attribute Y, then S does not have the attribute 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)
(=>
    (greaterThanByQuality ?E1 ?E2 ?ATT)
    (not
        (greaterThanByQuality ?E2 ?E1 ?ATT)))		 Merge.kif 751-754 If X has more Y than Z, then Z has more Y than X
(=>
    (greaterThanByQuality ?E1 ?E2 ?ATT)
    (not
        (equal ?E2 ?E1)))		 Merge.kif 756-759 If X has more Y than Z, then equal Z and X
(=>
    (equal ?F
        (FrontFn ?O))
    (not
        (overlapsSpatially ?F
            (BackFn ?O))))		 Merge.kif 907-912 If equal X and the front of Y, then X and the back of Y doesn't overlapsSpatially
(=>
    (equal ?B
        (BackFn ?O))
    (not
        (overlapsSpatially ?B
            (FrontFn ?O))))		 Merge.kif 914-919 If equal X and the back of Y, then X and the front of Y doesn't overlapsSpatially
(=>
    (properPart ?OBJ1 ?OBJ2)
    (and
        (part ?OBJ1 ?OBJ2)
        (not
            (part ?OBJ2 ?OBJ1))))		 Merge.kif 944-949 If X is a proper part of Y, then X is a part of Y and Y is not a part of X
(=>
    (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
(=>
    (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
(=>
    (and
        (instance ?LANG AnimalLanguage)
        (agent ?PROC ?AGENT)
        (instrument ?PROC ?LANG))
    (and
        (instance ?AGENT Animal)
        (not
            (instance ?AGENT Human))))		 Merge.kif 1509-1516 If X is an instance of animal language, Y is an agent of Z, and X is an instrument for Z, then Y is an instance of animal and Y is not an instance of human
(=>
    (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
(=>
    (and
        (instance ?PROC SingleAgentProcess)
        (agent ?PROC ?AGENT1)
        (agent ?PROC ?AGENT2))
    (and
        (equal ?AGENT1 ?AGENT2)
        (not
            (exists (?AGENT3)
                (and
                    (agent ?PROC ?AGENT3)
                    (not
                        (equal ?AGENT3 ?AGENT1)))))))		 Merge.kif 1748-1760 If X is an instance of single agent process, Y is an agent of X, and Z is an agent of X, then equal Y and Z and there doesn't exist W such that W is an agent of X, equal W, and Y
(=>
    (instance ?REL IrreflexiveRelation)
    (forall (?INST)
        (not
            (?REL ?INST ?INST))))		 Merge.kif 2364-2368 If X is an instance of irreflexive relation, then For all Entity Y: X Y and Y
(=>
    (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 IntransitiveRelation)
    (forall (?INST1 ?INST2 ?INST3)
        (=>
            (and
                (?REL ?INST1 ?INST2)
                (?REL ?INST2 ?INST3))
            (not
                (?REL ?INST1 ?INST3)))))		 Merge.kif 2465-2473 If X is an instance of intransitive relation, then For all Entities Y, Z, and W: if X Y and Z and X Z and W, then X Y and W
(=>
    (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
        (resourceExhausted ?P ?R)
        (instance ?R ?C))
    (holdsDuring
        (ImmediateFutureFn
            (WhenFn ?P))
        (not
            (exists (?OBJ1)
                (and
                    (part ?OBJ1 ?R)
                    (instance ?OBJ1 ?C))))))		 Merge.kif 2644-2655 If X exhausts Y and Y is an instance of Z, then there doesn't exist W such that W is a part of Y and W is an instance of Z holds during immediately after the time of existence of X
(=>
    (disjointDecomposition ?CLASS @ROW)
    (forall (?ITEM1 ?ITEM2)
        (=>
            (and
                (inList ?ITEM1
                    (ListFn @ROW))
                (inList ?ITEM2
                    (ListFn @ROW))
                (not
                    (equal ?ITEM1 ?ITEM2)))
            (disjoint ?ITEM1 ?ITEM2))))		 Merge.kif 3068-3077 If X is disjointly decomposed into @ROW, then For all Classes Z and W: if Z is a member of (@ROW), W is a member of (@ROW), and equal Z and W, then Z is disjoint from W
(=>
    (instance ?FUN OneToOneFunction)
    (forall (?ARG1 ?ARG2)
        (=>
            (exists (?CLASS)
                (and
                    (domain ?FUN 1 ?CLASS)
                    (instance ?ARG1 ?CLASS)
                    (instance ?ARG2 ?CLASS)
                    (not
                        (equal ?ARG1 ?ARG2))))
            (not
                (equal
                    (AssignmentFn ?FUN ?ARG1)
                    (AssignmentFn ?FUN ?ARG2))))))		 Merge.kif 3488-3498 If X is an instance of one to one function, then For all Entities Y and Z: if there exists W such that the number 1 argument of X is an instance of W, Y is an instance of W, Z is an instance of W, equal Y, and Z, then equal X(Y) and X(Z)
(=>
    (instance ?REL VariableArityRelation)
    (not
        (exists (?INT)
            (valence ?REL ?INT))))		 Merge.kif 3640-3644 If X is an instance of variable arity relation, then there doesn't exist Y such that X has Y argument(s)
(=>
    (holdsDuring ?TIME
        (not ?SITUATION))
    (not
        (holdsDuring ?TIME ?SITUATION)))		 Merge.kif 3997-4001 If X holds during Y, then X doesn't hold during Y

Display limited to 25 items. Show next 25

Display limited to 25 items. Show next 25

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


(forall (?A ?COURSE)
    (not
        (classmate ?A ?A ?COURSE)))		 Mid-level-ontology.kif 18442-18443 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 18461-18462 For all Human X and Organization Y: X and X were employs by the same organization Y
(holdsDuring
    (FutureFn ?TIME)
    (and
        (instance ?TIME
            (DayFn 3
                (MonthFn June
                    (YearFn 2006))))
        (not
            (instance SerbiaAndMontenegro IndependentState))))		 Media.kif 2493-2497 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

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


(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
(not
    (overlapsTemporally CommonEra BeforeCommonEra))		 Mid-level-ontology.kif 9212-9212 Before common era doesn't overlap common era
(not
    (and
        (instance ?CURSOR MouseCursor)
        (hasGUEState ?CURSOR GUE_ActiveState)))		 ComputerInput.kif 1968-1971 ~{ 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 2027-2031 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 2242-2245 ~{ X is an instance of cursor } or ~{ X has state GUE selected state }
(not
    (vegetationType ArcticRegion BotanicalTree))		 Geography.kif 5011-5011 Botanical tree is found in arctic region
(not
    (equal BigSix GroupOf6))		 Government.kif 2907-2907 equal big six and group of6
(not
    (member Denmark EuropeanMonetaryUnion))		 Government.kif 3211-3211 Denmark is not a member of european monetary union
(not
    (member Sweden EuropeanMonetaryUnion))		 Government.kif 3212-3212 Sweden is not a member of european monetary union
(not
    (member UnitedKingdom EuropeanMonetaryUnion))		 Government.kif 3213-3213 United kingdom is not a member of european monetary union


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