<=> (<=>)

The truth-functional connective of bi-implication.

Ontology

SUMO / STRUCTURAL-ONTOLOGY

Class(es)

logischer Operator

<=>

Coordinate term(s)

=> and hatZurFolge exists forall not or

Type restrictions

<=>(Formel, Formel)

Axioms (101)

Wenn rel1 ist eine inverse von rel2 , dann für jeden inst1,inst2 gilt: rel1(inst1,inst2) gilt nur wenn rel2(inst2,inst1) gilt .

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

subclass ist eine teilkategorie von class nur wenn

subclass ist ein fall von Menge oder Kategorie
class ist ein fall von Menge oder Kategorie
für jeden inst gilt: wenn inst ist ein fall von subclass , dann inst ist ein fall von class

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

Wenn thing1 ist gleich thing2 , dann für jeden attr gilt: thing1 hat ein attribut attr nur wenn thing2 hat ein attribut attr .

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

Wenn attr1 ist gleich attr2 , dann für jeden thing gilt: thing hat ein attribut attr1 nur wenn thing hat ein attribut attr2 .

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

Wenn thing1 ist gleich thing2 , dann für jeden class gilt: thing1 ist ein fall von class nur wenn thing2 ist ein fall von class .

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

Wenn class1 ist gleich class2 , dann für jeden thing gilt: thing ist ein fall von class1 nur wenn thing ist ein fall von class2 .

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

Wenn rel1 ist gleich rel2 , dann für jeden gilt: rel1() gilt nur wenn rel2() gilt .

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

wenn obj1 ist gleich obj2 ,
dann wenn obj1 ist gleich "numberte mitglied von "()"" und obj2 ist gleich "numberte mitglied von "()"" und "()" ist gleich "()" , dann () gilt nur wenn () gilt

