<=> (<=>)

The truth-functional connective of bi-implication.

Ontology

SUMO / STRUCTURAL-ONTOLOGY

Class(es)

logical operator

<=>

Coordinate term(s)

=> and entails exists forall not or

Type restrictions

<=>(formula, formula)

Axioms (101)

If rel1 is an inverse of rel2, then for all inst1,inst2 holds: rel1(inst1,inst2) holds if and only if rel2(inst2,inst1) holds.

(=>
      (inverse ?REL1 ?REL2)
      (forall
            (?INST1 ?INST2)
            (<=>
                  (holds ?REL1 ?INST1 ?INST2)
                  (holds ?REL2 ?INST2 ?INST1))))

subclass is a subclass of class if and only if

subclass is an instance of set or class
class is an instance of set or class
for all inst holds: if inst is an instance of subclass, then inst is an instance of class

(<=>
      (subclass ?SUBCLASS ?CLASS)
      (and
            (instance ?SUBCLASS SetOrClass)
            (instance ?CLASS SetOrClass)
            (forall
                  (?INST)
                  (=>
                        (instance ?INST ?SUBCLASS)
                        (instance ?INST ?CLASS)))))

If thing1 is equal to thing2, then for all attr holds: thing1 has an attribute attr if and only if thing2 has an attribute attr.

(=>
      (equal ?THING1 ?THING2)
      (forall
            (?ATTR)
            (<=>
                  (property ?THING1 ?ATTR)
                  (property ?THING2 ?ATTR))))

If attr1 is equal to attr2, then for all thing holds: thing has an attribute attr1 if and only if thing has an attribute attr2.

(=>
      (equal ?ATTR1 ?ATTR2)
      (forall
            (?THING)
            (<=>
                  (property ?THING ?ATTR1)
                  (property ?THING ?ATTR2))))

If thing1 is equal to thing2, then for all class holds: thing1 is an instance of class if and only if thing2 is an instance of class.

(=>
      (equal ?THING1 ?THING2)
      (forall
            (?CLASS)
            (<=>
                  (instance ?THING1 ?CLASS)
                  (instance ?THING2 ?CLASS))))

If class1 is equal to class2, then for all thing holds: thing is an instance of class1 if and only if thing is an instance of class2.

(=>
      (equal ?CLASS1 ?CLASS2)
      (forall
            (?THING)
            (<=>
                  (instance ?THING ?CLASS1)
                  (instance ?THING ?CLASS2))))

If rel1 is equal to rel2, then for all holds: rel1() holds if and only if rel2() holds.

(=>
      (equal ?REL1 ?REL2)
      (forall
            (@ROW)
            (<=>
                  (holds ?REL1 @ROW)
                  (holds ?REL2 @ROW))))

if obj1 is equal to obj2,
then if obj1 is equal to "numberth element of "()"" and obj2 is equal to "numberth element of "()"" and "()" is equal to "()", then () holds if and only if () holds

(=>
      (equal ?OBJ1 ?OBJ2)
      (=>
            (and
                  (equal
                        ?OBJ1
                        (ListOrderFn
                              (ListFn @ROW1)
                              ?NUMBER))
                  (equal
                        ?OBJ2
                        (ListOrderFn
                              (ListFn @ROW2)
                              ?NUMBER))
                  (equal
                        (ListFn @ROW1)
                        (ListFn @ROW2)))
            (<=>
                  (holds @ROW1)
                  (holds @ROW2))))

class1 is disjoint from class2 if and only if

class1 is an instance of set or class
class2 is an instance of set or class
for all inst holds: inst is not an instance of class1 or inst is not an instance of class2

(<=>
      (disjoint ?CLASS1 ?CLASS2)
      (and
            (instance ?CLASS1 SetOrClass)
            (instance ?CLASS2 SetOrClass)
            (forall
                  (?INST)
                  (not
                        (and
                              (instance ?INST ?CLASS1)
                              (instance ?INST ?CLASS2))))))

is exhaustively partitioned into if and only if is covered by and is disjointly decomposed into .

(<=>
      (partition @ROW)
      (and
            (exhaustiveDecomposition @ROW)
            (disjointDecomposition @ROW)))

phys is an instance of physical if and only if there exist loc,time so that phys is located at loc and phys exists during time.

(<=>
      (instance ?PHYS Physical)
      (exists
            (?LOC ?TIME)
            (and
                  (located ?PHYS ?LOC)
                  (time ?PHYS ?TIME))))

obj1 is a properPart of obj2 if and only if obj1 is a part of obj2 and obj2 is not a part of obj1.

(<=>
      (properPart ?OBJ1 ?OBJ2)
      (and
            (part ?OBJ1 ?OBJ2)
            (not
                  (part ?OBJ2 ?OBJ1))))

coll1 is a proper sub-collection of coll2 if and only if

