<=> (<=>)

The truth-functional connective of bi-implication.

Ontologie

SUMO / STRUCTURAL-ONTOLOGY

Class(es)

logický operátor

<=>

Související termín(y)

=> and entails exists forall not or

Typy argumentů

<=>(formule, formule)

Axiomy (101)

Jestliže rel1 je inverzní k rel2, potom pro všechny inst1,inst2 platí: rel1(inst1,inst2) holds tehdy a jen tehdy pokud rel2(inst2,inst1) holds.

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

subclass je podtřídou class tehdy a jen tehdy pokud

subclass je instancí třídy množina nebo třída
class je instancí třídy množina nebo třída
pro všechny inst platí: jestliže inst je instancí třídy subclass, potom inst je instancí třídy class

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

Jestliže thing1 se rovná thing2, potom pro všechny attr platí: thing1 má atribut attr tehdy a jen tehdy pokud thing2 má atribut attr.

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

Jestliže attr1 se rovná attr2, potom pro všechny thing platí: thing má atribut attr1 tehdy a jen tehdy pokud thing má atribut attr2.

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

Jestliže thing1 se rovná thing2, potom pro všechny class platí: thing1 je instancí třídy class tehdy a jen tehdy pokud thing2 je instancí třídy class.

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

Jestliže class1 se rovná class2, potom pro všechny thing platí: thing je instancí třídy class1 tehdy a jen tehdy pokud thing je instancí třídy class2.

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

Jestliže rel1 se rovná rel2, potom pro všechny platí: rel1() holds tehdy a jen tehdy pokud rel2() holds.

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

jestliže obj1 se rovná obj2,
potom jestliže obj1 se rovná "numberth element of "()"" a obj2 se rovná "numberth element of "()"" a "()" se rovná "()", potom () holds tehdy a jen tehdy pokud () 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 je disjoint from class2 tehdy a jen tehdy pokud

class1 je instancí třídy množina nebo třída
class2 je instancí třídy množina nebo třída
pro všechny inst platí: inst není instancí třídy class1 nebo inst není instancí třídy class2

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

je exhaustively partitioned into tehdy a jen tehdy pokud je covered by a je disjointly decomposed into .

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

phys je instancí třídy fyzický objekt tehdy a jen tehdy pokud existují loc,time tak, že phys je located at loc a phys exists during time.

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

obj1 je vlastní částí obj2 tehdy a jen tehdy pokud obj1 je částí obj2 a obj2 není částí obj1.

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

coll1 je a proper sub-collection of coll2 tehdy a jen tehdy pokud

coll1 je instancí třídy kolekce
coll2 je instancí třídy kolekce
pro všechny member platí: jestliže member je a členem coll1, potom member je a členem coll2

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

agent je instancí třídy původce tehdy a jen tehdy pokud existuje proc tak, že agent je původcem proc.

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

abs je instancí třídy abstraktum tehdy a jen tehdy pokud neexistuje point tak, že abs je located at point nebo abs exists during point.

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

"abstraction fn(class)" se rovná attr tehdy a jen tehdy pokud pro všechny inst platí: inst je instancí třídy class tehdy a jen tehdy pokud inst má atribut attr.

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

"extension fn(attribute)" se rovná class tehdy a jen tehdy pokud "abstraction fn(class)" se rovná attribute.

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

number1 je menší než nebo roven number2 tehdy a jen tehdy pokud number1 se rovná number2 nebo number1 je menší než number2.

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

number1 je větší než nebo roven number2 tehdy a jen tehdy pokud number1 se rovná number2 nebo number1 je větší než number2.

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

number je instancí třídy nezáporné reálné číslo tehdy a jen tehdy pokud number je větší než nebo roven a number je instancí třídy reálné číslo.

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

number je instancí třídy kladné reálné číslo tehdy a jen tehdy pokud number je větší než a number je instancí třídy reálné číslo.

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

number je instancí třídy záporné reálné číslo tehdy a jen tehdy pokud number je menší než a number je instancí třídy reálné číslo.

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

Jestliže rel je instancí třídy relace, potom rel() holds tehdy a jen tehdy pokud rel() platí.

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

rel je instancí třídy relace s jedinou hodnotou tehdy a jen tehdy pokud pro všechny ,item1,item2 platí: jestliže rel(,item1) holds a rel(,item2) holds, potom item1 se rovná item2.

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

rel je instancí třídy úplná relace tehdy a jen tehdy pokud existuje valence tak, že rel je instancí třídy relace a rel has valence argument(s) a

