若且唯若 (<=>)

The truth-functional connective of bi-implication.

Ontology

SUMO / STRUCTURAL-ONTOLOGY

Class(es)

邏輯運算元

若且唯若

Coordinate term(s)

若和推知存在所有非或

Type restrictions

<=>(SUO-KIF表述式, SUO-KIF表述式)

Axioms (101)

If rel1 是 rel2 的倒序, then for all inst1,inst2 holds: rel1(inst1,inst2) (不) 成立s if and only if rel2(inst2,inst1) (不) 成立s.

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

subclass 是 class 的次種類 if and only if

subclass 是集合或種類的實例
class 是集合或種類的實例
for all inst holds: if inst 是 subclass 的實例, then inst 是 class 的實例

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

If thing1 等於 thing2, then for all attr holds: thing1 有屬性 attr if and only if thing2 有屬性 attr.

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

If attr1 等於 attr2, then for all thing holds: thing 有屬性 attr1 if and only if thing 有屬性 attr2.

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

If thing1 等於 thing2, then for all class holds: thing1 是 class 的實例 if and only if thing2 是 class 的實例.

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

If class1 等於 class2, then for all thing holds: thing 是 class1 的實例 if and only if thing 是 class2 的實例.

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

If rel1 等於 rel2, then for all holds: rel1() (不) 成立s if and only if rel2() (不) 成立s.

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

if obj1 等於 obj2,
then if obj1 等於 ""()" 的第二元素" and obj2 等於 ""()" 的第二元素" and "()" 等於 "()", then () (不) 成立s if and only if () (不) 成立s

(=>
      (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 無交集於 class2 if and only if

class1 是集合或種類的實例
class2 是集合或種類的實例
for all inst holds: inst 是 class1 的實例 or inst 是 class2 的實例

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

完全分割成 if and only if 被 �]含 and 無交集地分解成 .

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

phys 是物質的的實例 if and only if there exist loc,time so that phys 位於 loc and phys (不) 存在s time 期間.

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

obj1 是 obj2 的正部分 if and only if obj1 是 obj2 的部分) and obj2 是 obj1 的部分).

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

coll1 是 coll2 的正次聚集 if and only if

coll1 是群集的實例
coll2 是群集的實例
for all member holds: if member 是 coll1的成員, then member 是 coll2的成員

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

agent 是施事者的實例 if and only if there exists proc so that proc 是 agent 的施事者.

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

abs 是抽象的的實例 if and only if there doesn't exist point so that abs 位於 point or abs (不) 存在s point 期間.

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

"class 的描述" 等於 attr if and only if for all inst holds: inst 是 class 的實例 if and only if inst 有屬性 attr.

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

"種類符合 attribute" 等於 class if and only if "class 的描述" 等於 attribute.

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

number1 小於或等於 number2 if and only if number1 等於 number2 or number1 小於 number2.

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

number1 大於或等於 number2 if and only if number1 等於 number2 or number1 (不) 大於 number2.

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

number 是非負實數的實例 if and only if number 大於或等於 and number 是實數的實例.

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

number 是正實數的實例 if and only if number (不) 大於 and number 是實數的實例.

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

number 是負實數的實例 if and only if number 小於 and number 是實數的實例.

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

If rel 是關係的實例, then rel() (不) 成立s if and only if rel() holds.

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

rel 是單值關係的實例 if and only if for all ,item1,item2 holds: if rel(,item1) (不) 成立s and rel(,item2) (不) 成立s, then item1 等於 item2.

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

rel 是全值關係的實例 if and only if there exists valence so that rel 是關係的實例 and rel %&有論元(s) valence and

if for all number,element,class holds: if number 小於 valence and rel 的論元 number 是 class 的實例 and element 等於 ""()" 的第二元素", then element 是 class 的實例,
then there exists item so that rel(,item) (不) 成立s