coll1 is an instance of collection
coll2 is an instance of collection
for all member holds: if member is a member of coll1, then member is a member of coll2

(<=>
      (subCollection ?COLL1 ?COLL2)
      (and
            (instance ?COLL1 Collection)
            (instance ?COLL2 Collection)
            (forall
                  (?MEMBER)
                  (=>
                        (member ?MEMBER ?COLL1)
                        (member ?MEMBER ?COLL2)))))

agent is an instance of agent if and only if there exists proc so that proc is an agent of agent.

(<=>
      (instance ?AGENT Agent)
      (exists
            (?PROC)
            (agent ?PROC ?AGENT)))

abs is an instance of abstract if and only if there doesn't exist point so that abs is located at point or abs exists during point.

(<=>
      (instance ?ABS Abstract)
      (not
            (exists
                  (?POINT)
                  (or
                        (located ?ABS ?POINT)
                        (time ?ABS ?POINT)))))

"the description of class" is equal to attr if and only if for all inst holds: inst is an instance of class if and only if inst has an attribute attr.

(<=>
      (equal
            (AbstractionFn ?CLASS)
            ?ATTR)
      (forall
            (?INST)
            (<=>
                  (instance ?INST ?CLASS)
                  (property ?INST ?ATTR))))

"the class corresponding to attribute" is equal to class if and only if "the description of class" is equal to attribute.

(<=>
      (equal
            (ExtensionFn ?ATTRIBUTE)
            ?CLASS)
      (equal
            (AbstractionFn ?CLASS)
            ?ATTRIBUTE))

number1 is less than or equal to number2 if and only if number1 is equal to number2 or number1 is less than number2.

(<=>
      (lessThanOrEqualTo ?NUMBER1 ?NUMBER2)
      (or
            (equal ?NUMBER1 ?NUMBER2)
            (lessThan ?NUMBER1 ?NUMBER2)))

number1 is greater than or equal to number2 if and only if number1 is equal to number2 or number1 is greater than number2.

(<=>
      (greaterThanOrEqualTo ?NUMBER1 ?NUMBER2)
      (or
            (equal ?NUMBER1 ?NUMBER2)
            (greaterThan ?NUMBER1 ?NUMBER2)))

number is an instance of nonnegative real number if and only if number is greater than or equal to and number is an instance of real number.

(<=>
      (instance ?NUMBER NonnegativeRealNumber)
      (and
            (greaterThanOrEqualTo ?NUMBER 0)
            (instance ?NUMBER RealNumber)))

number is an instance of positive real number if and only if number is greater than and number is an instance of real number.

(<=>
      (instance ?NUMBER PositiveRealNumber)
      (and
            (greaterThan ?NUMBER 0)
            (instance ?NUMBER RealNumber)))

number is an instance of negative real number if and only if number is less than and number is an instance of real number.

(<=>
      (instance ?NUMBER NegativeRealNumber)
      (and
            (lessThan ?NUMBER 0)
            (instance ?NUMBER RealNumber)))

If rel is an instance of relation, then rel() holds if and only if rel() holds.

(=>
      (instance ?REL Relation)
      (<=>
            (holds ?REL @ROW)
            (?REL @ROW)))

rel is an instance of single valued relation if and only if for all ,item1,item2 holds: if rel(,item1) holds and rel(,item2) holds, then item1 is equal to item2.

(<=>
      (instance ?REL SingleValuedRelation)
      (forall
            (@ROW ?ITEM1 ?ITEM2)
            (=>
                  (and
                        (holds ?REL @ROW ?ITEM1)
                        (holds ?REL @ROW ?ITEM2))
                  (equal ?ITEM1 ?ITEM2))))

rel is an instance of total valued relation if and only if there exists valence so that rel is an instance of relation and rel %&has valence argument(s) and

if for all number,element,class holds: if number is less than valence and the number number argument of rel is an instance of class and element is equal to "numberth element of "()"", then element is an instance of class,
then there exists item so that rel(,item) holds

(<=>
      (instance ?REL TotalValuedRelation)
      (exists
            (?VALENCE)
            (and
                  (instance ?REL Relation)
                  (valence ?REL ?VALENCE)
                  (=>
                        (forall
                              (?NUMBER ?ELEMENT ?CLASS)
                              (=>
                                    (and
                                          (lessThan ?NUMBER ?VALENCE)
                                          (domain ?REL ?NUMBER ?CLASS)
                                          (equal
                                                ?ELEMENT
                                                (ListOrderFn
                                                      (ListFn @ROW)
                                                      ?NUMBER)))
                                    (instance ?ELEMENT ?CLASS)))
                        (exists
                              (?ITEM)
                              (holds ?REL @ROW ?ITEM))))))

list is an instance of unique list if and only if for all number1,number2 holds: if "number1th element of list" is equal to "number2th element of list", then number1 is equal to number2.