jestliže pro všechny number,element,class platí: jestliže number je menší než valence a numberth argument of rel je an instance of class a element se rovná "numberth element of "()"", potom element je instancí třídy class,
potom existuje item tak, že 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 je instancí třídy seznam bez duplicit tehdy a jen tehdy pokud pro všechny number1,number2 platí: jestliže "number1th element of list" se rovná "number2th element of list", potom number1 se rovná number2.

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

list se rovná null list tehdy a jen tehdy pokud neexistuje item tak, že item je a member of list.

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

Jestliže "length of list" se rovná number1, potom pro všechny number2 platí: existuje item tak, že "number2th element of list" se rovná item tehdy a jen tehdy pokud number2 je menší než nebo roven number1.

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

list3 se rovná "list concatenate fn(list1,list2)" tehdy a jen tehdy pokud pro všechny number1,number2 platí: jestliže number1 je menší než nebo roven "length of list1" a number2 je menší než nebo roven "length of list2" a number1 je instancí třídy kladné celé číslo a number2 je instancí třídy kladné celé číslo, potom "number1th element of list3" se rovná "number1th element of list1" a ""("length of list1"+number2)"th element of list3" se rovná "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 je a member of list tehdy a jen tehdy pokud existuje number tak, že "numberth element of list" se rovná item.

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

relation je total ordering on class tehdy a jen tehdy pokud relation je partial ordering on class a relation je trichotomizing on class.

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

"místo kde thing byl v čase time" se rovná region tehdy a jen tehdy pokud thing je přesně umístěn v region během time.

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

obj je instancí třídy "belongings of person" tehdy a jen tehdy pokud person posesses obj.

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

subsumes content class(class1,class2) platí a subsumes content class(class2,class1) platí tehdy a jen tehdy pokud equivalent content class(class1,class2) platí.

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

subsumes content class(class1,class2) platí tehdy a jen tehdy pokud pro všechny obj2,info platí: jestliže obj2 je instancí třídy class2 a obj2 contains information info, potom existuje class1 obj1 tak, že 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))))))

subsumes content instance(obj1,obj2) platí a subsumes content instance(obj2,obj1) platí tehdy a jen tehdy pokud equivalent content instance(obj1,obj2) platí.

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

subsumes content instance(obj1,obj2) platí tehdy a jen tehdy pokud pro všechny info platí: jestliže obj2 contains information info, potom obj1 contains information info.

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

expressed in language(express,language) platí tehdy a jen tehdy pokud existuje prop tak, že represents in language(express,prop,language) platí.

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

"absolute value fn(number1)" se rovná number2 a number1 je instancí třídy reálné číslo a number2 je instancí třídy reálné číslo tehdy a jen tehdy pokud

number1 je instancí třídy nezáporné reálné číslo a number1 se rovná number2
number1 je instancí třídy záporné reálné číslo a number2 se rovná "(-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" se rovná number tehdy a jen tehdy pokud "(""floor fn(number1/number2)"*number2"+number)" se rovná number1.

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

Jestliže pro všechny element platí: element je an element of set1 tehdy a jen tehdy pokud element je an element of set2, potom set1 se rovná set2.

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

graph je instancí třídy cyklus tehdy a jen tehdy pokud existuje node tak, že "the beginning of graph" se rovná node a "the end of graph" se rovná node.

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

graph je instancí třídy multigraf tehdy a jen tehdy pokud existují arc1,arc2,node1,node2 tak, že arc1 je částí graph a arc2 je částí graph a node1 je částí graph a node2 je částí graph a arc1 spojuje node1 a node2 a arc2 spojuje node1 a node2 a arc1 se nerovná 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 je instancí třídy pseudograf tehdy a jen tehdy pokud existuje smyčka grafu loop tak, že loop je částí graph.

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

loop je instancí třídy smyčka grafu tehdy a jen tehdy pokud existuje node tak, že loop spojuje node a node.

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

Jestliže path je částí graph a graph není instancí třídy orientovaný graf, potom "graph path fn(node1,node2)" se rovná path tehdy a jen tehdy pokud "graph path fn(node2,node1)" se rovná path.

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

quantity je instancí třídy "interval fn(from,to)" tehdy a jen tehdy pokud quantity je větší než nebo roven from a quantity je menší než nebo roven to.

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

"value of belongings of person" se rovná amount tehdy a jen tehdy pokud value of "belongings of person" je amount.

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

pos je a part of doba existence thing tehdy a jen tehdy pokud thing exists during pos.

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