(<=>
      (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 是唯一序列的實例 if and only if for all number1,number2 holds: if "list 的第二元素" 等於 "list 的第二元素", then number1 等於 number2.

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

list 等於空列 if and only if there doesn't exist item so that item 是 list 的一成員.

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

If "list 的長度" 等於 number1, then for all number2 holds: there exists item so that "list 的第二元素" 等於 item if and only if number2 小於或等於 number1.

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

list3 等於 "list1 和 list2 組成的序列" if and only if for all number1,number2 holds: if number1 小於或等於 "list1 的長度" and number2 小於或等於 "list2 的長度" and number1 是正整數的實例 and number2 是正整數的實例, then "list3 的第二元素" 等於 "list1 的第二元素" and "list3 的第二元素" 等於 "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 是 list 的一成員 if and only if there exists number so that "list 的第二元素" 等於 item.

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

relation 全序於 class if and only if relation 偏序於 class and relation 對 class 是三分法.

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

"thing 在 time 的 time位置" 等於 region if and only if thing 精確位於 region timea(之中) time.

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

obj 是 "person 的附屬物" 的實例 if and only if person (沒) 擁有not(s) obj.

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

class1 �]容 class2 and class2 �]容 class1 if and only if class1 訊息等同於 class2.

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

class1 �]容 class2 if and only if for all obj2,info holds: if obj2 是 class2 的實例 and obj2 (不) �]含s) 訊息 %2, then there exists class1 obj1 so that obj1 (不) �]含s) 訊息 %2.

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

obj1 �]容 obj2 and obj2 �]容 obj1 if and only if obj1 訊息等同於 obj2.

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

obj1 �]容 obj2 if and only if for all info holds: if obj2 (不) �]含s) 訊息 %2, then obj1 (不) �]含s) 訊息 %2.

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

express 以 language 語言表達 if and only if there exists prop so that express 以語言 language 呈�{ prop.

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

"number1 的絕對值" 等於 number2 and number1 是實數的實例 and number2 是實數的實例 if and only if

number1 是非負實數的實例 and number1 等於 number2
number1 是負實數的實例 and number2 等於 "(-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 取餘數 number2" 等於 number if and only if "(""最大整數小於或等於 "number1/number2""*number2"+number)" 等於 number1.

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

If for all element holds: element 是 set1 的元素 if and only if element 是 set2 的元素, then set1 等於 set2.

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

graph 是圖形迴路的實例 if and only if there exists node so that "graph 的最初�`點" 等於 node and "graph 的最後�`點" 等於 node.

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

graph 是多圖的實例 if and only if there exist arc1,arc2,node1,node2 so that arc1 是 graph 的部分 and arc2 是 graph 的部分 and node1 是 graph 的部分 and node2 是 graph 的部分 and arc1 (沒) 連結not(s) node1 和 node2 and arc2 (沒) 連結not(s) node1 和 node2 and arc1 等於 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 是擬圖的實例 if and only if there exists 圖迴圈 loop so that loop 是 graph 的部分.

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

loop 是圖迴圈的實例 if and only if there exists node so that loop (沒) 連結not(s) node 和 node.

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

If path 是 graph 的部分 and graph 是有向圖的實例, then "node1 和 node2 間集合路�|" 等於 path if and only if "node2 和 node1 間集合路�|" 等於 path.

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

quantity 是 "從 from 到 to 的間隔" 的實例 if and only if quantity 大於或等於 from and quantity 小於或等於 to.

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

"person 的財產的價值" 等於 amount if and only if "person 的附屬物" 的價值是 amount.

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

pos 是 "thing 存在的時間" 的部分 if and only if thing (不) 存在s pos 期間.

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

interval1 (沒) �}始s interval2 if and only if "interval1 的 �}始" 等於 "interval2 的 �}始" and "interval1 的結束" (沒) 發生?{s} 在 "interval2 的結束" 之前.

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

interval1 (沒) 完成s interval2 if and only if "interval2 的 �}始" (沒) 發生?{s} 在 "interval1 的 �}始" 之前 and "interval2 的結束" 等於 "interval1 的結束".

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