(<=>
      (instance ?LIST UniqueList)
      (forall
            (?NUMBER1 ?NUMBER2)
            (=>
                  (equal
                        (ListOrderFn ?LIST ?NUMBER1)
                        (ListOrderFn ?LIST ?NUMBER2))
                  (equal ?NUMBER1 ?NUMBER2))))

list is equal to null list if and only if there doesn't exist item so that item is a member of list.

(<=>
      (equal ?LIST NullList)
      (not
            (exists
                  (?ITEM)
                  (inList ?ITEM ?LIST))))

If "length of list" is equal to number1, then for all number2 holds: there exists item so that "number2th element of list" is equal to item if and only if number2 is less than or equal to number1.

(=>
      (equal
            (ListLengthFn ?LIST)
            ?NUMBER1)
      (forall
            (?NUMBER2)
            (<=>
                  (exists
                        (?ITEM)
                        (equal
                              (ListOrderFn ?LIST ?NUMBER2)
                              ?ITEM))
                  (lessThanOrEqualTo ?NUMBER2 ?NUMBER1))))

list3 is equal to "the list composed of list1 and list2" if and only if for all number1,number2 holds: if number1 is less than or equal to "length of list1" and number2 is less than or equal to "length of list2" and number1 is an instance of positive integer and number2 is an instance of positive integer, then "number1th element of list3" is equal to "number1th element of list1" and ""("length of list1"+number2)"th element of list3" is equal to "number2th element of list2".

(<=>
      (equal
            ?LIST3
            (ListConcatenateFn ?LIST1 ?LIST2))
      (forall
            (?NUMBER1 ?NUMBER2)
            (=>
                  (and
                        (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))))))

item is a member of list if and only if there exists number so that "numberth element of list" is equal to item.

(<=>
      (inList ?ITEM ?LIST)
      (exists
            (?NUMBER)
            (equal
                  (ListOrderFn ?LIST ?NUMBER)
                  ?ITEM)))

relation is total ordering on class if and only if relation is partial ordering on class and relation is trichotomizing on class.

(<=>
      (totalOrderingOn ?RELATION ?CLASS)
      (and
            (partialOrderingOn ?RELATION ?CLASS)
            (trichotomizingOn ?RELATION ?CLASS)))

"the place where thing was at time" is equal to region if and only if thing is exactly located in region during time.

(<=>
      (equal
            (WhereFn ?THING ?TIME)
            ?REGION)
      (holdsDuring
            ?TIME
            (exactlyLocated ?THING ?REGION)))

obj is an instance of "belongings of person" if and only if person posesses obj.

(<=>
      (instance
            ?OBJ
            (PropertyFn ?PERSON))
      (possesses ?PERSON ?OBJ))

class1 subsumes the content of class2 and class2 subsumes the content of class1 if and only if class1 is equivalent to class2.

(<=>
      (and
            (subsumesContentClass ?CLASS1 ?CLASS2)
            (subsumesContentClass ?CLASS2 ?CLASS1))
      (equivalentContentClass ?CLASS1 ?CLASS2))

class1 subsumes the content of class2 if and only if for all obj2,info holds: if obj2 is an instance of class2 and obj2 contains information info, then there exists class1 obj1 so that obj1 contains information info.

(<=>
      (subsumesContentClass ?CLASS1 ?CLASS2)
      (forall
            (?OBJ2 ?INFO)
            (=>
                  (and
                        (instance ?OBJ2 ?CLASS2)
                        (containsInformation ?OBJ2 ?INFO))
                  (exists
                        (?OBJ1)
                        (and
                              (instance ?OBJ1 ?CLASS1)
                              (containsInformation ?OBJ1 ?INFO))))))

obj1 subsumes the content of obj2 and obj2 subsumes the content of obj1 if and only if obj1 is equivalent to obj2.

(<=>
      (and
            (subsumesContentInstance ?OBJ1 ?OBJ2)
            (subsumesContentInstance ?OBJ2 ?OBJ1))
      (equivalentContentInstance ?OBJ1 ?OBJ2))

obj1 subsumes the content of obj2 if and only if for all info holds: if obj2 contains information info, then obj1 contains information info.

(<=>
      (subsumesContentInstance ?OBJ1 ?OBJ2)
      (forall
            (?INFO)
            (=>
                  (containsInformation ?OBJ2 ?INFO)
                  (containsInformation ?OBJ1 ?INFO))))

express is expressed in language language if and only if there exists prop so that express represents prop in the language language.

(<=>
      (expressedInLanguage ?EXPRESS ?LANGUAGE)
      (exists
            (?PROP)
            (representsInLanguage ?EXPRESS ?PROP ?LANGUAGE)))

"the absolute value of number1" is equal to number2 and number1 is an instance of real number and number2 is an instance of real number if and only if

number1 is an instance of nonnegative real number and number1 is equal to number2
number1 is an instance of negative real number and number2 is equal to "(-number1)"