interval1 starts interval2 tehdy a jen tehdy pokud "the beginning of interval1" se rovná "the beginning of interval2" a "the end of interval1" happens before the end of interval2.

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

interval1 finishes interval2 tehdy a jen tehdy pokud "the beginning of interval2" happens before the beginning of interval1 a "the end of interval2" se rovná "the end of interval1".

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

point2 je between point1 and point3 tehdy a jen tehdy pokud point1 happens before point2 a point2 happens before point3.

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

point2 je between or at point1 and point3 tehdy a jen tehdy pokud point1 happen?{s} before or at point2 a point2 happen?{s} before or at point3.

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

phys exists during time a time je instancí třídy okamžik tehdy a jen tehdy pokud time je between or at "the beginning of doba existence phys" and "the end of doba existence phys".

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

interval2 overlaps interval1 tehdy a jen tehdy pokud existuje časový interval interval3 tak, že interval3 je a part of interval1 a interval3 je a part of interval2.

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

interval1 meets interval2 tehdy a jen tehdy pokud "the end of interval1" se rovná "the beginning of interval2".

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

interval1 happens earlier than interval2 tehdy a jen tehdy pokud "the end of interval1" happens before the beginning of interval2.

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

phys1 occurs at the same time as phys2 tehdy a jen tehdy pokud "doba existence phys1" se rovná "doba existence phys2".

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

Jestliže "interval between point1 and point2" se rovná interval, potom pro všechny point platí: point je between or at point1 and point2 tehdy a jen tehdy pokud point je a part of interval.

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

obj je instancí třídy spojitý objekt tehdy a jen tehdy pokud pro všechny part1,part2 platí: jestliže obj se rovná "mereological sum fn(part1,part2)", potom part1 je spojen s part2.

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

obj1 spojuje obj2 a obj3 tehdy a jen tehdy pokud obj1 je spojen s obj2 a obj1 je spojen s obj3 a obj2 není spojen s obj3.

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

obj1 se překrývá s obj2 tehdy a jen tehdy pokud existuje obj3 tak, že obj3 je částí obj1 a obj3 je částí obj2.

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

obj1 se částečně překrývá s obj2 tehdy a jen tehdy pokud

obj1 není částí obj2
obj2 není částí obj1
existuje obj3 tak, že obj3 je částí obj1 a obj3 je částí obj2

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

width(object,width) platí tehdy a jen tehdy pokud existují side1,side2 tak, že side(side1,object) platí a side(side2,object) platí a distance(side1,side2,width) platí.

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

Jestliže obj3 se rovná "mereological sum fn(obj1,obj2)", potom pro všechny part platí: part je částí obj3 tehdy a jen tehdy pokud part je částí obj1 nebo part je částí obj2.

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

Jestliže obj3 se rovná "mereological product fn(obj1,obj2)", potom pro všechny part platí: part je částí obj3 tehdy a jen tehdy pokud part je částí obj1 a part je částí obj2.

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

Jestliže obj3 se rovná "mereological difference fn(obj1,obj2)", potom pro všechny part platí: part je částí obj3 tehdy a jen tehdy pokud part je částí obj1 a part není částí obj2.

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

hole je instancí třídy díra tehdy a jen tehdy pokud existuje obj tak, že hole je díra v obj.

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

Jestliže obj1 se rovná "principal host fn(hole)", potom pro všechny obj2 platí: obj2 se překrývá s obj1 tehdy a jen tehdy pokud existuje obj3 tak, že hole je díra v obj3 a obj2 se překrývá s obj3.

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

fillable je atributem hole1 tehdy a jen tehdy pokud existuje díra hole2 tak, že hole1 je částí hole2.

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

Jestliže obj1 se rovná "skin fn(hole)", potom pro všechny obj2 platí: obj2 se překrývá s obj1 tehdy a jen tehdy pokud existuje obj3 tak, že obj3 je a minimální částí "principal host fn(hole)" a hole se dotýká obj3 a obj2 se překrývá s obj3.

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

inj je instancí třídy zranění tehdy a jen tehdy pokud inj je instancí třídy poškození a organismus je účastníkem inj.

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

Existuje půjčování si borrow tak, že agent1 je původcem borrow a borrow začíná v agent2 a object je účastníkem borrow tehdy a jen tehdy pokud existuje půjčování lend tak, že agent2 je původcem lend a lend končí v agent1 a object je účastníkem 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))))