point2 在 point1 和 point3 之間 if and only if point1 (沒) 發生?{s} 在 point2 之前 and point2 (沒) 發生?{s} 在 point3 之前.

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

point2 在 point1 和 point3 或之間 if and only if point1 (沒) 發生?{s} 在 point2 或之前 and point2 (沒) 發生?{s} 在 point3 或之前.

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

phys (不) 存在s time 期間 and time 是時點的實例 if and only if time 在 ""phys 存在的時間" 的 �}始" 和 ""phys 存在的時間" 的結束" 或之間 .

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

interval2 (沒) 與 1 ?重疊s if and only if there exists 時段 interval3 so that interval3 是 interval1 的部分 and interval3 是 interval2 的部分.

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

interval1 (沒) 相接s interval2 if and only if "interval1 的結束" 等於 "interval2 的 �}始".

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

interval1 (沒) 比 interval2 較早發生not(s) if and only if "interval1 的結束" (沒) 發生?{s} 在 "interval2 的 �}始" 之前.

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

phys1 (沒) 與 phys2 同時發生not(s) if and only if "phys1 存在的時間" 等於 "phys2 存在的時間".

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

If "point1 和 point2 的間距" 等於 interval, then for all point holds: point 在 point1 和 point2 或之間 if and only if point 是 interval 的部分.

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

obj 是自身連續物體的實例 if and only if for all part1,part2 holds: if obj 等於 "part1 和 part2 的聯集", then part1 與 part2 相連.

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

obj1 連結 obj2 和 obj3 if and only if obj1 與 obj2 相連 and obj1 與 obj3 相連 and obj2 與 obj3 相連.

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

obj1 (沒) 與 obj2 重�|s if and only if there exists obj3 so that obj3 是 obj1 的部分) and obj3 是 obj2 的部分).

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

obj1 (沒) 與 obj2 部分重�|s if and only if

obj1 是 obj2 的部分)
obj2 是 obj1 的部分)
there exists obj3 so that obj3 是 obj1 的部分) and obj3 是 obj2 的部分)

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

object 的寬度是 width if and only if there exist side1,side2 so that object 的側面是 side1 and object 的側面是 side2 and side1 和 side2 之間距離是 width.

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

If obj3 等於 "obj1 和 obj2 的聯集", then for all part holds: part 是 obj3 的部分) if and only if part 是 obj1 的部分) or part 是 obj2 的部分).

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

If obj3 等於 "obj1 和 obj2 的交集", then for all part holds: part 是 obj3 的部分) if and only if part 是 obj1 的部分) and part 是 obj2 的部分).

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

If obj3 等於 "obj1 和 obj2 的差異", then for all part holds: part 是 obj3 的部分) if and only if part 是 obj1 的部分) and part 是 obj2 的部分).

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

hole 是洞的實例 if and only if there exists obj so that hole 在 obj 是 �}.

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

If obj1 等於 "洞 hole 的主體", then for all obj2 holds: obj2 (沒) 與 obj1 重�|s if and only if there exists obj3 so that hole 在 obj3 是 �} and obj2 (沒) 與 obj3 重�|s.

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

可填充的是 hole1 的屬性 if and only if there exists 洞 hole2 so that hole1 是 hole2 的部分).

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

If obj1 等於 "洞 hole 的表皮", then for all obj2 holds: obj2 (沒) 與 obj1 重�|s if and only if there exists obj3 so that obj3 是 "洞 hole 的主體"的 �~表部分 and hole (沒) 接觸s obj3 and obj2 (沒) 與 obj3 重�|s.

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

inj 是傷害的實例 if and only if inj 是損害的實例 and 生物體是 inj 的受事者.

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