(<=>
      (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 ?NUMBER1)))))

"number1 mod number2" is equal to number if and only if "(""the largest integer less than or equal to "number1/number2""*number2"+number)" is equal to number1.

(<=>
      (equal
            (RemainderFn ?NUMBER1 ?NUMBER2)
            ?NUMBER)
      (equal
            (AdditionFn
                  (MultiplicationFn
                        (FloorFn
                              (DivisionFn ?NUMBER1 ?NUMBER2))
                        ?NUMBER2)
                  ?NUMBER)
            ?NUMBER1))

If for all element holds: element is an element of set1 if and only if element is an element of set2, then set1 is equal to set2.

(=>
      (forall
            (?ELEMENT)
            (<=>
                  (element ?ELEMENT ?SET1)
                  (element ?ELEMENT ?SET2)))
      (equal ?SET1 ?SET2))

graph is an instance of graph circuit if and only if there exists node so that "the beginning of graph" is equal to node and "the end of graph" is equal to node.

(<=>
      (instance ?GRAPH GraphCircuit)
      (exists
            (?NODE)
            (and
                  (equal
                        (BeginNodeFn ?GRAPH)
                        ?NODE)
                  (equal
                        (EndNodeFn ?GRAPH)
                        ?NODE))))

graph is an instance of multi graph if and only if there exist arc1,arc2,node1,node2 so that arc1 is a part of graph and arc2 is a part of graph and node1 is a part of graph and node2 is a part of graph and arc1 links node1 and node2 and arc2 links node1 and node2 and arc1 is not equal to arc2.

(<=>
      (instance ?GRAPH MultiGraph)
      (exists
            (?ARC1 ?ARC2 ?NODE1 ?NODE2)
            (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)))))

graph is an instance of pseudo graph if and only if there exists graph loop loop so that loop is a part of graph.

(<=>
      (instance ?GRAPH PseudoGraph)
      (exists
            (?LOOP)
            (and
                  (instance ?LOOP GraphLoop)
                  (graphPart ?LOOP ?GRAPH))))

loop is an instance of graph loop if and only if there exists node so that loop links node and node.

(<=>
      (instance ?LOOP GraphLoop)
      (exists
            (?NODE)
            (links ?NODE ?NODE ?LOOP)))

If path is a part of graph and graph is not an instance of directed graph, then "the set of paths between node1 and node2" is equal to path if and only if "the set of paths between node2 and node1" is equal to path.

(=>
      (and
            (graphPart ?PATH ?GRAPH)
            (not
                  (instance ?GRAPH DirectedGraph)))
      (<=>
            (equal
                  (GraphPathFn ?NODE1 ?NODE2)
                  ?PATH)
            (equal
                  (GraphPathFn ?NODE2 ?NODE1)
                  ?PATH)))

quantity is an instance of "the interval from from to to" if and only if quantity is greater than or equal to from and quantity is less than or equal to to.

(<=>
      (instance
            ?QUANTITY
            (IntervalFn ?FROM ?TO))
      (and
            (greaterThanOrEqualTo ?QUANTITY ?FROM)
            (lessThanOrEqualTo ?QUANTITY ?TO)))

"value of belongings of person" is equal to amount if and only if value of "belongings of person" is amount.

(<=>
      (equal
            (WealthFn ?PERSON)
            ?AMOUNT)
      (monetaryValue
            (PropertyFn ?PERSON)
            ?AMOUNT))

pos is a part of "the time of existence of thing" if and only if thing exists during pos.

(<=>
      (temporalPart
            ?POS
            (WhenFn ?THING))
      (time ?THING ?POS))

interval1 starts interval2 if and only if "the beginning of interval1" is equal to "the beginning of interval2" and "the end of interval1" happen?{s} before "the end of interval2".

(<=>
      (starts ?INTERVAL1 ?INTERVAL2)
      (and
            (equal
                  (BeginFn ?INTERVAL1)
                  (BeginFn ?INTERVAL2))
            (before
                  (EndFn ?INTERVAL1)
                  (EndFn ?INTERVAL2))))

interval1 finishes interval2 if and only if "the beginning of interval2" happen?{s} before "the beginning of interval1" and "the end of interval2" is equal to "the end of interval1".

(<=>
      (finishes ?INTERVAL1 ?INTERVAL2)
      (and
            (before
                  (BeginFn ?INTERVAL2)
                  (BeginFn ?INTERVAL1))
            (equal
                  (EndFn ?INTERVAL2)
                  (EndFn ?INTERVAL1))))

point2 is between point1 and point3 if and only if point1 happen?{s} before point2 and point2 happen?{s} before point3.

(<=>
      (temporallyBetween ?POINT1 ?POINT2 ?POINT3)
      (and
            (before ?POINT1 ?POINT2)
            (before ?POINT2 ?POINT3)))