Existuje kupování buy tak, že agent1 je původcem buy a buy začíná v agent2 a object je účastníkem buy tehdy a jen tehdy pokud existuje prodávání sell tak, že agent2 je původcem sell a sell končí v agent1 a object je účastníkem 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 je instancí třídy zničení tehdy a jen tehdy pokud existuje patient tak, že patient je účastníkem process a patient exists during "právě před doba existence process" a patient doesn't exist during "právě po doba existence process".

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

combine je instancí třídy spojení a obj1 je nástrojem pro combine a obj2 je výsledkem combine tehdy a jen tehdy pokud obj1 není částí obj2 právě před doba existence combine a obj1 je částí obj2 právě po doba existence 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 je instancí třídy sloučenina tehdy a jen tehdy pokud existují elementární látka element1,elementární látka element2,chemická syntéza process tak, že element1 se nerovná element2 a element1 je nástrojem pro process a element2 je nástrojem pro process a compound je výsledkem 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 je instancí třídy vytváření tehdy a jen tehdy pokud existuje patient tak, že patient je účastníkem process a patient exists during "právě po doba existence process" a patient doesn't exist during "právě před doba existence process".

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

Existuje konstrukce build tak, že artifact je výsledkem build tehdy a jen tehdy pokud artifact je instancí třídy nemovitost.

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

Existuje vyzařování světla emit tak, že region je účastníkem emit a region je instancí třídy oblast tehdy a jen tehdy pokud illuminated je atributem region.

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

animal1 je a sibling of animal2 tehdy a jen tehdy pokud existují father,mother tak, že father je a father of animal1 a father je a father of animal2 a mother je a mother of animal1 a mother je a mother of animal2.

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

publishes(org,text) platí tehdy a jen tehdy pokud existuje publikování pub tak, že org je původcem pub a text je účastníkem pub.

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

artifact je instancí třídy artefakt tehdy a jen tehdy pokud existuje tvorba making tak, že artifact je výsledkem making.

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

connected engineering components(comp1,comp2) platí tehdy a jen tehdy pokud existuje connection tak, že connects engineering components(connection,comp1,comp2) platí.

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

Jestliže "organization fn(unit)" se rovná org a attr je instancí třídy objektivní atribut, potom attr je atributem unit tehdy a jen tehdy pokud attr je atributem org.

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

obj1 je north vzhledem k obj2 tehdy a jen tehdy pokud obj2 je south vzhledem k obj1.

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

obj1 je east vzhledem k obj2 tehdy a jen tehdy pokud obj2 je west vzhledem k obj1.

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

obj1 je vertical vzhledem k obj2 tehdy a jen tehdy pokud obj2 je horizontal vzhledem k obj1.

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

obj1 je above vzhledem k obj2 tehdy a jen tehdy pokud obj2 je below vzhledem k obj1.

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

obj1 je right vzhledem k obj2 tehdy a jen tehdy pokud obj2 je left vzhledem k obj1.

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

Pro všechny org platí: org doesn't employ person a person je instancí třídy člověk tehdy a jen tehdy pokud unemployed je atributem person.

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

modal attribute(formula,necessity) platí tehdy a jen tehdy pokud modal attribute(formula,possibility) doesn't hold.

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

modal attribute(formula,obligation) platí tehdy a jen tehdy pokud modal attribute(formula,permission) doesn't hold.

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

obj je instancí třídy látka tehdy a jen tehdy pokud existuje skupenství attr tak, že attr je atributem obj.

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

agent je instancí třídy vnímavý agent a living je atributem agent tehdy a jen tehdy pokud existuje stav vědomí attr tak, že attr je atributem agent.

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

entity je instancí třídy "union fn(class1,class2)" tehdy a jen tehdy pokud entity je instancí třídy class1 nebo entity je instancí třídy class2.

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

entity je instancí třídy "intersection fn(class1,class2)" tehdy a jen tehdy pokud entity je instancí třídy class1 a entity je instancí třídy class2.

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

entity je instancí třídy "complement fn(class)" tehdy a jen tehdy pokud entity není instancí třídy class.

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

entity je instancí třídy "generalized union fn(superclass)" tehdy a jen tehdy pokud existuje superclass class tak, že entity je instancí třídy class.

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

entity je instancí třídy "generalized intersection fn(superclass)" tehdy a jen tehdy pokud pro všechny class platí: jestliže class je instancí třídy superclass, potom entity je instancí třídy class.

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

subclass je instancí třídy "all subclasses of class" tehdy a jen tehdy pokud subclass je podtřídou class.

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