There exists 借取 borrow so that borrow 是 agent1 的施事者 and borrow (不) �_源s 於 agent2 and object 是 borrow 的受事者 if and only if there exists 借予 lend so that lend 是 agent2 的施事者 and lend (不) 終結not(s) agent1 and object 是 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 買 buy so that buy 是 agent1 的施事者 and buy (不) �_源s 於 agent2 and object 是 buy 的受事者 if and only if there exists 銷售 sell so that sell 是 agent2 的施事者 and sell (不) 終結not(s) agent1 and object 是 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 是毀滅的實例 if and only if there exists patient so that patient 是 process 的受事者 and patient (不) 存在s ""process 存在的時間" 不久之前" 期間 and patient not(不) 存在 ""process 存在的時間" 不久之後" 期間.

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

combine 是結合的實例 and obj1 對 combine 是資源 and obj2 是 combine 的結果 if and only if obj1 是 obj2 的部分) ""combine 存在的時間" 不久之前"a(之中) "combine 存在的時間" 不久之前 and obj1 是 obj2 的部分) ""combine 存在的時間" 不久之後"a(之中) "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 是化合物的實例 if and only if there exist 基本物質 element1,基本物質 element2,化學合成 process so that element1 等於 element2 and element1 對 process 是資源 and element2 對 process 是資源 and compound 是 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 是產生的實例 if and only if there exists patient so that patient 是 process 的受事者 and patient (不) 存在s ""process 存在的時間" 不久之後" 期間 and patient not(不) 存在 ""process 存在的時間" 不久之前" 期間.

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

There exists 建構 build so that artifact 是 build 的結果 if and only if artifact 是固定人造物的實例.

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

There exists 光線 emit so that region 是 emit 的受事者 and region 是區域的實例 if and only if 被光照的是 region 的屬性.

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

animal1 是 animal2 的兄弟姊妹 if and only if there exist father,mother so that father 是 animal1 的父親 and father 是 animal2 的父親 and mother 是 animal1 的母親 and mother 是 animal2 的母親.

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

org 出版 text if and only if there exists 出版 pub so that pub 是 org 的施事者 and text 是 pub 的受事者.

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

artifact 是人造物的實例 if and only if there exists 製作 making so that artifact 是 making 的結果.

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

comp1 與 comp2 連結 if and only if there exists connection so that connection 連結 comp1 和 comp2.

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

If "unit 的合法組織實體 " 等於 org and attr 是規範屬性的實例, then attr 是 unit 的屬性 if and only if attr 是 org 的屬性.

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

obj1 對 obj2 是北方 if and only if obj2 對 obj1 是南方.

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

obj1 對 obj2 是東方 if and only if obj2 對 obj1 是西方.

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

obj1 對 obj2 是垂直的 if and only if obj2 對 obj1 是水平線.

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

obj1 對 obj2 是在...之上 if and only if obj2 對 obj1 是在...之下.

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

obj1 對 obj2 是右邊 if and only if obj2 對 obj1 是左邊.

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

For all org holds: org not(沒) 雇用(s) person and person 是人類的實例 if and only if 失業的是 person 的屬性.

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

陳述 formula 有必要性的型態意義 if and only if 陳述 "formula" 有可能性的型態意義.

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

陳述 formula 有義務的型態意義 if and only if 陳述 "formula" 有許可的型態意義.

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

obj 是物質的實例 if and only if there exists 物理狀態 attr so that attr 是 obj 的屬性.

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

agent 是能知覺的行為主體的實例 and 活的是 agent 的屬性 if and only if there exists 意識屬性 attr so that attr 是 agent 的屬性.

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

entity 是 "class1 和 class2 的聯集" 的實例 if and only if entity 是 class1 的實例 or entity 是 class2 的實例.

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

entity 是 "class1 和 class2 的聯集" 的實例 if and only if entity 是 class1 的實例 and entity 是 class2 的實例.

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

entity 是 "class 的互補" 的實例 if and only if entity 是 class 的實例.

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

entity 是 "superclass 的所有元素的聯集" 的實例 if and only if there exists superclass class so that entity 是 class 的實例.

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

entity 是 "superclass 的所有元素的交集" 的實例 if and only if for all class holds: if class 是 superclass 的實例, then entity 是 class 的實例.

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

subclass 是 "class 的所有次種類" 的實例 if and only if subclass 是 class 的次種類.

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