point2 is between or at point1 and point3 if and only if point1 happen?{s} before or at point2 and point2 happen?{s} before or at point3.

(<=>
      (temporallyBetweenOrEqual ?POINT1 ?POINT2 ?POINT3)
      (and
            (beforeOrEqual ?POINT1 ?POINT2)
            (beforeOrEqual ?POINT2 ?POINT3)))

phys exists during time and time is an instance of time point if and only if time is between or at "the beginning of "the time of existence of phys"" and "the end of "the time of existence of phys"".

(<=>
      (and
            (time ?PHYS ?TIME)
            (instance ?TIME TimePoint))
      (temporallyBetweenOrEqual
            (BeginFn
                  (WhenFn ?PHYS))
            ?TIME
            (EndFn
                  (WhenFn ?PHYS))))

interval2 overlaps interval1 if and only if there exists time interval interval3 so that interval3 is a part of interval1 and interval3 is a part of interval2.

(<=>
      (overlapsTemporally ?INTERVAL1 ?INTERVAL2)
      (exists
            (?INTERVAL3)
            (and
                  (instance ?INTERVAL3 TimeInterval)
                  (temporalPart ?INTERVAL3 ?INTERVAL1)
                  (temporalPart ?INTERVAL3 ?INTERVAL2))))

interval1 meets interval2 if and only if "the end of interval1" is equal to "the beginning of interval2".

(<=>
      (meetsTemporally ?INTERVAL1 ?INTERVAL2)
      (equal
            (EndFn ?INTERVAL1)
            (BeginFn ?INTERVAL2)))

interval1 happens earlier than interval2 if and only if "the end of interval1" happen?{s} before "the beginning of interval2".

(<=>
      (earlier ?INTERVAL1 ?INTERVAL2)
      (before
            (EndFn ?INTERVAL1)
            (BeginFn ?INTERVAL2)))

phys1 occurs at the same time as phys2 if and only if "the time of existence of phys1" is equal to "the time of existence of phys2".

(<=>
      (cooccur ?PHYS1 ?PHYS2)
      (equal
            (WhenFn ?PHYS1)
            (WhenFn ?PHYS2)))

If "interval between point1 and point2" is equal to interval, then for all point holds: point is between or at point1 and point2 if and only if point is a part of interval.

(=>
      (equal
            (TimeIntervalFn ?POINT1 ?POINT2)
            ?INTERVAL)
      (forall
            (?POINT)
            (<=>
                  (temporallyBetweenOrEqual ?POINT1 ?POINT ?POINT2)
                  (temporalPart ?POINT ?INTERVAL))))

obj is an instance of self connected object if and only if for all part1,part2 holds: if obj is equal to "the union of the parts of part1 and part2", then part1 is connected to part2.

(<=>
      (instance ?OBJ SelfConnectedObject)
      (forall
            (?PART1 ?PART2)
            (=>
                  (equal
                        ?OBJ
                        (MereologicalSumFn ?PART1 ?PART2))
                  (connected ?PART1 ?PART2))))

obj1 connects obj2 and obj3 if and only if obj1 is connected to obj2 and obj1 is connected to obj3 and obj2 is not connected to obj3.

(<=>
      (connects ?OBJ1 ?OBJ2 ?OBJ3)
      (and
            (connected ?OBJ1 ?OBJ2)
            (connected ?OBJ1 ?OBJ3)
            (not
                  (connected ?OBJ2 ?OBJ3))))

obj1 overlaps with obj2 if and only if there exists obj3 so that obj3 is a part of obj1 and obj3 is a part of obj2.

(<=>
      (overlapsSpatially ?OBJ1 ?OBJ2)
      (exists
            (?OBJ3)
            (and
                  (part ?OBJ3 ?OBJ1)
                  (part ?OBJ3 ?OBJ2))))

obj1 partially overlaps with obj2 if and only if

obj1 is not a part of obj2
obj2 is not a part of obj1
there exists obj3 so that obj3 is a part of obj1 and obj3 is a part of obj2

(<=>
      (overlapsPartially ?OBJ1 ?OBJ2)
      (and
            (not
                  (part ?OBJ1 ?OBJ2))
            (not
                  (part ?OBJ2 ?OBJ1))
            (exists
                  (?OBJ3)
                  (and
                        (part ?OBJ3 ?OBJ1)
                        (part ?OBJ3 ?OBJ2)))))

The width of object is width if and only if there exist side1,side2 so that a side of object is side1 and a side of object is side2 and the distance between side1 and side2 is width.

(<=>
      (width ?OBJECT ?WIDTH)
      (exists
            (?SIDE1 ?SIDE2)
            (and
                  (side ?SIDE1 ?OBJECT)
                  (side ?SIDE2 ?OBJECT)
                  (distance ?SIDE1 ?SIDE2 ?WIDTH))))