(=>
      (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 ist dijunkt von class2 nur wenn

class1 ist ein fall von Menge oder Kategorie
class2 ist ein fall von Menge oder Kategorie
für jeden inst gilt: inst ist ein fall von class1 nicht oder inst ist ein fall von class2 nicht

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

wird vollständig in verteilt nur wenn wird mit behandelt und wird zusammenhanglos auf disjunkt.

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

phys ist ein fall von körperlicher Gegenstand nur wenn es gibt ein loc,time der phys befindet sich an und phys besteht während time .

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

obj1 ist ein korrektes teil von obj2 nur wenn obj1 ist ein teil von obj2 und obj2 ist ein teil von obj1 nicht.

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

coll1 ist eine korrekte teilsammlung von coll2 nur wenn

coll1 ist ein fall von Ansammlung
coll2 ist ein fall von Ansammlung
für jeden member gilt: wenn member ist ein Mitglied von coll1 , dann member ist ein Mitglied von coll2

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

agent ist ein fall von Agent nur wenn es gibt ein proc der proc ist der agent von agent .

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

abs ist ein fall von abstrakter Gegenstand nur wenn es gibt kein point der abs befindet sich an oder abs besteht während point .

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

"die beschreibung von class" ist gleich attr nur wenn für jeden inst gilt: inst ist ein fall von class nur wenn inst hat ein attribut attr .

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

"die kategorie, die attribute entspricht" ist gleich class nur wenn "die beschreibung von class" ist gleich attribute .

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

number1 ist kleinerAlsOderGleich number2 nur wenn number1 ist gleich number2 oder number1 ist kleinerAls number2 .

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

number1 ist grösserAlsOderGleich number2 nur wenn number1 ist gleich number2 oder number1 ist grösserAls number2 .

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

number ist ein fall von nichtnegative reelle Zahl nur wenn number ist grösserAlsOderGleich und number ist ein fall von reelle Zahl .

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

number ist ein fall von positive reelle Zahl nur wenn number ist grösserAls und number ist ein fall von reelle Zahl .

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

number ist ein fall von negative reelle Zahl nur wenn number ist kleinerAls und number ist ein fall von reelle Zahl .

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

Wenn rel ist ein fall von Relation , dann rel() gilt nur wenn rel() gilt.

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

rel ist ein fall von einwertige Relation nur wenn für jeden ,item1,item2 gilt: wenn rel(,item1) gilt und rel(,item2) gilt , dann item1 ist gleich item2 .

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

rel ist ein fall von totalwertige Relation nur wenn es gibt ein valence der rel ist ein fall von Relation und rel hat valence argument(e) und

wenn für jeden number,element,class gilt: wenn number ist kleinerAls valence und die Zahl number Argument von rel ist ein fall von class und element ist gleich "numberte mitglied von "()"" , dann element ist ein fall von class ,
dann es gibt ein item der rel(,item) gilt

(<=>
      (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 ist ein fall von einzigartige Liste nur wenn für jeden number1,number2 gilt: wenn "number1te mitglied von list" ist gleich "number2te mitglied von list" , dann number1 ist gleich number2 .

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

list ist gleich null list nur wenn es gibt kein item der item ist ein Mitglied von list.

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

Wenn "Länge von list" ist gleich number1 , dann für jeden number2 gilt: es gibt ein item der "number2te mitglied von list" ist gleich item nur wenn number2 ist kleinerAlsOderGleich number1 .

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

list3 ist gleich "die Liste bestanden aus list1 und list2" nur wenn für jeden number1,number2 gilt: wenn number1 ist kleinerAlsOderGleich "Länge von list1" und number2 ist kleinerAlsOderGleich "Länge von list2" und number1 ist ein fall von positive Ganzzahl und number2 ist ein fall von positive Ganzzahl , dann "number1te mitglied von list3" ist gleich "number1te mitglied von list1" und ""("Länge von list1"+number2)"te mitglied von list3" ist gleich "number2te mitglied von 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 ist ein Mitglied von list nur wenn es gibt ein number der "numberte mitglied von list" ist gleich item .

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

relation ist eine gesampteinrichtung auf class nur wenn relation ist eine teilweise Einrichtung auf class und relation ist eine trichotomizierung auf class .

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

"die Stelle wo thing an time war" ist gleich region nur wenn "thing liegtGenau in region " hält während time .

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

obj ist ein fall von "eigentum von person" nur wenn person besitzt obj .

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

class1 fasst das Inhalt von class2 zusammen und class2 fasst das Inhalt von class1 zusammen nur wenn class1 ist mit class2 gleichwertig.

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

class1 fasst das Inhalt von class2 zusammen nur wenn für jeden obj2,info gilt: wenn obj2 ist ein fall von class2 und obj2 enthält Informationen über info, dann es gibt ein class1 obj1 der obj1 enthält Informationen über info.

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

obj1 fasst das Inhalt von obj2 zusammen und obj2 fasst das Inhalt von obj1 zusammen nur wenn obj1 ist mit obj2 gleichwertig.

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

obj1 fasst das Inhalt von obj2 zusammen nur wenn für jeden info gilt: wenn obj2 enthält Informationen über info, dann obj1 enthält Informationen über info.

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

express ist in Sprache language ausgedrückt nur wenn es gibt ein prop der express ist in Sprache prop ausgedrückt.

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

"der absolutebetrag von number1" ist gleich number2 und number1 ist ein fall von reelle Zahl und number2 ist ein fall von reelle Zahl nur wenn

number1 ist ein fall von nichtnegative reelle Zahl und number1 ist gleich number2
number1 ist ein fall von negative reelle Zahl und number2 ist gleich "(-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 betrag number2" ist gleich number nur wenn "(""die grösste Ganzzahl kleiner als oder Gleichgestelltes zu "number1/number2""*number2"+number)" ist gleich number1 .

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

Wenn für jeden element gilt: element ist ein element von set1 nur wenn element ist ein element von set2 , dann set1 ist gleich set2 .

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

graph ist ein fall von Graphschaltkreis nur wenn es gibt ein node der "der anfang von graph" ist gleich node und "das ende von graph" ist gleich node .

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

graph ist ein fall von Multigraph nur wenn es gibt ein arc1,arc2,node1,node2 der arc1 ist ein teil von graph und arc2 ist ein teil von graph und node1 ist ein teil von graph und node2 ist ein teil von graph und arc1 verbindet node1 und node2 und arc2 verbindet node1 und node2 und arc1 ist gleich arc2 nicht.

(<=>
      (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 ist ein fall von Pseudograph nur wenn es gibt ein Graphschleife loop der loop ist ein teil von graph .

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

loop ist ein fall von Graphschleife nur wenn es gibt ein node der loop verbindet node und node .

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

Wenn path ist ein teil von graph und graph ist ein fall von gerichtetes Graph nicht, dann "die menge von Pfaden zwischen node1 und node2" ist gleich path nur wenn "die menge von Pfaden zwischen node2 und node1" ist gleich path .

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

quantity ist ein fall von "der zeitabstand von from nach to" nur wenn quantity ist grösserAlsOderGleich from und quantity ist kleinerAlsOderGleich to .

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

"wert von dem Eigentum von person" ist gleich amount nur wenn wert von "eigentum von person" ist amount.

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

pos ist ein teil von "die zeit des Bestehens von thing" nur wenn thing besteht während pos .

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

interval1 beginnt interval2 nur wenn "der anfang von interval1" ist gleich "der anfang von interval2" und "das ende von interval1" geschieht vor "das ende von interval2" .

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

interval1 beendet interval2 nur wenn "der anfang von interval2" geschieht vor "der anfang von interval1" und "das ende von interval2" ist gleich "das ende von interval1" .

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

point2 ist zwischen point1 und point3 nur wenn point1 geschieht vor point2 und point2 geschieht vor point3 .

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

point2 ist zwischen oder gleichzeitig mit point1 und point3 nur wenn point1 geschieht vor oder gleichzeitig mit point2 und point2 geschieht vor oder gleichzeitig mit point3 .

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

phys besteht während time und time ist ein fall von Zeitpunkt nur wenn time ist zwischen oder gleichzeitig mit "der anfang von "die zeit des Bestehens von phys"" und "das ende von "die zeit des Bestehens von phys"".

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

interval2 deckt sich mit interval1 nur wenn es gibt ein Zeitabstand interval3 der interval3 ist ein teil von interval1 und interval3 ist ein teil von interval2 .

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

interval1 schliesst interval2 zeitlich an nur wenn "das ende von interval1" ist gleich "der anfang von interval2" .

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

interval1 geschieht früh als interval2 nur wenn "das ende von interval1" geschieht vor "der anfang von interval2" .

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

phys1 geschiecht gleichzeitig mit phys2 nur wenn "die zeit des Bestehens von phys1" ist gleich "die zeit des Bestehens von phys2" .

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

Wenn "abstand zwischen point1 und point2" ist gleich interval , dann für jeden point gilt: point ist zwischen oder gleichzeitig mit point1 und point2 nur wenn point ist ein teil von interval .

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

obj ist ein fall von selbstverbundener Gegenstand nur wenn für jeden part1,part2 gilt: wenn obj ist gleich "die vereinigung von den teilen von part1 und part2" , dann part1 wird an part2 angeschlossen.

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

obj1 schleisst obj2 und obj3 an nur wenn obj1 wird an obj2 angeschlossen und obj1 wird an obj3 angeschlossen und obj2 wird an obj3 nicht angeschlossen.

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

obj1 deckt sich mit obj2 räumlich nur wenn es gibt ein obj3 der obj3 ist ein teil von obj1 und obj3 ist ein teil von obj2 .

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

obj1 deckt sich mit obj2 teilweise nur wenn

obj1 ist ein teil von obj2 nicht
obj2 ist ein teil von obj1 nicht
es gibt ein obj3 der obj3 ist ein teil von obj1 und obj3 ist ein teil von obj2

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

Die breite von object ist width nur wenn es gibt ein side1,side2 der eine seite von object ist side1 und eine seite von object ist side2 und der abstand zwischen side1 und side2 ist width.

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

Wenn obj3 ist gleich "die vereinigung von den teilen von obj1 und obj2" , dann für jeden part gilt: part ist ein teil von obj3 nur wenn part ist ein teil von obj1 oder part ist ein teil von obj2 .

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

Wenn obj3 ist gleich "der durchschnitt von den teilen von obj1 und obj2" , dann für jeden part gilt: part ist ein teil von obj3 nur wenn part ist ein teil von obj1 und part ist ein teil von obj2 .

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

Wenn obj3 ist gleich "die differenz zwischen den Teilen von obj1 und obj2" , dann für jeden part gilt: part ist ein teil von obj3 nur wenn part ist ein teil von obj1 und part ist ein teil von obj2 nicht.

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

hole ist ein fall von Loch nur wenn es gibt ein obj der hole ist ein loch in obj .

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

Wenn obj1 ist gleich "der wirt von dem Loch hole" , dann für jeden obj2 gilt: obj2 deckt sich mit obj1 räumlich nur wenn es gibt ein obj3 der hole ist ein loch in obj3 und obj2 deckt sich mit obj3 räumlich .

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

fillable ist ein attribut von hole1 nur wenn es gibt ein Loch hole2 der hole1 ist ein teil von hole2 .

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

Wenn obj1 ist gleich "die oberfläche von dem Loch hole" , dann für jeden obj2 gilt: obj2 deckt sich mit obj1 räumlich nur wenn es gibt ein obj3 der obj3 ist ein oberflächliches teil von "der wirt von dem Loch hole" und hole schliesst obj3 räumlich an und obj2 deckt sich mit obj3 räumlich .

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

inj ist ein fall von Verletzen nur wenn inj ist ein fall von Beschädigen und Organismus ist ein patient von inj .

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

Es gibt ein Borgen borrow der borrow ist der agent von agent1 und borrow beginnet an agent2 und object ist ein patient von borrow nur wenn es gibt ein Verleihen lend der lend ist der agent von agent2 und lend endet an agent1 und object ist ein patient von 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))))

Es gibt ein Kaufen buy der buy ist der agent von agent1 und buy beginnet an agent2 und object ist ein patient von buy nur wenn es gibt ein Verkaufen sell der sell ist der agent von agent2 und sell endet an agent1 und object ist ein patient von 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 ist ein fall von Zerstörung nur wenn es gibt ein patient der patient ist ein patient von process und patient besteht während "direkt vor "die zeit des Bestehens von process"" und patient besteht während "sofort nach "die zeit des Bestehens von process"" nicht.

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

combine ist ein fall von Kombinieren und obj1 ist ein hilfmittel für combine und obj2 ist ein resultat von combine nur wenn "obj1 ist ein teil von obj2 nicht" hält während "direkt vor "die zeit des Bestehens von combine"" und "obj1 ist ein teil von obj2 " hält während "sofort nach "die zeit des Bestehens von 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 ist ein fall von Verbindung nur wenn es gibt ein elementare Substanz element1,elementare Substanz element2,chemische Synthese process der element1 ist gleich element2 nicht und element1 ist ein hilfmittel für process und element2 ist ein hilfmittel für process und compound ist ein resultat von 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 ist ein fall von Kreation nur wenn es gibt ein patient der patient ist ein patient von process und patient besteht während "sofort nach "die zeit des Bestehens von process"" und patient besteht während "direkt vor "die zeit des Bestehens von process"" nicht.

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

Es gibt ein Konstruieren build der artifact ist ein resultat von build nur wenn artifact ist ein fall von feststehendes Kunstprodukt .

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

Es gibt ein ausstrahlendes Licht emit der region ist ein patient von emit und region ist ein fall von Gebiet nur wenn illuminated ist ein attribut von region .

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

animal2 ist die geschwister von animal1 nur wenn es gibt ein father,mother der father ist der vater von animal1 und father ist der vater von animal2 und mother ist die mutter von animal1 und mother ist die mutter von animal2 .

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

org veröffentlicht text nur wenn es gibt ein Publikation pub der pub ist der agent von org und text ist ein patient von pub .

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

artifact ist ein fall von Kunstprodukt nur wenn es gibt ein Bilden making der artifact ist ein resultat von making .

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

comp1 wird mit comp2 angeschlossen nur wenn es gibt ein connection der connection schliesst comp1 und comp2 an.

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

Wenn "die zugelassene organisatorishe Gruppe von unit" ist gleich org und attr ist ein fall von normatives Attribut , dann attr ist ein attribut von unit nur wenn attr ist ein attribut von org .

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

obj1 ist north hinsichlich obj2 nur wenn obj2 ist south hinsichlich obj1 .

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

obj1 ist east hinsichlich obj2 nur wenn obj2 ist west hinsichlich obj1 .

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

obj1 ist vertical hinsichlich obj2 nur wenn obj2 ist horizontal hinsichlich obj1 .

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

obj1 ist above hinsichlich obj2 nur wenn obj2 ist below hinsichlich obj1 .

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

obj1 ist right hinsichlich obj2 nur wenn obj2 ist left hinsichlich obj1 .

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

Für jeden org gilt: org beschäftigt person nicht und person ist ein fall von Mensch nur wenn unemployed ist ein attribut von person .

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

Die Aussage formula hat die modale Kraft von necessity nur wenn die Aussage "formula" hat die modale Kraft von possibility.

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

Die Aussage formula hat die modale Kraft von obligation nur wenn die Aussage "formula" hat die modale Kraft von permission.

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

obj ist ein fall von Substanz nur wenn es gibt ein körperliche Zustand attr der attr ist ein attribut von obj .

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

agent ist ein fall von empfindungsfähiger Agent und living ist ein attribut von agent nur wenn es gibt ein Bewusstseinsattribut attr der attr ist ein attribut von agent .

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

entity ist ein fall von "die vereinigung von class1 und class2" nur wenn entity ist ein fall von class1 oder entity ist ein fall von class2 .

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

entity ist ein fall von "der durchschnitt von class1 und class2" nur wenn entity ist ein fall von class1 und entity ist ein fall von class2 .

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

entity ist ein fall von "die ergänzung von class" nur wenn entity ist ein fall von class nicht.

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

entity ist ein fall von "die vereinigung aller Elementen von superclass" nur wenn es gibt ein superclass class der entity ist ein fall von class .

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

entity ist ein fall von "der durchschnitt aller Elementen von superclass" nur wenn für jeden class gilt: wenn class ist ein fall von superclass , dann entity ist ein fall von class .

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

subclass ist ein fall von "alle teilkategorien von class" nur wenn subclass ist eine teilkategorie von class.

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