If obj3 is equal to "the union of the parts of obj1 and obj2", then for all part holds: part is a part of obj3 if and only if part is a part of obj1 or part is a part of obj2.

(=>
      (equal
            ?OBJ3
            (MereologicalSumFn ?OBJ1 ?OBJ2))
      (forall
            (?PART)
            (<=>
                  (part ?PART ?OBJ3)
                  (or
                        (part ?PART ?OBJ1)
                        (part ?PART ?OBJ2)))))

If obj3 is equal to "the intersection of the parts of obj1 and obj2", then for all part holds: part is a part of obj3 if and only if part is a part of obj1 and part is a part of obj2.

(=>
      (equal
            ?OBJ3
            (MereologicalProductFn ?OBJ1 ?OBJ2))
      (forall
            (?PART)
            (<=>
                  (part ?PART ?OBJ3)
                  (and
                        (part ?PART ?OBJ1)
                        (part ?PART ?OBJ2)))))

If obj3 is equal to "the difference between the parts of obj1 and obj2", then for all part holds: part is a part of obj3 if and only if part is a part of obj1 and part is not a part of obj2.

(=>
      (equal
            ?OBJ3
            (MereologicalDifferenceFn ?OBJ1 ?OBJ2))
      (forall
            (?PART)
            (<=>
                  (part ?PART ?OBJ3)
                  (and
                        (part ?PART ?OBJ1)
                        (not
                              (part ?PART ?OBJ2))))))

hole is an instance of hole if and only if there exists obj so that hole is a hole in obj.

(<=>
      (instance ?HOLE Hole)
      (exists
            (?OBJ)
            (hole ?HOLE ?OBJ)))

If obj1 is equal to "the host of the hole hole", then for all obj2 holds: obj2 overlaps with obj1 if and only if there exists obj3 so that hole is a hole in obj3 and obj2 overlaps with obj3.

(=>
      (equal
            ?OBJ1
            (PrincipalHostFn ?HOLE))
      (forall
            (?OBJ2)
            (<=>
                  (overlapsSpatially ?OBJ2 ?OBJ1)
                  (exists
                        (?OBJ3)
                        (and
                              (hole ?HOLE ?OBJ3)
                              (overlapsSpatially ?OBJ2 ?OBJ3))))))

fillable is an attribute of hole1 if and only if there exists hole hole2 so that hole1 is a part of hole2.

(<=>
      (attribute ?HOLE1 Fillable)
      (exists
            (?HOLE2)
            (and
                  (instance ?HOLE2 Hole)
                  (part ?HOLE1 ?HOLE2))))

If obj1 is equal to "the surface of the hole hole", then for all obj2 holds: obj2 overlaps with obj1 if and only if there exists obj3 so that obj3 is a superficial part of "the host of the hole hole" and hole meets obj3 and obj2 overlaps with obj3.

(=>
      (equal
            ?OBJ1
            (SkinFn ?HOLE))
      (forall
            (?OBJ2)
            (<=>
                  (overlapsSpatially ?OBJ2 ?OBJ1)
                  (exists
                        (?OBJ3)
                        (and
                              (superficialPart
                                    ?OBJ3
                                    (PrincipalHostFn ?HOLE))
                              (meetsSpatially ?HOLE ?OBJ3)
                              (overlapsSpatially ?OBJ2 ?OBJ3))))))

inj is an instance of injuring if and only if inj is an instance of damaging and organism is a patient of inj.

(<=>
      (instance ?INJ Injuring)
      (and
            (instance ?INJ Damaging)
            (patient ?INJ Organism)))

There exists borrowing borrow so that borrow is an agent of agent1 and borrow origins at agent2 and object is a patient of borrow if and only if there exists lending lend so that lend is an agent of agent2 and lend ends at agent1 and object is a patient of lend.

(<=>
      (exists
            (?BORROW)
            (and
                  (instance ?BORROW Borrowing)
                  (agent ?BORROW ?AGENT1)
                  (origin ?BORROW ?AGENT2)
                  (patient ?BORROW ?OBJECT)))
      (exists
            (?LEND)
            (and
                  (instance ?LEND Lending)
                  (agent ?LEND ?AGENT2)
                  (destination ?LEND ?AGENT1)
                  (patient ?LEND ?OBJECT))))

There exists buying buy so that buy is an agent of agent1 and buy origins at agent2 and object is a patient of buy if and only if there exists selling sell so that sell is an agent of agent2 and sell ends at agent1 and object is a patient of sell.

(<=>
      (exists
            (?BUY)
            (and
                  (instance ?BUY Buying)
                  (agent ?BUY ?AGENT1)
                  (origin ?BUY ?AGENT2)
                  (patient ?BUY ?OBJECT)))
      (exists
            (?SELL)
            (and
                  (instance ?SELL Selling)
                  (agent ?SELL ?AGENT2)
                  (destination ?SELL ?AGENT1)
                  (patient ?SELL ?OBJECT))))

process is an instance of destruction if and only if there exists patient so that patient is a patient of process and patient exists during "immediately before "the time of existence of process"" and patient doesn't exist during "immediately after "the time of existence of process"".

(<=>
      (instance ?PROCESS Destruction)
      (exists
            (?PATIENT)
            (and
                  (patient ?PROCESS ?PATIENT)
                  (time
                        ?PATIENT
                        (ImmediatePastFn
                              (WhenFn ?PROCESS)))
                  (not
                        (time
                              ?PATIENT
                              (ImmediateFutureFn
                                    (WhenFn ?PROCESS)))))))

combine is an instance of combining and obj1 is a resource for combine and obj2 is a result of combine if and only if obj1 is not a part of obj2 immediately before "the time of existence of combine" and obj1 is a part of obj2 immediately after "the time of existence of combine".

(<=>
      (and
            (instance ?COMBINE Combining)
            (resource ?COMBINE ?OBJ1)
            (result ?COMBINE ?OBJ2))
      (and
            (holdsDuring
                  (ImmediatePastFn
                        (WhenFn ?COMBINE))
                  (not
                        (part ?OBJ1 ?OBJ2)))
            (holdsDuring
                  (ImmediateFutureFn
                        (WhenFn ?COMBINE))
                  (part ?OBJ1 ?OBJ2))))

compound is an instance of compound substance if and only if there exist elemental substance element1,elemental substance element2,chemical synthesis process so that element1 is not equal to element2 and element1 is a resource for process and element2 is a resource for process and compound is a result of process.

(<=>
      (instance ?COMPOUND CompoundSubstance)
      (exists
            (?ELEMENT1 ?ELEMENT2 ?PROCESS)
            (and
                  (instance ?ELEMENT1 ElementalSubstance)
                  (instance ?ELEMENT2 ElementalSubstance)
                  (not
                        (equal ?ELEMENT1 ?ELEMENT2))
                  (instance ?PROCESS ChemicalSynthesis)
                  (resource ?PROCESS ?ELEMENT1)
                  (resource ?PROCESS ?ELEMENT2)
                  (result ?PROCESS ?COMPOUND))))

process is an instance of creation if and only if there exists patient so that patient is a patient of process and patient exists during "immediately after "the time of existence of process"" and patient doesn't exist during "immediately before "the time of existence of process"".

(<=>
      (instance ?PROCESS Creation)
      (exists
            (?PATIENT)
            (and
                  (patient ?PROCESS ?PATIENT)
                  (time
                        ?PATIENT
                        (ImmediateFutureFn
                              (WhenFn ?PROCESS)))
                  (not
                        (time
                              ?PATIENT
                              (ImmediatePastFn
                                    (WhenFn ?PROCESS)))))))

There exists constructing build so that artifact is a result of build if and only if artifact is an instance of stationary artifact.

(<=>
      (exists
            (?BUILD)
            (and
                  (instance ?BUILD Constructing)
                  (result ?BUILD ?ARTIFACT)))
      (instance ?ARTIFACT StationaryArtifact))

There exists radiating light emit so that region is a patient of emit and region is an instance of region if and only if illuminated is an attribute of region.

(<=>
      (exists
            (?EMIT)
            (and
                  (instance ?EMIT RadiatingLight)
                  (patient ?EMIT ?REGION)
                  (instance ?REGION Region)))
      (attribute ?REGION Illuminated))

animal1 is a sibling of animal2 if and only if there exist father,mother so that father is a father of animal1 and father is a father of animal2 and mother is a mother of animal1 and mother is a mother of animal2.

(<=>
      (sibling ?ANIMAL1 ?ANIMAL2)
      (exists
            (?FATHER ?MOTHER)
            (and
                  (father ?ANIMAL1 ?FATHER)
                  (father ?ANIMAL2 ?FATHER)
                  (mother ?ANIMAL1 ?MOTHER)
                  (mother ?ANIMAL2 ?MOTHER))))

org publishes text if and only if there exists publication pub so that pub is an agent of org and text is a patient of pub.

(<=>
      (publishes ?ORG ?TEXT)
      (exists
            (?PUB)
            (and
                  (instance ?PUB Publication)
                  (agent ?PUB ?ORG)
                  (patient ?PUB ?TEXT))))

artifact is an instance of artifact if and only if there exists making making so that artifact is a result of making.

(<=>
      (instance ?ARTIFACT Artifact)
      (exists
            (?MAKING)
            (and
                  (instance ?MAKING Making)
                  (result ?MAKING ?ARTIFACT))))

comp1 is connected to comp2 if and only if there exists connection so that connection connects comp1 and comp2.

(<=>
      (connectedEngineeringComponents ?COMP1 ?COMP2)
      (exists
            (?CONNECTION)
            (connectsEngineeringComponents ?CONNECTION ?COMP1 ?COMP2)))

If "the legal organizational entity of unit" is equal to org and attr is an instance of normative attribute, then attr is an attribute of unit if and only if attr is an attribute of org.

(=>
      (and
            (equal
                  (OrganizationFn ?UNIT)
                  ?ORG)
            (instance ?ATTR NormativeAttribute))
      (<=>
            (attribute ?UNIT ?ATTR)
            (attribute ?ORG ?ATTR)))

obj1 is north to obj2 if and only if obj2 is south to obj1.

(<=>
      (orientation ?OBJ1 ?OBJ2 North)
      (orientation ?OBJ2 ?OBJ1 South))

obj1 is east to obj2 if and only if obj2 is west to obj1.

(<=>
      (orientation ?OBJ1 ?OBJ2 East)
      (orientation ?OBJ2 ?OBJ1 West))

obj1 is vertical to obj2 if and only if obj2 is horizontal to obj1.

(<=>
      (orientation ?OBJ1 ?OBJ2 Vertical)
      (orientation ?OBJ2 ?OBJ1 Horizontal))

obj1 is above to obj2 if and only if obj2 is below to obj1.

(<=>
      (orientation ?OBJ1 ?OBJ2 Above)
      (orientation ?OBJ2 ?OBJ1 Below))

obj1 is right to obj2 if and only if obj2 is left to obj1.

(<=>
      (orientation ?OBJ1 ?OBJ2 Right)
      (orientation ?OBJ2 ?OBJ1 Left))

For all org holds: org doesn't employ person and person is an instance of human if and only if unemployed is an attribute of person.

(<=>
      (forall
            (?ORG)
            (and
                  (not
                        (employs ?ORG ?PERSON))
                  (instance ?PERSON Human)))
      (attribute ?PERSON Unemployed))

The statement formula has the model force of necessity if and only if the statement "formula" has the model force of possibility.

(<=>
      (modalAttribute ?FORMULA Necessity)
      (not
            (modalAttribute
                  (not ?FORMULA)
                  Possibility)))

The statement formula has the model force of obligation if and only if the statement "formula" has the model force of permission.

(<=>
      (modalAttribute ?FORMULA Obligation)
      (not
            (modalAttribute
                  (not ?FORMULA)
                  Permission)))

obj is an instance of substance if and only if there exists physical state attr so that attr is an attribute of obj.

(<=>
      (instance ?OBJ Substance)
      (exists
            (?ATTR)
            (and
                  (instance ?ATTR PhysicalState)
                  (attribute ?OBJ ?ATTR))))

agent is an instance of sentient agent and living is an attribute of agent if and only if there exists consciousness attribute attr so that attr is an attribute of agent.

(<=>
      (and
            (instance ?AGENT SentientAgent)
            (attribute ?AGENT Living))
      (exists
            (?ATTR)
            (and
                  (instance ?ATTR ConsciousnessAttribute)
                  (attribute ?AGENT ?ATTR))))

entity is an instance of "the union of class1 and class2" if and only if entity is an instance of class1 or entity is an instance of class2.

(<=>
      (instance
            ?ENTITY
            (UnionFn ?CLASS1 ?CLASS2))
      (or
            (instance ?ENTITY ?CLASS1)
            (instance ?ENTITY ?CLASS2)))

entity is an instance of "the union of class1 and class2" if and only if entity is an instance of class1 and entity is an instance of class2.

(<=>
      (instance
            ?ENTITY
            (IntersectionFn ?CLASS1 ?CLASS2))
      (and
            (instance ?ENTITY ?CLASS1)
            (instance ?ENTITY ?CLASS2)))

entity is an instance of "the complement of class" if and only if entity is not an instance of class.

(<=>
      (instance
            ?ENTITY
            (ComplementFn ?CLASS))
      (not
            (instance ?ENTITY ?CLASS)))

entity is an instance of "the union of all the elements of superclass" if and only if there exists superclass class so that entity is an instance of class.

(<=>
      (instance
            ?ENTITY
            (GeneralizedUnionFn ?SUPERCLASS))
      (exists
            (?CLASS)
            (and
                  (instance ?CLASS ?SUPERCLASS)
                  (instance ?ENTITY ?CLASS))))

entity is an instance of "the intersection of all the elements of superclass" if and only if for all class holds: if class is an instance of superclass, then entity is an instance of class.

(<=>
      (instance
            ?ENTITY
            (GeneralizedIntersectionFn ?SUPERCLASS))
      (forall
            (?CLASS)
            (=>
                  (instance ?CLASS ?SUPERCLASS)
                  (instance ?ENTITY ?CLASS))))

subclass is an instance of "all subclasses of class" if and only if subclass is a subclass of class.

(<=>
      (instance
            ?SUBCLASS
            (PowerSetFn ?CLASS))
      (subclass ?SUBCLASS ?CLASS))