若 (=>)

The truth-functional connective of implication.

Ontology

SUMO / STRUCTURAL-ONTOLOGY

Class(es)

邏輯運算元

若

Coordinate term(s)

若且唯若和推知存在所有非或

Type restrictions

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

Related WordNet synsets

See more related synsets on a separate page.

Axioms (679)

If entity 是 class 的直接實例, then there doesn't exist class subclass so that entity 是 subclass 的實例.

(=>
      (immediateInstance ?ENTITY ?CLASS)
      (not
            (exists
                  (?SUBCLASS)
                  (and
                        (subclass ?SUBCLASS ?CLASS)
                        (instance ?ENTITY ?SUBCLASS)))))

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 class1 是 class2 的直接次種類, then there doesn't exist class2 class3 so that class1 是 class3 的次種類 and class2 等於 class3 and class1 等於 class3.

(=>
      (immediateSubclass ?CLASS1 ?CLASS2)
      (not
            (exists
                  (?CLASS3)
                  (and
                        (subclass ?CLASS3 ?CLASS2)
                        (subclass ?CLASS1 ?CLASS3)
                        (not
                              (equal ?CLASS2 ?CLASS3))
                        (not
                              (equal ?CLASS1 ?CLASS3))))))

If pred1 是 pred2 的次關係 and pred1 %&有論元(s) number, then pred2 %&有論元(s) number.

(=>
      (and
            (subrelation ?PRED1 ?PRED2)
            (valence ?PRED1 ?NUMBER))
      (valence ?PRED2 ?NUMBER))

If pred1 是 pred2 的次關係 and pred2 的論元 number 是 class1 的實例, then pred1 的論元 number 是 class1 的實例.

(=>
      (and
            (subrelation ?PRED1 ?PRED2)
            (domain ?PRED2 ?NUMBER ?CLASS1))
      (domain ?PRED1 ?NUMBER ?CLASS1))

If rel1 是 rel2 的次關係 and rel1() (不) 成立s, then rel2() (不) 成立s.

(=>
      (and
            (subrelation ?REL1 ?REL2)
            (holds ?REL1 @ROW))
      (holds ?REL2 @ROW))

If pred1 是 pred2 的次關係 and pred2 是 class 的實例 and class 是可繼承關係的實例, then pred1 是 class 的實例.

(=>
      (and
            (subrelation ?PRED1 ?PRED2)
            (instance ?PRED2 ?CLASS)
            (instance ?CLASS InheritableRelation))
      (instance ?PRED1 ?CLASS))

If rel 的論元 number 是 class1 的實例 and rel 的論元 number 是 class2 的實例, then class1 是 class2 的次種類 or class2 是 class1 的次種類.

(=>
      (and
            (domain ?REL ?NUMBER ?CLASS1)
            (domain ?REL ?NUMBER ?CLASS2))
      (or
            (subclass ?CLASS1 ?CLASS2)
            (subclass ?CLASS2 ?CLASS1)))

If rel1 是 rel2 的次關係 and rel2 的論元 number 是 class1 的次種類, then rel1 的論元 number 是 class1 的次種類.

(=>
      (and
            (subrelation ?REL1 ?REL2)
            (domainSubclass ?REL2 ?NUMBER ?CLASS1))
      (domainSubclass ?REL1 ?NUMBER ?CLASS1))

If rel 的論元 number 是 class1 的次種類 and rel 的論元 number 是 class2 的次種類, then class1 是 class2 的次種類 or class2 是 class1 的次種類.

(=>
      (and
            (domainSubclass ?REL ?NUMBER ?CLASS1)
            (domainSubclass ?REL ?NUMBER ?CLASS2))
      (or
            (subclass ?CLASS1 ?CLASS2)
            (subclass ?CLASS2 ?CLASS1)))

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))))

if list1 等於 list2,
then if list1 等於 "()" and list2 等於 "()", then for all number holds: ""()" 的第二元素" 等於 ""()" 的第二元素"

(=>
      (equal ?LIST1 ?LIST2)
      (=>
            (and
                  (equal
                        ?LIST1
                        (ListFn @ROW1))
                  (equal
                        ?LIST2
                        (ListFn @ROW2)))
            (forall
                  (?NUMBER)
                  (equal
                        (ListOrderFn
                              (ListFn @ROW1)
                              ?NUMBER)
                        (ListOrderFn
                              (ListFn @ROW2)
                              ?NUMBER)))))

If function 的範圍是 class 的實例 and "function()" 等於 value, then value 是 class 的實例.

(=>
      (and
            (range ?FUNCTION ?CLASS)
            (equal
                  (AssignmentFn ?FUNCTION @ROW)
                  ?VALUE))
      (instance ?VALUE ?CLASS))

If rel1 是 rel2 的次關係 and rel2 的範圍是 class1 的實例, then rel1 的範圍是 class1 的實例.

(=>
      (and
            (subrelation ?REL1 ?REL2)
            (range ?REL2 ?CLASS1))
      (range ?REL1 ?CLASS1))

If rel 的範圍是 class1 的實例 and rel 的範圍是 class2 的實例, then class1 是 class2 的次種類 or class2 是 class1 的次種類.

(=>
      (and
            (range ?REL ?CLASS1)
            (range ?REL ?CLASS2))
      (or
            (subclass ?CLASS1 ?CLASS2)
            (subclass ?CLASS2 ?CLASS1)))

If 被 function 歸回的值是 class的次種類 and "function()" 等於 value, then value 是 class 的次種類.

(=>
      (and
            (rangeSubclass ?FUNCTION ?CLASS)
            (equal
                  (AssignmentFn ?FUNCTION @ROW)
                  ?VALUE))
      (subclass ?VALUE ?CLASS))

If rel1 是 rel2 的次關係 and 被 rel2 歸回的值是 class1的次種類, then 被 rel1 歸回的值是 class1的次種類.

(=>
      (and
            (subrelation ?REL1 ?REL2)
            (rangeSubclass ?REL2 ?CLASS1))
      (rangeSubclass ?REL1 ?CLASS1))

If 被 rel 歸回的值是 class1的次種類 and 被 rel 歸回的值是 class2的次種類, then class1 是 class2 的次種類 or class2 是 class1 的次種類.

(=>
      (and
            (rangeSubclass ?REL ?CLASS1)
            (rangeSubclass ?REL ?CLASS2))
      (or
            (subclass ?CLASS1 ?CLASS2)
            (subclass ?CLASS2 ?CLASS1)))

If 無交集關係() holds and rel 是 "()" 的一成員, then rel 是關係的實例.

(=>
      (and
            (disjointRelation @ROW)
            (inList
                  ?REL
                  (ListFn @ROW)))
      (instance ?REL Relation))

If 無交集關係() holds and rel1 是 "()" 的一成員 and rel2 是 "()" 的一成員 and rel1 %&有論元(s) number, then rel2 %&有論元(s) number.

(=>
      (and
            (disjointRelation @ROW)
            (inList
                  ?REL1
                  (ListFn @ROW))
            (inList
                  ?REL2
                  (ListFn @ROW))
            (valence ?REL1 ?NUMBER))
      (valence ?REL2 ?NUMBER))

If rel1 的論元 number 是 class1 的實例 and rel2 的論元 number 是 class2 的實例 and class1 無交集於 class2, then 無交集關係(rel1,rel2) holds.

(=>
      (and
            (domain ?REL1 ?NUMBER ?CLASS1)
            (domain ?REL2 ?NUMBER ?CLASS2)
            (disjoint ?CLASS1 ?CLASS2))
      (disjointRelation ?REL1 ?REL2))

If rel1 的論元 number 是 class1 的次種類 and rel2 的論元 number 是 class2 的次種類 and class1 無交集於 class2, then 無交集關係(rel1,rel2) holds.

(=>
      (and
            (domainSubclass ?REL1 ?NUMBER ?CLASS1)
            (domainSubclass ?REL2 ?NUMBER ?CLASS2)
            (disjoint ?CLASS1 ?CLASS2))
      (disjointRelation ?REL1 ?REL2))

If rel1 的範圍是 class1 的實例 and rel2 的範圍是 class2 的實例 and class1 無交集於 class2, then 無交集關係(rel1,rel2) holds.

(=>
      (and
            (range ?REL1 ?CLASS1)
            (range ?REL2 ?CLASS2)
            (disjoint ?CLASS1 ?CLASS2))
      (disjointRelation ?REL1 ?REL2))

If 被 rel1 歸回的值是 class1的次種類 and 被 rel2 歸回的值是 class2的次種類 and class1 無交集於 class2, then 無交集關係(rel1,rel2) holds.

(=>
      (and
            (rangeSubclass ?REL1 ?CLASS1)
            (rangeSubclass ?REL2 ?CLASS2)
            (disjoint ?CLASS1 ?CLASS2))
      (disjointRelation ?REL1 ?REL2))

If 無交集關係() holds and rel1 是 "()" 的一成員 and rel2 是 "()" 的一成員 and rel1 等於 rel2 and rel1() (不) 成立s, then rel2() not(不) 成立.

(=>
      (and
            (disjointRelation @ROW1)
            (inList
                  ?REL1
                  (ListFn @ROW1))
            (inList
                  ?REL2
                  (ListFn @ROW1))
            (not
                  (equal ?REL1 ?REL2))
            (holds ?REL1 @ROW2))
      (not
            (holds ?REL2 @ROW2)))

if 對立於 ?,
then if element 是 "()" 的一成員, then element 是屬性的實例

(=>
      (contraryAttribute @ROW)
      (=>
            (inList
                  ?ELEMENT
                  (ListFn @ROW))
            (instance ?ELEMENT Attribute)))

if 對立於 ?,
then for all attr1,attr2 holds:
- if attr1 等於 ""()" 的第二元素" and attr2 等於 ""()" 的第二元素" and number1 等於 number2,
- then if obj 有屬性 attr1, then obj 有屬性 attr2

(=>
      (contraryAttribute @ROW)
      (forall
            (?ATTR1 ?ATTR2)
            (=>
                  (and
                        (equal
                              ?ATTR1
                              (ListOrderFn
                                    (ListFn @ROW)
                                    ?NUMBER1))
                        (equal
                              ?ATTR2
                              (ListOrderFn
                                    (ListFn @ROW)
                                    ?NUMBER2))
                        (not
                              (equal ?NUMBER1 ?NUMBER2)))
                  (=>
                        (property ?OBJ ?ATTR1)
                        (not
                              (property ?OBJ ?ATTR2))))))

if 窮盡的屬性,
then if attr 是 "()" 的一成員, then attr 是屬性的實例

(=>
      (exhaustiveAttribute ?CLASS @ROW)
      (=>
            (inList
                  ?ATTR
                  (ListFn @ROW))
            (instance ?ATTR Attribute)))

if 窮盡的屬性,
then for all obj holds: if attr1 是 class 的實例, then there exists attr2 so that attr2 是 "()" 的一成員 and attr1 等於 attr2

(=>
      (exhaustiveAttribute ?CLASS @ROW)
      (forall
            (?OBJ)
            (=>
                  (instance ?ATTR1 ?CLASS)
                  (exists
                        (?ATTR2)
                        (and
                              (inList
                                    ?ATTR2
                                    (ListFn @ROW))
                              (equal ?ATTR1 ?ATTR2))))))

if 被 �]含,
then if element 是 "()" 的一成員, then element 是種類的實例

(=>
      (exhaustiveDecomposition @ROW)
      (=>
            (inList
                  ?ELEMENT
                  (ListFn @ROW))
            (instance ?ELEMENT Class)))

if 無交集地分解成 ,
then if element 是 "()" 的一成員, then element 是種類的實例

(=>
      (disjointDecomposition @ROW)
      (=>
            (inList
                  ?ELEMENT
                  (ListFn @ROW))
            (instance ?ELEMENT Class)))

if attr1 是 attr2 的次屬性,
then for all obj holds: if obj 有屬性 attr1, then obj 有屬性 attr2

(=>
      (subAttribute ?ATTR1 ?ATTR2)
      (forall
            (?OBJ)
            (=>
                  (property ?OBJ ?ATTR1)
                  (property ?OBJ ?ATTR2))))

If attr1 是 attr2 的次屬性 and attr2 是 class 的實例, then attr1 是 class 的實例.

(=>
      (and
            (subAttribute ?ATTR1 ?ATTR2)
            (instance ?ATTR2 ?CLASS))
      (instance ?ATTR1 ?CLASS))

If attr1 是 attr2 的續接屬性 and entity 有屬性 attr2 time1a(之中) time1, then there exists time2 so that time2 是 "time1 之前" 的部分 and entity 有屬性 attr1 time2a(之中) time2.

(=>
      (and
            (successorAttribute ?ATTR1 ?ATTR2)
            (holdsDuring
                  ?TIME1
                  (property ?ENTITY ?ATTR2)))
      (exists
            (?TIME2)
            (and
                  (temporalPart
                        ?TIME2
                        (PastFn ?TIME1))
                  (holdsDuring
                        ?TIME2
                        (property ?ENTITY ?ATTR1)))))

If attr1 是 attr2 的續接屬性, then attr1 是 attr2 的封閉續接屬性.

(=>
      (successorAttribute ?ATTR1 ?ATTR2)
      (successorAttributeClosure ?ATTR1 ?ATTR2))

If rel(,inst) (不) 成立s and rel 是函數的實例, then "rel()" 等於 inst.

(=>
      (and
            (holds ?REL @ROW ?INST)
            (instance ?REL Function))
      (equal
            (AssignmentFn ?REL @ROW)
            ?INST))

If class 是種類的實例, then class 是實體的次種類.

(=>
      (instance ?CLASS Class)
      (subclass ?CLASS Entity))

If obj 是自身連續物體的實例, then "obj 的正面" 是 obj 的部分).

(=>
      (instance ?OBJ SelfConnectedObject)
      (part
            (FrontFn ?OBJ)
            ?OBJ))

If obj 是自身連續物體的實例, then "obj 的反面" 是 obj 的部分).

(=>
      (instance ?OBJ SelfConnectedObject)
      (part
            (BackFn ?OBJ)
            ?OBJ))

if substance1 是 substance2 的 �@小部分,
then for all class holds: if substance1 是 class 的實例, then substance2 是 class 的實例

(=>
      (piece ?SUBSTANCE1 ?SUBSTANCE2)
      (forall
            (?CLASS)
            (=>
                  (instance ?SUBSTANCE1 ?CLASS)
                  (instance ?SUBSTANCE2 ?CLASS))))

If objecttype 是物質的次種類 and object 是 objecttype 的實例 and part 是 object 的部分), then part 是 objecttype 的實例.

(=>
      (and
            (subclass ?OBJECTTYPE Substance)
            (instance ?OBJECT ?OBJECTTYPE)
            (part ?PART ?OBJECT))
      (instance ?PART ?OBJECTTYPE))

If obj 是物質的實例 and attr 是 obj 的屬性 and part 是 obj 的部分), then attr 是 part 的屬性.

(=>
      (and
            (instance ?OBJ Substance)
            (attribute ?OBJ ?ATTR)
            (part ?PART ?OBJ))
      (attribute ?PART ?ATTR))

If atom 是原子的實例, then there exist 質子 proton,電子 electron so that proton 是 atom 的元件 and electron 是 atom 的元件.

(=>
      (instance ?ATOM Atom)
      (exists
            (?PROTON ?ELECTRON)
            (and
                  (component ?PROTON ?ATOM)
                  (component ?ELECTRON ?ATOM)
                  (instance ?PROTON Proton)
                  (instance ?ELECTRON Electron))))

if atom 是原子的實例,
then for all nucleus1,nucleus2 holds: if nucleus1 是 atom 的元件 and nucleus2 是 atom 的元件 and nucleus1 是原子核的實例 and nucleus2 是原子核的實例, then nucleus1 等於 nucleus2

(=>
      (instance ?ATOM Atom)
      (forall
            (?NUCLEUS1 ?NUCLEUS2)
            (=>
                  (and
                        (component ?NUCLEUS1 ?ATOM)
                        (component ?NUCLEUS2 ?ATOM)
                        (instance ?NUCLEUS1 AtomicNucleus)
                        (instance ?NUCLEUS2 AtomicNucleus))
                  (equal ?NUCLEUS1 ?NUCLEUS2))))

If particle 是次原子粒子的實例, then there exists 原子 atom so that particle 是 atom 的部分).

(=>
      (instance ?PARTICLE SubatomicParticle)
      (exists
            (?ATOM)
            (and
                  (instance ?ATOM Atom)
                  (part ?PARTICLE ?ATOM))))

If nucleus 是原子核的實例, then there exist 中子 neutron,質子 proton so that neutron 是 nucleus 的元件 and proton 是 nucleus 的元件.

(=>
      (instance ?NUCLEUS AtomicNucleus)
      (exists
            (?NEUTRON ?PROTON)
            (and
                  (component ?NEUTRON ?NUCLEUS)
                  (component ?PROTON ?NUCLEUS)
                  (instance ?NEUTRON Neutron)
                  (instance ?PROTON Proton))))

If mixture 是混合物的實例, then there exist 純物質 pure1,純物質 pure2 so that pure1 等於 pure2 and pure1 是 mixture 的 �@小部分 and pure2 是 mixture 的 �@小部分.

(=>
      (instance ?MIXTURE Mixture)
      (exists
            (?PURE1 ?PURE2)
            (and
                  (subclass ?PURE1 PureSubstance)
                  (subclass ?PURE2 PureSubstance)
                  (not
                        (equal ?PURE1 ?PURE2))
                  (piece ?PURE1 ?MIXTURE)
                  (piece ?PURE2 ?MIXTURE))))

If obj 是複雜體/非單質體的實例, then there exist 物質 substance1,物質 substance2 so that substance1 是由 obj 組成 and substance2 是由 obj 組成 and substance1 等於 substance2.

(=>
      (instance ?OBJ CorpuscularObject)
      (exists
            (?SUBSTANCE1 ?SUBSTANCE2)
            (and
                  (subclass ?SUBSTANCE1 Substance)
                  (subclass ?SUBSTANCE2 Substance)
                  (material ?SUBSTANCE1 ?OBJ)
                  (material ?SUBSTANCE2 ?OBJ)
                  (not
                        (equal ?SUBSTANCE1 ?SUBSTANCE2)))))

If region 是區域的實例, then there exists phys so that phys 位於 region.

(=>
      (instance ?REGION Region)
      (exists
            (?PHYS)
            (located ?PHYS ?REGION)))

If coll 是群集的實例, then there exists obj so that obj 是 coll的成員.

(=>
      (instance ?COLL Collection)
      (exists
            (?OBJ)
            (member ?OBJ ?COLL)))

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)))))

If string 是符號串的實例, then there exists 字元 part so that part 是 string 的部分).

(=>
      (instance ?STRING SymbolicString)
      (exists
            (?PART)
            (and
                  (part ?PART ?STRING)
                  (instance ?PART Character))))

If lang 是動物語言的實例 and proc 是 agent 的施事者 and lang 對 proc 是工具, then agent 是動物的實例 and agent 是人類的實例.

(=>
      (and
            (instance ?LANG AnimalLanguage)
            (agent ?PROC ?AGENT)
            (instrument ?PROC ?LANG))
      (and
            (instance ?AGENT Animal)
            (not
                  (instance ?AGENT Human))))

If lang 是電腦語言的實例 and proc 是 agent 的施事者 and lang 對 proc 是工具, then agent 是機器的實例.

(=>
      (and
            (instance ?LANG ComputerLanguage)
            (agent ?PROC ?AGENT)
            (instrument ?PROC ?LANG))
      (instance ?AGENT Machine))

If lang 是人類語言的實例 and proc 是 agent 的施事者 and lang 對 proc 是工具, then agent 是人類的實例.

(=>
      (and
            (instance ?LANG HumanLanguage)
            (agent ?PROC ?AGENT)
            (instrument ?PROC ?LANG))
      (instance ?AGENT Human))

If lang 是人造語言的實例, then there exists 計畫 plan so that lang 是 plan 的結果.

(=>
      (instance ?LANG ConstructedLanguage)
      (exists
            (?PLAN)
            (and
                  (instance ?PLAN Planning)
                  (result ?PLAN ?LANG))))

If process 是雙受事歷程的實例, then there exist obj1,obj2 so that obj1 是 process 的受事者 and obj2 是 process 的受事者 and obj1 等於 obj2.

(=>
      (instance ?PROCESS DualObjectProcess)
      (exists
            (?OBJ1 ?OBJ2)
            (and
                  (patient ?PROCESS ?OBJ1)
                  (patient ?PROCESS ?OBJ2)
                  (not
                        (equal ?OBJ1 ?OBJ2)))))

If number 是虛數的實例, then there exists 實數 real so that number 等於 "real*" 的平方根"".

(=>
      (instance ?NUMBER ImaginaryNumber)
      (exists
            (?REAL)
            (and
                  (instance ?REAL RealNumber)
                  (equal
                        ?NUMBER
                        (MultiplicationFn
                              ?REAL
                              (SquareRootFn -1))))))

If number 是複數的實例, then there exist 實數 real1,實數 real2 so that number 等於 "(real1+"real2*" 的平方根"")".

(=>
      (instance ?NUMBER ComplexNumber)
      (exists
            (?REAL1 ?REAL2)
            (and
                  (instance ?REAL1 RealNumber)
                  (instance ?REAL2 RealNumber)
                  (equal
                        ?NUMBER
                        (AdditionFn
                              ?REAL1
                              (MultiplicationFn
                                    ?REAL2
                                    (SquareRootFn -1)))))))

If function 是一元恆定函數量的實例, then function 的論元是常量的實例 and function 的範圍是常量的實例.

(=>
      (instance ?FUNCTION UnaryConstantFunctionQuantity)
      (and
            (domain ?FUNCTION 1 ConstantQuantity)
            (range ?FUNCTION ConstantQuantity)))

If function 是時間依變量的實例, then function 的論元是時間單位的實例.

(=>
      (instance ?FUNCTION TimeDependentQuantity)
      (domain ?FUNCTION 1 TimeMeasure))

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))))))

If rel 是二元關係的實例, then there don't exist item1,item2,item3, so that rel(item1,item2,item3,) (不) 成立s.

(=>
      (instance ?REL BinaryRelation)
      (not
            (exists
                  (?ITEM1 ?ITEM2 ?ITEM3 @ROW)
                  (holds ?REL ?ITEM1 ?ITEM2 ?ITEM3 @ROW))))

if rel 是反身關係的實例,
then if rel(inst1,inst2) (不) 成立s or rel(inst2,inst1) (不) 成立s, then rel(inst1,inst1) (不) 成立s

(=>
      (instance ?REL ReflexiveRelation)
      (=>
            (or
                  (holds ?REL ?INST1 ?INST2)
                  (holds ?REL ?INST2 ?INST1))
            (holds ?REL ?INST1 ?INST1)))

If rel 是非反身關係的實例, then for all inst holds: rel(inst,inst) not(不) 成立.

(=>
      (instance ?REL IrreflexiveRelation)
      (forall
            (?INST)
            (not
                  (holds ?REL ?INST ?INST))))

if rel 是對稱關係的實例,
then for all inst1,inst2 holds: if rel(inst1,inst2) (不) 成立s, then rel(inst2,inst1) (不) 成立s

(=>
      (instance ?REL SymmetricRelation)
      (forall
            (?INST1 ?INST2)
            (=>
                  (holds ?REL ?INST1 ?INST2)
                  (holds ?REL ?INST2 ?INST1))))

rel 是二元關係的實例
rel 的論元是 class1 的實例 or rel 的論元是 class1 的次種類
rel 的論元是 class2 的實例 or rel 的論元是 class2 的次種類 or rel 的範圍是 class2 的實例 or 被 rel 歸回的值是 class2的次種類
class1 無交集於 class2

, then rel 是不對稱關係的實例.

(=>
      (and
            (instance ?REL BinaryRelation)
            (or
                  (domain ?REL 1 ?CLASS1)
                  (domainSubclass ?REL 1 ?CLASS1))
            (or
                  (domain ?REL 2 ?CLASS2)
                  (domainSubclass ?REL 2 ?CLASS2)
                  (range ?REL ?CLASS2)
                  (rangeSubclass ?REL ?CLASS2))
            (disjoint ?CLASS1 ?CLASS2))
      (instance ?REL AsymmetricRelation))

if rel 是反對稱關係的實例,
then for all inst1,inst2 holds: if rel(inst1,inst2) (不) 成立s and rel(inst2,inst1) (不) 成立s, then inst1 等於 inst2

(=>
      (instance ?REL AntisymmetricRelation)
      (forall
            (?INST1 ?INST2)
            (=>
                  (and
                        (holds ?REL ?INST1 ?INST2)
                        (holds ?REL ?INST2 ?INST1))
                  (equal ?INST1 ?INST2))))

If rel 是三角關係的實例, then for all inst1,inst2 holds: rel(inst1,inst2) (不) 成立s or inst1 等於 inst2 or rel(inst2,inst1) (不) 成立s.

(=>
      (instance ?REL TrichotomizingRelation)
      (forall
            (?INST1 ?INST2)
            (or
                  (holds ?REL ?INST1 ?INST2)
                  (equal ?INST1 ?INST2)
                  (holds ?REL ?INST2 ?INST1))))

if rel 是可遞關係的實例,
then for all inst1,inst2,inst3 holds: if rel(inst1,inst2) (不) 成立s and rel(inst2,inst3) (不) 成立s, then rel(inst1,inst3) (不) 成立s

(=>
      (instance ?REL TransitiveRelation)
      (forall
            (?INST1 ?INST2 ?INST3)
            (=>
                  (and
                        (holds ?REL ?INST1 ?INST2)
                        (holds ?REL ?INST2 ?INST3))
                  (holds ?REL ?INST1 ?INST3))))

if rel 是非可遞關係的實例,
then for all inst1,inst2,inst3 holds: if rel(inst1,inst2) (不) 成立s and rel(inst2,inst3) (不) 成立s, then rel(inst1,inst3) not(不) 成立

(=>
      (instance ?REL IntransitiveRelation)
      (forall
            (?INST1 ?INST2 ?INST3)
            (=>
                  (and
                        (holds ?REL ?INST1 ?INST2)
                        (holds ?REL ?INST2 ?INST3))
                  (not
                        (holds ?REL ?INST1 ?INST3)))))

If rel 是全序關係的實例, then for all inst1,inst2 holds: rel(inst1,inst2) (不) 成立s or rel(inst2,inst1) (不) 成立s.

(=>
      (instance ?REL TotalOrderingRelation)
      (forall
            (?INST1 ?INST2)
            (or
                  (holds ?REL ?INST1 ?INST2)
                  (holds ?REL ?INST2 ?INST1))))

If process 是歷程的實例, then there exists cause so that process 是 cause 的施事者.

(=>
      (instance ?PROCESS Process)
      (exists
            (?CAUSE)
            (agent ?PROCESS ?CAUSE)))

If formula1 (不）增�[s) %2 的可能性 and "formula2 的或然率" 等於 number1 and formula1 的機率是 formula2 在 formula2 為真的情況下 , then number2 (不) 大於 number1.

(=>
      (and
            (increasesLikelihood ?FORMULA1 ?FORMULA2)
            (equal
                  (ProbabilityFn ?FORMULA2)
                  ?NUMBER1)
            (conditionalProbability ?FORMULA1 ?FORMULA2 ?NUMBER2))
      (greaterThan ?NUMBER2 ?NUMBER1))

If formula1 (不）降低s) %2 的可能性 and "formula2 的或然率" 等於 number1 and formula1 的機率是 formula2 在 formula2 為真的情況下 , then number2 小於 number1.

(=>
      (and
            (decreasesLikelihood ?FORMULA1 ?FORMULA2)
            (equal
                  (ProbabilityFn ?FORMULA2)
                  ?NUMBER1)
            (conditionalProbability ?FORMULA1 ?FORMULA2 ?NUMBER2))
      (lessThan ?NUMBER2 ?NUMBER1))

If formula1 和 formula2 的或然率是獨立的 and "formula2 的或然率" 等於 number1 and formula1 的機率是 formula2 在 formula2 為真的情況下 , then number2 等於 number1.

(=>
      (and
            (independentProbability ?FORMULA1 ?FORMULA2)
            (equal
                  (ProbabilityFn ?FORMULA2)
                  ?NUMBER1)
            (conditionalProbability ?FORMULA1 ?FORMULA2 ?NUMBER2))
      (equal ?NUMBER2 ?NUMBER1))

If formula1 是 SUO-KIF表述式的實例 and formula2 是 SUO-KIF表述式的實例, then formula1 (不）增�[s) %2 的可能性 or formula1 (不）降低s) %2 的可能性 or formula1 和 formula2 的或然率是獨立的.

(=>
      (and
            (instance ?FORMULA1 Formula)
            (instance ?FORMULA2 Formula))
      (or
            (increasesLikelihood ?FORMULA1 ?FORMULA2)
            (decreasesLikelihood ?FORMULA1 ?FORMULA2)
            (independentProbability ?FORMULA1 ?FORMULA2)))

If rel 是意圖關係的實例 and rel(agent,) (不) 成立s and obj 是 "()" 的一成員, then agent 在 obj 範圍中.

(=>
      (and
            (instance ?REL IntentionalRelation)
            (holds ?REL ?AGENT @ROW)
            (inList
                  ?OBJ
                  (ListFn @ROW)))
      (inScopeOfInterest ?AGENT ?OBJ))

if agent (不) 偏愛not(s) formula1 在 formula2,
then if formula1 &$是真的, then formula2 &$是假的

(=>
      (prefers ?AGENT ?FORMULA1 ?FORMULA2)
      (=>
            (true ?FORMULA1 True)
            (true ?FORMULA2 False)))

If agent (不) 需要not(s) object, then agent (不) 想要not(s) object.

(=>
      (needs ?AGENT ?OBJECT)
      (wants ?AGENT ?OBJECT))

If agent (不) 想要not(s) obj, then there exists purp so that obj 對agent 有意圖 purp.

(=>
      (wants ?AGENT ?OBJ)
      (exists
            (?PURP)
            (hasPurposeForAgent ?OBJ ?PURP ?AGENT)))

If agent (不) 想要not(s) obj, then agent (不) 冀求not(s) "agent (沒) 擁有not(s) obj".

(=>
      (wants ?AGENT ?OBJ)
      (desires
            ?AGENT
            (possesses ?AGENT ?OBJ)))

If agent (不)相信 formula, then there exists time so that agent (不) 考�{p{s} formula timea(之中) time.

(=>
      (believes ?AGENT ?FORMULA)
      (exists
            (?TIME)
            (holdsDuring
                  ?TIME
                  (considers ?AGENT ?FORMULA))))

If agent (不）知道s) %2, then agent (不)相信 formula.

(=>
      (knows ?AGENT ?FORMULA)
      (believes ?AGENT ?FORMULA))

If agent (不）知道s) %2, then formula &$是真的.

(=>
      (knows ?AGENT ?FORMULA)
      (true ?FORMULA True))

If rel 是三元關係的實例, then there don't exist item1,item2,item3,item4, so that rel(item1,item2,item3,item4,) (不) 成立s.

(=>
      (instance ?REL TernaryRelation)
      (not
            (exists
                  (?ITEM1 ?ITEM2 ?ITEM3 ?ITEM4 @ROW)
                  (holds ?REL ?ITEM1 ?ITEM2 ?ITEM3 ?ITEM4 @ROW))))

If rel 是四元關係的實例, then there don't exist item1,item2,item3,item4,item5, so that rel(item1,item2,item3,item4,item5,) (不) 成立s.

(=>
      (instance ?REL QuaternaryRelation)
      (not
            (exists
                  (?ITEM1 ?ITEM2 ?ITEM3 ?ITEM4 ?ITEM5 @ROW)
                  (holds ?REL ?ITEM1 ?ITEM2 ?ITEM3 ?ITEM4 ?ITEM5 @ROW))))

If rel 是五元關係的實例, then there don't exist item1,item2,item3,item4,item5,item6, so that rel(item1,item2,item3,item4,item5,item6,) (不) 成立s.

(=>
      (instance ?REL QuintaryRelation)
      (not
            (exists
                  (?ITEM1 ?ITEM2 ?ITEM3 ?ITEM4 ?ITEM5 ?ITEM6 @ROW)
                  (holds ?REL ?ITEM1 ?ITEM2 ?ITEM3 ?ITEM4 ?ITEM5 ?ITEM6 @ROW))))

if list 是序列的實例,
then there exists number1 so that there exists item1 so that "list 的第二元素" 等於 item1 and for all number2 holds: if number2 是正整數的實例 and number2 小於 number1, then there exists item2 so that "list 的第二元素" 等於 item2

(=>
      (instance ?LIST List)
      (exists
            (?NUMBER1)
            (exists
                  (?ITEM1)
                  (and
                        (not
                              (equal
                                    (ListOrderFn ?LIST ?NUMBER1)
                                    ?ITEM1))
                        (forall
                              (?NUMBER2)
                              (=>
                                    (and
                                          (instance ?NUMBER2 PositiveInteger)
                                          (lessThan ?NUMBER2 ?NUMBER1))
                                    (exists
                                          (?ITEM2)
                                          (equal
                                                (ListOrderFn ?LIST ?NUMBER2)
                                                ?ITEM2))))))))

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))))

if class 被 �]含,
then for all obj holds: if obj 是 class 的實例, then there exists item so that item 是 "()" 的一成員 and obj 是 item 的實例

(=>
      (exhaustiveDecomposition ?CLASS @ROW)
      (forall
            (?OBJ)
            (=>
                  (instance ?OBJ ?CLASS)
                  (exists
                        (?ITEM)
                        (and
                              (inList
                                    ?ITEM
                                    (ListFn @ROW))
                              (instance ?OBJ ?ITEM))))))

if class 無交集地分解成 ,
then for all item holds: if item 是 "()" 的一成員, then item 是 class 的次種類

(=>
      (disjointDecomposition ?CLASS @ROW)
      (forall
            (?ITEM)
            (=>
                  (inList
                        ?ITEM
                        (ListFn @ROW))
                  (subclass ?ITEM ?CLASS))))

if class 無交集地分解成 ,
then for all item1,item2 holds: if item1 是 "()" 的一成員 and item2 是 "()" 的一成員 and item1 等於 item2, then item1 無交集於 item2

(=>
      (disjointDecomposition ?CLASS @ROW)
      (forall
            (?ITEM1 ?ITEM2)
            (=>
                  (and
                        (inList
                              ?ITEM1
                              (ListFn @ROW))
                        (inList
                              ?ITEM2
                              (ListFn @ROW))
                        (not
                              (equal ?ITEM1 ?ITEM2)))
                  (disjoint ?ITEM1 ?ITEM2))))

If list1 是序列的實例 and list2 是序列的實例 and for all number holds: "list1 的第二元素" 等於 "list2 的第二元素", then list1 等於 list2.

(=>
      (and
            (instance ?LIST1 List)
            (instance ?LIST2 List)
            (forall
                  (?NUMBER)
                  (equal
                        (ListOrderFn ?LIST1 ?NUMBER)
                        (ListOrderFn ?LIST2 ?NUMBER))))
      (equal ?LIST1 ?LIST2))

If rel 的論元 number 是 class 的實例 and rel() (不) 成立s, then ""()" 的第二元素" 是 class 的實例.

(=>
      (and
            (domain ?REL ?NUMBER ?CLASS)
            (holds ?REL @ROW))
      (instance
            (ListOrderFn
                  (ListFn @ROW)
                  ?NUMBER)
            ?CLASS))

If rel 的論元 number 是 class 的次種類 and rel() (不) 成立s, then ""()" 的第二元素" 是 class 的次種類.

(=>
      (and
            (domainSubclass ?REL ?NUMBER ?CLASS)
            (holds ?REL @ROW))
      (subclass
            (ListOrderFn
                  (ListFn @ROW)
                  ?NUMBER)
            ?CLASS))

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))))

if rel %&有論元(s) number,
then for all holds: if rel() (不) 成立s, then ""()" 的長度" 等於 number

(=>
      (valence ?REL ?NUMBER)
      (forall
            (@ROW)
            (=>
                  (holds ?REL @ROW)
                  (equal
                        (ListLengthFn
                              (ListFn @ROW))
                        ?NUMBER))))

If "list1 的長度" 等於 number, then there exists list2 so that list1 (沒）初始化not(s) list2 and "(number+1)" 等於 "list2 的長度" and "list2 的第二元素" 等於 item.

(=>
      (equal
            (ListLengthFn ?LIST1)
            ?NUMBER)
      (exists
            (?LIST2)
            (and
                  (initialList ?LIST1 ?LIST2)
                  (equal
                        (SuccessorFn ?NUMBER)
                        (ListLengthFn ?LIST2))
                  (equal
                        (ListOrderFn
                              ?LIST2
                              (SuccessorFn ?NUMBER))
                        ?ITEM))))

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))))))

if list1 是 list2 的次序列,
then for all item holds: if item 是 list1 的一成員, then item 是 list2 的一成員

(=>
      (subList ?LIST1 ?LIST2)
      (forall
            (?ITEM)
            (=>
                  (inList ?ITEM ?LIST1)
                  (inList ?ITEM ?LIST2))))

if list1 是 list2 的次序列,
then there exists number3 so that for all item holds: if item 是 list1 的一成員, then there exist number1,number2 so that "list1 的第二元素" 等於 item and "list2 的第二元素" 等於 item and number2 等於 "(number1+number3)"

(=>
      (subList ?LIST1 ?LIST2)
      (exists
            (?NUMBER3)
            (forall
                  (?ITEM)
                  (=>
                        (inList ?ITEM ?LIST1)
                        (exists
                              (?NUMBER1 ?NUMBER2)
                              (and
                                    (equal
                                          (ListOrderFn ?LIST1 ?NUMBER1)
                                          ?ITEM)
                                    (equal
                                          (ListOrderFn ?LIST2 ?NUMBER2)
                                          ?ITEM)
                                    (equal
                                          ?NUMBER2
                                          (AdditionFn ?NUMBER1 ?NUMBER3))))))))

if list1 (沒）初始化not(s) list2,
then for all number1,number2 holds: if "list1 的長度" 等於 number1 and number2 小於或等於 number1, then "list1 的第二元素" 等於 "list2 的第二元素"

(=>
      (initialList ?LIST1 ?LIST2)
      (forall
            (?NUMBER1 ?NUMBER2)
            (=>
                  (and
                        (equal
                              (ListLengthFn ?LIST1)
                              ?NUMBER1)
                        (lessThanOrEqualTo ?NUMBER2 ?NUMBER1))
                  (equal
                        (ListOrderFn ?LIST1 ?NUMBER2)
                        (ListOrderFn ?LIST2 ?NUMBER2)))))

If function 是一元函數的實例, then function %&有論元(s) .

(=>
      (instance ?FUNCTION UnaryFunction)
      (valence ?FUNCTION 1))

if fun 是一對一函數的實例,
then for all arg1,arg2 holds: if fun 的論元是 class 的實例 and arg1 是 class 的實例 and arg2 是 class 的實例 and arg1 等於 arg2, then "fun(arg1)" 等於 "fun(arg2)"

(=>
      (instance ?FUN OneToOneFunction)
      (forall
            (?ARG1 ?ARG2)
            (=>
                  (and
                        (domain ?FUN 1 ?CLASS)
                        (instance ?ARG1 ?CLASS)
                        (instance ?ARG2 ?CLASS)
                        (not
                              (equal ?ARG1 ?ARG2)))
                  (not
                        (equal
                              (AssignmentFn ?FUN ?ARG1)
                              (AssignmentFn ?FUN ?ARG2))))))

If seq 是順序函數的實例 and seq 的範圍是 class 的實例, then class 是整數的次種類.

(=>
      (and
            (instance ?SEQ SequenceFunction)
            (range ?SEQ ?CLASS))
      (subclass ?CLASS Integer))

If function 是二元函數的實例, then function %&有論元(s) .

(=>
      (instance ?FUNCTION BinaryFunction)
      (valence ?FUNCTION 2))

if function 是關連函數的實例,
then for all inst1,inst2,inst3 holds: if function 的論元是 class 的實例 and inst1 是 class 的實例 and inst2 是 class 的實例 and inst3 是 class 的實例, then "function(inst1,"function(inst2,inst3)")" 等於 "function("function(inst1,inst2)",inst3)"

(=>
      (instance ?FUNCTION AssociativeFunction)
      (forall
            (?INST1 ?INST2 ?INST3)
            (=>
                  (and
                        (domain ?FUNCTION 1 ?CLASS)
                        (instance ?INST1 ?CLASS)
                        (instance ?INST2 ?CLASS)
                        (instance ?INST3 ?CLASS))
                  (equal
                        (AssignmentFn
                              ?FUNCTION
                              ?INST1
                              (AssignmentFn ?FUNCTION ?INST2 ?INST3))
                        (AssignmentFn
                              ?FUNCTION
                              (AssignmentFn ?FUNCTION ?INST1 ?INST2)
                              ?INST3)))))

if function 是可換函數的實例,
then for all inst1,inst2 holds: if function 的論元是 class 的實例 and inst1 是 class 的實例 and inst2 是 class 的實例, then "function(inst1,inst2)" 等於 "function(inst2,inst1)"

(=>
      (instance ?FUNCTION CommutativeFunction)
      (forall
            (?INST1 ?INST2)
            (=>
                  (and
                        (domain ?FUNCTION 1 ?CLASS)
                        (instance ?INST1 ?CLASS)
                        (instance ?INST2 ?CLASS))
                  (equal
                        (AssignmentFn ?FUNCTION ?INST1 ?INST2)
                        (AssignmentFn ?FUNCTION ?INST2 ?INST1)))))

If function 是三元函數的實例, then function %&有論元(s) .

(=>
      (instance ?FUNCTION TernaryFunction)
      (valence ?FUNCTION 3))

If function 是四元函數的實例, then function %&有論元(s) .

(=>
      (instance ?FUNCTION QuaternaryFunction)
      (valence ?FUNCTION 4))

If rel 是二元述詞的實例, then rel %&有論元(s) .

(=>
      (instance ?REL BinaryPredicate)
      (valence ?REL 2))

If rel 是三元述詞的實例, then rel %&有論元(s) .

(=>
      (instance ?REL TernaryPredicate)
      (valence ?REL 3))

If rel 是四元述詞的實例, then rel %&有論元(s) .

(=>
      (instance ?REL QuaternaryPredicate)
      (valence ?REL 4))

If rel 是五元述詞的實例, then rel %&有論元(s) .

(=>
      (instance ?REL QuintaryPredicate)
      (valence ?REL 5))

If rel 是變異元數關係的實例, then there doesn't exist int so that rel %&有論元(s) int.

(=>
      (instance ?REL VariableArityRelation)
      (not
            (exists
                  (?INT)
                  (valence ?REL ?INT))))

if function 封閉於 class and function 是一元函數的實例,
then for all inst holds: if inst 是 class 的實例, then "function(inst)" 是 class 的實例

(=>
      (and
            (closedOn ?FUNCTION ?CLASS)
            (instance ?FUNCTION UnaryFunction))
      (forall
            (?INST)
            (=>
                  (instance ?INST ?CLASS)
                  (instance
                        (AssignmentFn ?FUNCTION ?INST)
                        ?CLASS))))

if function 封閉於 class and function 是二元函數的實例,
then for all inst1,inst2 holds: if inst1 是 class 的實例 and inst2 是 class 的實例, then "function(inst1,inst2)" 是 class 的實例

(=>
      (and
            (closedOn ?FUNCTION ?CLASS)
            (instance ?FUNCTION BinaryFunction))
      (forall
            (?INST1 ?INST2)
            (=>
                  (and
                        (instance ?INST1 ?CLASS)
                        (instance ?INST2 ?CLASS))
                  (instance
                        (AssignmentFn ?FUNCTION ?INST1 ?INST2)
                        ?CLASS))))

if relation 反應於 class ,
then for all inst holds: if inst 是 class 的實例, then relation(inst,inst) (不) 成立s

(=>
      (reflexiveOn ?RELATION ?CLASS)
      (forall
            (?INST)
            (=>
                  (instance ?INST ?CLASS)
                  (holds ?RELATION ?INST ?INST))))

if relation 非反射於 class ,
then for all inst holds: if inst 是 class 的實例, then relation(inst,inst) not(不) 成立

(=>
      (irreflexiveOn ?RELATION ?CLASS)
      (forall
            (?INST)
            (=>
                  (instance ?INST ?CLASS)
                  (not
                        (holds ?RELATION ?INST ?INST)))))

If relation 偏序於 class, then relation 反應於 class and relation 是可遞關係的實例 and relation 是反對稱關係的實例.

(=>
      (partialOrderingOn ?RELATION ?CLASS)
      (and
            (reflexiveOn ?RELATION ?CLASS)
            (instance ?RELATION TransitiveRelation)
            (instance ?RELATION AntisymmetricRelation)))

if relation 對 class 是三分法,
then for all inst1,inst2 holds: if inst1 是 class 的實例 and inst2 是 class 的實例, then relation(inst1,inst2) (不) 成立s or relation(inst2,inst1) (不) 成立s or inst1 等於 inst2

(=>
      (trichotomizingOn ?RELATION ?CLASS)
      (forall
            (?INST1 ?INST2)
            (=>
                  (and
                        (instance ?INST1 ?CLASS)
                        (instance ?INST2 ?CLASS))
                  (or
                        (holds ?RELATION ?INST1 ?INST2)
                        (holds ?RELATION ?INST2 ?INST1)
                        (equal ?INST1 ?INST2)))))

If relation 等同關係於 class , then relation 是可遞關係的實例 and relation 是對稱關係的實例 and relation 反應於 class .

(=>
      (equivalenceRelationOn ?RELATION ?CLASS)
      (and
            (instance ?RELATION TransitiveRelation)
            (instance ?RELATION SymmetricRelation)
            (reflexiveOn ?RELATION ?CLASS)))

if 分配(function1,function2) holds,
then for all inst1,inst2,inst3 holds: if function1 的論元是 class1 的實例 and inst1 是 class1 的實例 and inst2 是 class1 的實例 and inst3 是 class1 的實例 and function2 的論元是 class2 的實例 and inst1 是 class2 的實例 and inst2 是 class2 的實例 and inst3 是 class2 的實例, then "function1(inst1,"function2(inst2,inst3)")" 等於 "function2("function1(inst1,inst2)","function1(inst1,inst3)")"

(=>
      (distributes ?FUNCTION1 ?FUNCTION2)
      (forall
            (?INST1 ?INST2 ?INST3)
            (=>
                  (and
                        (domain ?FUNCTION1 1 ?CLASS1)
                        (instance ?INST1 ?CLASS1)
                        (instance ?INST2 ?CLASS1)
                        (instance ?INST3 ?CLASS1)
                        (domain ?FUNCTION2 1 ?CLASS2)
                        (instance ?INST1 ?CLASS2)
                        (instance ?INST2 ?CLASS2)
                        (instance ?INST3 ?CLASS2))
                  (equal
                        (AssignmentFn
                              ?FUNCTION1
                              ?INST1
                              (AssignmentFn ?FUNCTION2 ?INST2 ?INST3))
                        (AssignmentFn
                              ?FUNCTION2
                              (AssignmentFn ?FUNCTION1 ?INST1 ?INST2)
                              (AssignmentFn ?FUNCTION1 ?INST1 ?INST3))))))

If proc1 是歷程的實例, then there exists proc2 so that proc2 (不) 造成 proc1.

(=>
      (instance ?PROC1 Process)
      (exists
            (?PROC2)
            (causes ?PROC2 ?PROC1)))

if 次類肇因,
then for all inst2 holds: if inst2 是 proc2 的實例, then there exists proc1 inst1 so that inst1 (不) 造成 inst2

(=>
      (causesSubclass ?PROC1 ?PROC2)
      (forall
            (?INST2)
            (=>
                  (instance ?INST2 ?PROC2)
                  (exists
                        (?INST1)
                        (and
                              (instance ?INST1 ?PROC1)
                              (causes ?INST1 ?INST2))))))

if obj1 是 obj2 的精確複製,
then for all attr holds: if attr 是 obj1 的屬性, then attr 是 obj2 的屬性

(=>
      (copy ?OBJ1 ?OBJ2)
      (forall
            (?ATTR)
            (=>
                  (attribute ?OBJ1 ?ATTR)
                  (attribute ?OBJ2 ?ATTR))))

If situation1 (沒) 為真 timea(之中) time and 推知(situation1,situation2) holds, then situation2 (沒) 為真 timea(之中) time.

(=>
      (and
            (holdsDuring ?TIME ?SITUATION1)
            (entails ?SITUATION1 ?SITUATION2))
      (holdsDuring ?TIME ?SITUATION2))

If situation timea(之中) time, then situation (沒) 為真 timea(之中) time.

(=>
      (holdsDuring
            ?TIME
            (not ?SITUATION))
      (not
            (holdsDuring ?TIME ?SITUATION)))

If role 是格位角色的實例 and role(arg1,arg2) (不) 成立s and arg1 是 proc 的實例, then arg2 可以任角色 role 做 proc.

(=>
      (and
            (instance ?ROLE CaseRole)
            (holds ?ROLE ?ARG1 ?ARG2)
            (instance ?ARG1 ?PROC))
      (capability ?PROC ?ROLE ?ARG2))

If obj (不) 利用not(s) agent, then there exists process so that process 是 agent 的施事者 and obj 對 process 是資源.

(=>
      (exploits ?OBJ ?AGENT)
      (exists
            (?PROCESS)
            (and
                  (agent ?PROCESS ?AGENT)
                  (resource ?PROCESS ?OBJ))))

If thing 有意圖 purpose, then there exists agent so that thing 對agent 有意圖 purpose.

(=>
      (hasPurpose ?THING ?PURPOSE)
      (exists
            (?AGENT)
            (hasPurposeForAgent ?THING ?PURPOSE ?AGENT)))

If 有技巧(proc,agent) holds, then agent 可以任角色施事者做 proc.

(=>
      (hasSkill ?PROC ?AGENT)
      (capability ?PROC agent ?AGENT))

If agent 有權使 process 為真, then agent 可以任角色施事者做 process.

(=>
      (holdsRight ?PROCESS ?AGENT)
      (capability ?PROCESS agent ?AGENT))

If agent1 賦予 agent2 權力執行類型 process 任務, then agent2 有權使 process 為真.

(=>
      (confersRight ?PROCESS ?AGENT1 ?AGENT2)
      (holdsRight ?PROCESS ?AGENT2))

If agent 有義務執行類型 process 任務, then agent 可以任角色施事者做 process.

(=>
      (holdsObligation ?PROCESS ?AGENT)
      (capability ?PROCESS agent ?AGENT))

If agent1 賦予 agent2 義務執行類型 process 任務, then agent2 有義務執行類型 process 任務.

(=>
      (confersObligation ?PROCESS ?AGENT1 ?AGENT2)
      (holdsObligation ?PROCESS ?AGENT2))

if obj 位於 region,
then for all subobj holds: if subobj 是 obj 的部分), then subobj 位於 region

(=>
      (located ?OBJ ?REGION)
      (forall
            (?SUBOBJ)
            (=>
                  (part ?SUBOBJ ?OBJ)
                  (located ?SUBOBJ ?REGION))))

If obj 部分位於 region, then there exists subobj so that subobj 是 obj 的部分) and subobj 精確位於 region.

(=>
      (partlyLocated ?OBJ ?REGION)
      (exists
            (?SUBOBJ)
            (and
                  (part ?SUBOBJ ?OBJ)
                  (exactlyLocated ?SUBOBJ ?REGION))))

If obj 精確位於 region, then there doesn't exist otherobj so that otherobj 精確位於 region and otherobj 等於 obj.

(=>
      (exactlyLocated ?OBJ ?REGION)
      (not
            (exists
                  (?OTHEROBJ)
                  (and
                        (exactlyLocated ?OTHEROBJ ?REGION)
                        (not
                              (equal ?OTHEROBJ ?OBJ))))))

If obj1 橫越 obj2, then obj1 與 obj2 相交 or 穿入(obj1,obj2) holds.

(=>
      (traverses ?OBJ1 ?OBJ2)
      (or
            (crosses ?OBJ1 ?OBJ2)
            (penetrates ?OBJ1 ?OBJ2)))

if person (沒) 擁有not(s) obj,
then there exists type so that type 有權使 person 為真 and for all process holds: if process 是 type 的實例, then obj 是 process 的受事者

(=>
      (possesses ?PERSON ?OBJ)
      (exists
            (?TYPE)
            (and
                  (holdsRight ?PERSON ?TYPE)
                  (forall
                        (?PROCESS)
                        (=>
                              (instance ?PROCESS ?TYPE)
                              (patient ?PROCESS ?OBJ))))))

If time 是時間的實例 and agent1 (沒) 擁有not(s) obj timea(之中) time and agent2 (沒) 擁有not(s) obj timea(之中) time, then agent1 等於 agent2.

(=>
      (and
            (instance ?TIME TimePosition)
            (holdsDuring
                  ?TIME
                  (possesses ?AGENT1 ?OBJ))
            (holdsDuring
                  ?TIME
                  (possesses ?AGENT2 ?OBJ)))
      (equal ?AGENT1 ?AGENT2))

if proc1 是 proc2 的先決條件,
then if there exists inst2 so that inst2 是 proc2 的實例, then there exists inst1 so that inst1 是 proc1 的實例

(=>
      (precondition ?PROC1 ?PROC2)
      (=>
            (exists
                  (?INST2)
                  (instance ?INST2 ?PROC2))
            (exists
                  (?INST1)
                  (instance ?INST1 ?PROC1))))

If 抑制(proc1,proc2) holds, then for all time,place holds: "there exists proc1 inst1 so that inst1 位於 place timea(之中) time" (不）降低s) %2 的可能性.

(=>
      (inhibits ?PROC1 ?PROC2)
      (forall
            (?TIME ?PLACE)
            (decreasesLikelihood
                  (holdsDuring
                        ?TIME
                        (exists
                              (?INST1)
                              (and
                                    (instance ?INST1 ?PROC1)
                                    (located ?INST1 ?PLACE))))
                  (holdsDuring
                        ?TIME
                        (exists
                              (?INST2)
                              (and
                                    (instance ?INST2 ?PROC2)
                                    (located ?INST2 ?PLACE)))))))

if proc1 避免 proc2 的發生,
then for all time,place holds: if there exists proc1 inst1 so that inst1 位於 place timea(之中) time, then there exists proc2 inst2 so that inst2 位於 place timea(之中) time

(=>
      (prevents ?PROC1 ?PROC2)
      (forall
            (?TIME ?PLACE)
            (=>
                  (holdsDuring
                        ?TIME
                        (exists
                              (?INST1)
                              (and
                                    (instance ?INST1 ?PROC1)
                                    (located ?INST1 ?PLACE))))
                  (not
                        (holdsDuring
                              ?TIME
                              (exists
                                    (?INST2)
                                    (and
                                          (instance ?INST2 ?PROC2)
                                          (located ?INST2 ?PLACE))))))))

If agent 使用 rep 表示 entity, then rep 表達 entity.

(=>
      (representsForAgent ?REP ?ENTITY ?AGENT)
      (represents ?REP ?ENTITY))

If rep 以語言 language 呈�{ entity, then there exists agent so that agent 使用 rep 表示 entity.

(=>
      (representsInLanguage ?REP ?ENTITY ?LANGUAGE)
      (exists
            (?AGENT)
            (representsForAgent ?REP ?ENTITY ?AGENT)))

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 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))))

If process 表達 prop 的內容, then there exists 內容載體 obj so that obj (不) �]含s) 訊息 %2.

(=>
      (realization ?PROCESS ?PROP)
      (exists
            (?OBJ)
            (and
                  (instance ?OBJ ContentBearingObject)
                  (containsInformation ?OBJ ?PROP))))

if prop1 是 prop2 的次命題,
then for all obj1,obj2 holds: if obj1 (不) �]含s) 訊息 %2 and obj2 (不) �]含s) 訊息 %2, then obj2 �]容 obj1

(=>
      (subProposition ?PROP1 ?PROP2)
      (forall
            (?OBJ1 ?OBJ2)
            (=>
                  (and
                        (containsInformation ?OBJ1 ?PROP1)
                        (containsInformation ?OBJ2 ?PROP2))
                  (subsumesContentInstance ?OBJ2 ?OBJ1))))

If agent 使用 obj, then there exists proc so that proc 是 agent 的施事者 and obj 對 proc 是工具.

(=>
      (uses ?OBJ ?AGENT)
      (exists
            (?PROC)
            (and
                  (agent ?PROC ?AGENT)
                  (instrument ?PROC ?OBJ))))

If number 是有理數的實例, then there exist 整數 int1,整數 int2 so that number 等於 "int1/int2".

(=>
      (instance ?NUMBER RationalNumber)
      (exists
            (?INT1 ?INT2)
            (and
                  (instance ?INT1 Integer)
                  (instance ?INT2 Integer)
                  (equal
                        ?NUMBER
                        (DivisionFn ?INT1 ?INT2)))))

If "number 的上限" 等於 int, then there doesn't exist 整數 otherint so that otherint 大於或等於 number and otherint 小於 int.

(=>
      (equal
            (CeilingFn ?NUMBER)
            ?INT)
      (not
            (exists
                  (?OTHERINT)
                  (and
                        (instance ?OTHERINT Integer)
                        (greaterThanOrEqualTo ?OTHERINT ?NUMBER)
                        (lessThan ?OTHERINT ?INT)))))

If "最大整數小於或等於 number" 等於 int, then there doesn't exist 整數 otherint so that otherint 小於或等於 number and otherint (不) 大於 int.

(=>
      (equal
            (FloorFn ?NUMBER)
            ?INT)
      (not
            (exists
                  (?OTHERINT)
                  (and
                        (instance ?OTHERINT Integer)
                        (lessThanOrEqualTo ?OTHERINT ?NUMBER)
                        (greaterThan ?OTHERINT ?INT)))))

if " 的最大公約數" 等於 number,
then for all element holds: if element 是 "()" 的一成員, then "element 取餘數 number" 等於

(=>
      (equal
            (GreatestCommonDivisorFn @ROW)
            ?NUMBER)
      (forall
            (?ELEMENT)
            (=>
                  (inList
                        ?ELEMENT
                        (ListFn @ROW))
                  (equal
                        (RemainderFn ?ELEMENT ?NUMBER)
                        0))))

if " 的最大公約數" 等於 number,
then there doesn't exist greater so that greater (不) 大於 number and for all element holds: if element 是 "()" 的一成員, then "element 取餘數 greater" 等於

(=>
      (equal
            (GreatestCommonDivisorFn @ROW)
            ?NUMBER)
      (not
            (exists
                  (?GREATER)
                  (and
                        (greaterThan ?GREATER ?NUMBER)
                        (forall
                              (?ELEMENT)
                              (=>
                                    (inList
                                          ?ELEMENT
                                          (ListFn @ROW))
                                    (equal
                                          (RemainderFn ?ELEMENT ?GREATER)
                                          0)))))))

If number 是複數的實例, then there exist part1,part2 so that part1 等於 "number 的實數" and part2 等於 "number 的虛數".

(=>
      (instance ?NUMBER ComplexNumber)
      (exists
            (?PART1 ?PART2)
            (and
                  (equal
                        ?PART1
                        (RealNumberFn ?NUMBER))
                  (equal
                        ?PART2
                        (ImaginaryPartFn ?NUMBER)))))

if " 的最小公倍數" 等於 number,
then for all element holds: if element 是 "()" 的一成員, then "number 取餘數 element" 等於

(=>
      (equal
            (LeastCommonMultipleFn @ROW)
            ?NUMBER)
      (forall
            (?ELEMENT)
            (=>
                  (inList
                        ?ELEMENT
                        (ListFn @ROW))
                  (equal
                        (RemainderFn ?NUMBER ?ELEMENT)
                        0))))

if " 的最小公倍數" 等於 number,
then there doesn't exist less so that less 小於 number and for all element holds: if element 是 "()" 的一成員, then "less 取餘數 element" 等於

(=>
      (equal
            (LeastCommonMultipleFn @ROW)
            ?NUMBER)
      (not
            (exists
                  (?LESS)
                  (and
                        (lessThan ?LESS ?NUMBER)
                        (forall
                              (?ELEMENT)
                              (=>
                                    (inList
                                          ?ELEMENT
                                          (ListFn @ROW))
                                    (equal
                                          (RemainderFn ?LESS ?ELEMENT)
                                          0)))))))

If "number1 和 number2 的最大值 " 等於 number, then

number 等於 number1 and number1 (不) 大於 number2
number 等於 number2 and number2 (不) 大於 number1
number 等於 number1 and number 等於 number2

(=>
      (equal
            (MaxFn ?NUMBER1 ?NUMBER2)
            ?NUMBER)
      (or
            (and
                  (equal ?NUMBER ?NUMBER1)
                  (greaterThan ?NUMBER1 ?NUMBER2))
            (and
                  (equal ?NUMBER ?NUMBER2)
                  (greaterThan ?NUMBER2 ?NUMBER1))
            (and
                  (equal ?NUMBER ?NUMBER1)
                  (equal ?NUMBER ?NUMBER2))))

If "number1 和 number2 的最小值 " 等於 number, then

number 等於 number1 and number1 小於 number2
number 等於 number2 and number2 小於 number1
number 等於 number1 and number 等於 number2

(=>
      (equal
            (MinFn ?NUMBER1 ?NUMBER2)
            ?NUMBER)
      (or
            (and
                  (equal ?NUMBER ?NUMBER1)
                  (lessThan ?NUMBER1 ?NUMBER2))
            (and
                  (equal ?NUMBER ?NUMBER2)
                  (lessThan ?NUMBER2 ?NUMBER1))
            (and
                  (equal ?NUMBER ?NUMBER1)
                  (equal ?NUMBER ?NUMBER2))))

If number 是數量的實例, then "number 的倒數" 等於 "number 乘以次方".

(=>
      (instance ?NUMBER Quantity)
      (equal
            (ReciprocalFn ?NUMBER)
            (ExponentiationFn ?NUMBER -1)))

If number 是數量的實例, then 等於 "number*"number 的倒數"".

(=>
      (instance ?NUMBER Quantity)
      (equal
            1
            (MultiplicationFn
                  ?NUMBER
                  (ReciprocalFn ?NUMBER))))

If "number1 取餘數 number2" 等於 number, then "number2 的正負號" 等於 "number 的正負號".

(=>
      (equal
            (RemainderFn ?NUMBER1 ?NUMBER2)
            ?NUMBER)
      (equal
            (SignumFn ?NUMBER2)
            (SignumFn ?NUMBER)))

If number 是偶整數的實例, then "number 取餘數 " 等於 .

(=>
      (instance ?NUMBER EvenInteger)
      (equal
            (RemainderFn ?NUMBER 2)
            0))

If number 是奇整數的實例, then "number 取餘數 " 等於 .

(=>
      (instance ?NUMBER OddInteger)
      (equal
            (RemainderFn ?NUMBER 2)
            1))

if prime 是質數的實例,
then for all number holds: if "prime 取餘數 number" 等於 , then number 等於 or number 等於 prime

(=>
      (instance ?PRIME PrimeNumber)
      (forall
            (?NUMBER)
            (=>
                  (equal
                        (RemainderFn ?PRIME ?NUMBER)
                        0)
                  (or
                        (equal ?NUMBER 1)
                        (equal ?NUMBER ?PRIME)))))

if "整數 1" 等於 number2,
then
- if "(number1-"最大整數小於或等於 number1")" 小於 , then number2 等於 "最大整數小於或等於 number1"
- if "(number1-"最大整數小於或等於 number1")" 大於或等於 , then number2 等於 "number1 的上限"

(=>
      (equal
            (RoundFn ?NUMBER1)
            ?NUMBER2)
      (or
            (=>
                  (lessThan
                        (SubtractionFn
                              ?NUMBER1
                              (FloorFn ?NUMBER1))
                        0.5)
                  (equal
                        ?NUMBER2
                        (FloorFn ?NUMBER1)))
            (=>
                  (greaterThanOrEqualTo
                        (SubtractionFn
                              ?NUMBER1
                              (FloorFn ?NUMBER1))
                        0.5)
                  (equal
                        ?NUMBER2
                        (CeilingFn ?NUMBER1)))))

If number 是非負實數的實例, then "number 的正負號" 等於 or "number 的正負號" 等於 .

(=>
      (instance ?NUMBER NonnegativeRealNumber)
      (or
            (equal
                  (SignumFn ?NUMBER)
                  1)
            (equal
                  (SignumFn ?NUMBER)
                  0)))

If number 是正實數的實例, then "number 的正負號" 等於 .

(=>
      (instance ?NUMBER PositiveRealNumber)
      (equal
            (SignumFn ?NUMBER)
            1))

If number 是負實數的實例, then "number 的正負號" 等於 .

(=>
      (instance ?NUMBER NegativeRealNumber)
      (equal
            (SignumFn ?NUMBER)
            -1))

If "number1 的平方根" 等於 number2, then "number2*number2" 等於 number1.

(=>
      (equal
            (SquareRootFn ?NUMBER1)
            ?NUMBER2)
      (equal
            (MultiplicationFn ?NUMBER2 ?NUMBER2)
            ?NUMBER1))

If degree 是平面角單位的實例, then "degree 的正切" 等於 ""degree 的正弦"/"degree 的餘弦"".

(=>
      (instance ?DEGREE PlaneAngleMeasure)
      (equal
            (TangentFn ?DEGREE)
            (DivisionFn
                  (SineFn ?DEGREE)
                  (CosineFn ?DEGREE))))

if id 是 function 的同�@元素,
then for all inst holds: if function 的論元是 class 的實例 and inst 是 class 的實例, then "function(id,inst)" 等於 inst

(=>
      (identityElement ?FUNCTION ?ID)
      (forall
            (?INST)
            (=>
                  (and
                        (domain ?FUNCTION 1 ?CLASS)
                        (instance ?INST ?CLASS))
                  (equal
                        (AssignmentFn ?FUNCTION ?ID ?INST)
                        ?INST))))

If "(int1+1)" 等於 "(int2+1)", then int1 等於 int2.

(=>
      (equal
            (SuccessorFn ?INT1)
            (SuccessorFn ?INT2))
      (equal ?INT1 ?INT2))

If int 是整數的實例, then int 小於 "(int+1)".

(=>
      (instance ?INT Integer)
      (lessThan
            ?INT
            (SuccessorFn ?INT)))

If int1 是整數的實例 and int2 是整數的實例, then int1 小於 int2 or int2 小於 "(int1+1)".

(=>
      (and
            (instance ?INT1 Integer)
            (instance ?INT2 Integer))
      (not
            (and
                  (lessThan ?INT1 ?INT2)
                  (lessThan
                        ?INT2
                        (SuccessorFn ?INT1)))))

If int 是整數的實例, then int 等於 "("(int+2)"+1)".

(=>
      (instance ?INT Integer)
      (equal
            ?INT
            (SuccessorFn
                  (PredecessorFn ?INT))))

If int 是整數的實例, then int 等於 "("(int+1)"+2)".

(=>
      (instance ?INT Integer)
      (equal
            ?INT
            (PredecessorFn
                  (SuccessorFn ?INT))))

If "(int1+2)" 等於 "(int2+2)", then int1 等於 int2.

(=>
      (equal
            (PredecessorFn ?INT1)
            (PredecessorFn ?INT2))
      (equal ?INT1 ?INT2))

If int 是整數的實例, then int (不) 大於 "(int+2)".

(=>
      (instance ?INT Integer)
      (greaterThan
            ?INT
            (PredecessorFn ?INT)))

If int1 是整數的實例 and int2 是整數的實例, then int2 小於 int1 or "(int1+2)" 小於 int2.

(=>
      (and
            (instance ?INT1 Integer)
            (instance ?INT2 Integer))
      (not
            (and
                  (lessThan ?INT2 ?INT1)
                  (lessThan
                        (PredecessorFn ?INT1)
                        ?INT2))))

if subset 是 set 的子集,
then for all element holds: if element 是 subset 的元素, then element 是 set 的元素

(=>
      (subset ?SUBSET ?SET)
      (forall
            (?ELEMENT)
            (=>
                  (element ?ELEMENT ?SUBSET)
                  (element ?ELEMENT ?SET))))

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))

If set 是有限集合的實例, then there exists 非負整數 number so that number 等於 "set 中實例的數目".

(=>
      (instance ?SET FiniteSet)
      (exists
            (?NUMBER)
            (and
                  (instance ?NUMBER NonnegativeInteger)
                  (equal
                        ?NUMBER
                        (CardinalityFn ?SET)))))

if superclass 是成對獨立類的實例,
then for all class1,class2 holds: if class1 是 superclass 的實例 and class2 是 superclass 的實例, then class1 等於 class2 or class1 無交集於 class2

(=>
      (instance ?SUPERCLASS PairwiseDisjointClass)
      (forall
            (?CLASS1 ?CLASS2)
            (=>
                  (and
                        (instance ?CLASS1 ?SUPERCLASS)
                        (instance ?CLASS2 ?SUPERCLASS))
                  (or
                        (equal ?CLASS1 ?CLASS2)
                        (disjoint ?CLASS1 ?CLASS2)))))

if class 是互斥類的實例,
then for all inst1,inst2 holds: if inst1 是 class 的實例 and inst2 是 inst1 的實例, then there exists class inst3 so that inst2 是 inst3 的實例

(=>
      (instance ?CLASS MutuallyDisjointClass)
      (forall
            (?INST1 ?INST2)
            (=>
                  (and
                        (instance ?INST1 ?CLASS)
                        (instance ?INST2 ?INST1))
                  (exists
                        (?INST3)
                        (and
                              (instance ?INST3 ?CLASS)
                              (not
                                    (instance ?INST2 ?INST3)))))))

If graph 是圖的實例 and node1 是圖節點的實例 and node2 是圖節點的實例 and node1 是 graph 的部分 and node2 是 graph 的部分 and node1 等於 node2, then there exist arc,path so that

arc (沒) 連結not(s) node1 和 node2
- path 是 graph 的次圖
- path 是圖路徑的實例
- - "path 的最初�`點" 等於 node1 and "path 的最後�`點" 等於 node2
  - "path 的最初�`點" 等於 node2 and "path 的最後�`點" 等於 node1

(=>
      (and
            (instance ?GRAPH Graph)
            (instance ?NODE1 GraphNode)
            (instance ?NODE2 GraphNode)
            (graphPart ?NODE1 ?GRAPH)
            (graphPart ?NODE2 ?GRAPH)
            (not
                  (equal ?NODE1 ?NODE2)))
      (exists
            (?ARC ?PATH)
            (or
                  (links ?NODE1 ?NODE2 ?ARC)
                  (and
                        (subGraph ?PATH ?GRAPH)
                        (instance ?PATH GraphPath)
                        (or
                              (and
                                    (equal
                                          (BeginNodeFn ?PATH)
                                          ?NODE1)
                                    (equal
                                          (EndNodeFn ?PATH)
                                          ?NODE2))
                              (and
                                    (equal
                                          (BeginNodeFn ?PATH)
                                          ?NODE2)
                                    (equal
                                          (EndNodeFn ?PATH)
                                          ?NODE1)))))))

If graph 是圖的實例, then there exist node1,node2,node3,arc1,arc2 so that node1 是 graph 的部分 and node2 是 graph 的部分 and node3 是 graph 的部分 and arc1 是 graph 的部分 and arc2 是 graph 的部分 and node2 (沒) 連結not(s) arc1 和 node1 and node3 (沒) 連結not(s) arc2 和 node2 and node1 等於 node2 and node2 等於 node3 and node1 等於 node3 and arc1 等於 arc2.

(=>
      (instance ?GRAPH Graph)
      (exists
            (?NODE1 ?NODE2 ?NODE3 ?ARC1 ?ARC2)
            (and
                  (graphPart ?NODE1 ?GRAPH)
                  (graphPart ?NODE2 ?GRAPH)
                  (graphPart ?NODE3 ?GRAPH)
                  (graphPart ?ARC1 ?GRAPH)
                  (graphPart ?ARC2 ?GRAPH)
                  (links ?ARC1 ?NODE1 ?NODE2)
                  (links ?ARC2 ?NODE2 ?NODE3)
                  (not
                        (equal ?NODE1 ?NODE2))
                  (not
                        (equal ?NODE2 ?NODE3))
                  (not
                        (equal ?NODE1 ?NODE3))
                  (not
                        (equal ?ARC1 ?ARC2)))))

If graph 是有向圖的實例 and arc 是圖弧線的實例 and arc 是 graph 的部分, then there exist node1,node2 so that "arc 的 �_始節點" 等於 node1 and "arc 的最終�`點" 等於 node2.

(=>
      (and
            (instance ?GRAPH DirectedGraph)
            (instance ?ARC GraphArc)
            (graphPart ?ARC ?GRAPH))
      (exists
            (?NODE1 ?NODE2)
            (and
                  (equal
                        (InitialNodeFn ?ARC)
                        ?NODE1)
                  (equal
                        (TerminalNodeFn ?ARC)
                        ?NODE2))))

If graph 是樹狀圖的實例, then there doesn't exist 圖迴圈 loop so that loop 是 graph 的部分.

(=>
      (instance ?GRAPH Tree)
      (not
            (exists
                  (?LOOP)
                  (and
                        (instance ?LOOP GraphLoop)
                        (graphPart ?LOOP ?GRAPH)))))

if graph 是圖路徑的實例 and arc 是圖弧線的實例 and arc 是 graph 的部分,
then if "arc 的 �_始節點" 等於 node, then there doesn't exist other so that "other 的 �_始節點" 等於 node and other 等於 arc

(=>
      (and
            (instance ?GRAPH GraphPath)
            (instance ?ARC GraphArc)
            (graphPart ?ARC ?GRAPH))
      (=>
            (equal
                  (InitialNodeFn ?ARC)
                  ?NODE)
            (not
                  (exists
                        (?OTHER)
                        (and
                              (equal
                                    (InitialNodeFn ?OTHER)
                                    ?NODE)
                              (not
                                    (equal ?OTHER ?ARC)))))))

if graph 是圖路徑的實例 and arc 是圖弧線的實例 and arc 是 graph 的部分,
then if "arc 的最終�`點" 等於 node, then there doesn't exist other so that "other 的最終�`點" 等於 node and other 等於 arc

(=>
      (and
            (instance ?GRAPH GraphPath)
            (instance ?ARC GraphArc)
            (graphPart ?ARC ?GRAPH))
      (=>
            (equal
                  (TerminalNodeFn ?ARC)
                  ?NODE)
            (not
                  (exists
                        (?OTHER)
                        (and
                              (equal
                                    (TerminalNodeFn ?OTHER)
                                    ?NODE)
                              (not
                                    (equal ?OTHER ?ARC)))))))

If part 是圖元件的實例, then there exists 圖 graph so that part 是 graph 的部分.

(=>
      (instance ?PART GraphElement)
      (exists
            (?GRAPH)
            (and
                  (instance ?GRAPH Graph)
                  (graphPart ?PART ?GRAPH))))

If node 是圖節點的實例, then there exist other,arc so that arc (沒) 連結not(s) node 和 other.

(=>
      (instance ?NODE GraphNode)
      (exists
            (?OTHER ?ARC)
            (links ?NODE ?OTHER ?ARC)))

If arc 是圖弧線的實例, then there exist node1,node2 so that arc (沒) 連結not(s) node1 和 node2.

(=>
      (instance ?ARC GraphArc)
      (exists
            (?NODE1 ?NODE2)
            (links ?NODE1 ?NODE2 ?ARC)))

If "arc 的 �_始節點" 等於 node and "arc 的最終�`點" 等於 node, then arc 是圖迴圈的實例.

(=>
      (and
            (equal
                  (InitialNodeFn ?ARC)
                  ?NODE)
            (equal
                  (TerminalNodeFn ?ARC)
                  ?NODE))
      (instance ?ARC GraphLoop))

If arc (沒) 連結not(s) node1 和 node2, then arc (沒) 連結not(s) node2 和 node1.

(=>
      (links ?NODE1 ?NODE2 ?ARC)
      (links ?NODE2 ?NODE1 ?ARC))

If graph1 是 graph2 的次圖 and element 是 graph1 的部分, then element 是 graph2 的部分.

(=>
      (and
            (subGraph ?GRAPH1 ?GRAPH2)
            (graphPart ?ELEMENT ?GRAPH1))
      (graphPart ?ELEMENT ?GRAPH2))

if
- "path 的路�|長量值" 等於 sum
- subpath 是 path 的次圖
- arc1 是 path 的部分
- arc1 的弧線量是 number1
- for all arc2 holds: if arc2 是 path 的部分, then arc2 是 subpath 的部分 or arc2 等於 arc1
,
then sum 等於 "("subpath 的路�|長量值"+number1)"

(=>
      (and
            (equal
                  (PathWeightFn ?PATH)
                  ?SUM)
            (subGraph ?SUBPATH ?PATH)
            (graphPart ?ARC1 ?PATH)
            (arcWeight ?ARC1 ?NUMBER1)
            (forall
                  (?ARC2)
                  (=>
                        (graphPart ?ARC2 ?PATH)
                        (or
                              (graphPart ?ARC2 ?SUBPATH)
                              (equal ?ARC2 ?ARC1)))))
      (equal
            ?SUM
            (AdditionFn
                  (PathWeightFn ?SUBPATH)
                  ?NUMBER1)))

if
- "path 的路�|長量值" 等於 sum
- arc1 是 path 的部分
- arc2 是 path 的部分
- arc1 的弧線量是 number1
- arc2 的弧線量是 number2
- for all arc3 holds: if arc3 是 path 的部分, then arc3 等於 arc1 or arc3 等於 arc2
,
then "path 的路�|長量值" 等於 "(number1+number2)"

(=>
      (and
            (equal
                  (PathWeightFn ?PATH)
                  ?SUM)
            (graphPart ?ARC1 ?PATH)
            (graphPart ?ARC2 ?PATH)
            (arcWeight ?ARC1 ?NUMBER1)
            (arcWeight ?ARC2 ?NUMBER2)
            (forall
                  (?ARC3)
                  (=>
                        (graphPart ?ARC3 ?PATH)
                        (or
                              (equal ?ARC3 ?ARC1)
                              (equal ?ARC3 ?ARC2)))))
      (equal
            (PathWeightFn ?PATH)
            (AdditionFn ?NUMBER1 ?NUMBER2)))

If "最小量路徑函數(node1,node2)" 等於 path, then path 是 "node1 和 node2 間集合路�|" 的實例.

(=>
      (equal
            (MinimalWeightedPathFn ?NODE1 ?NODE2)
            ?PATH)
      (instance
            ?PATH
            (GraphPathFn ?NODE1 ?NODE2)))

if "最小量路徑函數(node1,node2)" 等於 path and "path 的路�|長量值" 等於 number,
then for all path2 holds: if path2 是 "node1 和 node2 間集合路�|" 的實例 and "path2 的路�|長量值" 等於 number2, then number2 大於或等於 number1

(=>
      (and
            (equal
                  (MinimalWeightedPathFn ?NODE1 ?NODE2)
                  ?PATH)
            (equal
                  (PathWeightFn ?PATH)
                  ?NUMBER))
      (forall
            (?PATH2)
            (=>
                  (and
                        (instance
                              ?PATH2
                              (GraphPathFn ?NODE1 ?NODE2))
                        (equal
                              (PathWeightFn ?PATH2)
                              ?NUMBER2))
                  (greaterThanOrEqualTo ?NUMBER2 ?NUMBER1))))

If "node1 和 node2 間最大路�|" 等於 path, then path 是 "node1 和 node2 間集合路�|" 的實例.

(=>
      (equal
            (MaximalWeightedPathFn ?NODE1 ?NODE2)
            ?PATH)
      (instance
            ?PATH
            (GraphPathFn ?NODE1 ?NODE2)))

if "node1 和 node2 間最大路�|" 等於 path and "path 的路�|長量值" 等於 number,
then for all path2 holds: if path2 是 "node1 和 node2 間集合路�|" 的實例 and "path2 的路�|長量值" 等於 number2, then number2 小於或等於 number1

(=>
      (and
            (equal
                  (MaximalWeightedPathFn ?NODE1 ?NODE2)
                  ?PATH)
            (equal
                  (PathWeightFn ?PATH)
                  ?NUMBER))
      (forall
            (?PATH2)
            (=>
                  (and
                        (instance
                              ?PATH2
                              (GraphPathFn ?NODE1 ?NODE2))
                        (equal
                              (PathWeightFn ?PATH2)
                              ?NUMBER2))
                  (lessThanOrEqualTo ?NUMBER2 ?NUMBER1))))

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)))

If graph 是圖的實例, then "劃分 graph 為兩獨立圖表的最小相交路�|" 是 "劃分 graph 為兩獨立圖表的相交路�|" 的次種類.

(=>
      (instance ?GRAPH Graph)
      (subclass
            (MinimalCutSetFn ?GRAPH)
            (CutSetFn ?GRAPH)))

if "劃分 graph 為兩獨立圖表的最小相交路�|" 等於 pathclass,
then there exists number so that for all path holds: if path 是 pathclass 的實例, then path 的路�|長是 number

(=>
      (equal
            (MinimalCutSetFn ?GRAPH)
            ?PATHCLASS)
      (exists
            (?NUMBER)
            (forall
                  (?PATH)
                  (=>
                        (instance ?PATH ?PATHCLASS)
                        (pathLength ?PATH ?NUMBER)))))

If "number unit(s)" 等於 quant and unit 是 quanttype 的次種類, then quant 是 quanttype 的實例.

(=>
      (and
            (equal
                  (MeasureFn ?NUMBER ?UNIT)
                  ?QUANT)
            (subclass ?UNIT ?QUANTTYPE))
      (instance ?QUANT ?QUANTTYPE))

if rel 是與量關係的實例 and rel 是三元關係的實例 and number1 是實數的實例 and number2 是實數的實例 and rel(number1,number2,value) (不) 成立s,
then for all unit holds: if unit 是量度單位的實例, then rel("number1 unit(s)","number2 unit(s)","value unit(s)") (不) 成立s

(=>
      (and
            (instance ?REL RelationExtendedToQuantities)
            (instance ?REL TernaryRelation)
            (instance ?NUMBER1 RealNumber)
            (instance ?NUMBER2 RealNumber)
            (holds ?REL ?NUMBER1 ?NUMBER2 ?VALUE))
      (forall
            (?UNIT)
            (=>
                  (instance ?UNIT UnitOfMeasure)
                  (holds
                        ?REL
                        (MeasureFn ?NUMBER1 ?UNIT)
                        (MeasureFn ?NUMBER2 ?UNIT)
                        (MeasureFn ?VALUE ?UNIT)))))

if rel 是與量關係的實例 and rel 是二元關係的實例 and number1 是實數的實例 and number2 是實數的實例 and rel(number1,number2) (不) 成立s,
then for all unit holds: if unit 是量度單位的實例, then rel("number1 unit(s)","number2 unit(s)") (不) 成立s

(=>
      (and
            (instance ?REL RelationExtendedToQuantities)
            (instance ?REL BinaryRelation)
            (instance ?NUMBER1 RealNumber)
            (instance ?NUMBER2 RealNumber)
            (holds ?REL ?NUMBER1 ?NUMBER2))
      (forall
            (?UNIT)
            (=>
                  (instance ?UNIT UnitOfMeasure)
                  (holds
                        ?REL
                        (MeasureFn ?NUMBER1 ?UNIT)
                        (MeasureFn ?NUMBER2 ?UNIT)))))

If unit 是量度單位的實例, then "1 千 units" 等於 " unit(s)".

(=>
      (instance ?UNIT UnitOfMeasure)
      (equal
            (KiloFn ?UNIT)
            (MeasureFn 1000 ?UNIT)))

If unit 是量度單位的實例, then "1 百萬 units" 等於 " unit(s)".

(=>
      (instance ?UNIT UnitOfMeasure)
      (equal
            (MegaFn ?UNIT)
            (MeasureFn 1000000 ?UNIT)))

If unit 是量度單位的實例, then "1 十億 units" 等於 " unit(s)".

(=>
      (instance ?UNIT UnitOfMeasure)
      (equal
            (GigaFn ?UNIT)
            (MeasureFn 1000000000 ?UNIT)))

If unit 是量度單位的實例, then "1 兆 units" 等於 " unit(s)".

(=>
      (instance ?UNIT UnitOfMeasure)
      (equal
            (TeraFn ?UNIT)
            (MeasureFn 1000000000000 ?UNIT)))

If unit 是量度單位的實例, then "unit 的千分之�@" 等於 " unit(s)".

(=>
      (instance ?UNIT UnitOfMeasure)
      (equal
            (MilliFn ?UNIT)
            (MeasureFn 0.001 ?UNIT)))

If unit 是量度單位的實例, then "unit 的百萬分之�@" 等於 " unit(s)".

(=>
      (instance ?UNIT UnitOfMeasure)
      (equal
            (MicroFn ?UNIT)
            (MeasureFn 0.000001 ?UNIT)))

If unit 是量度單位的實例, then "unit 的十億分之�@" 等於 " unit(s)".

(=>
      (instance ?UNIT UnitOfMeasure)
      (equal
            (NanoFn ?UNIT)
            (MeasureFn 0.000000001 ?UNIT)))

If unit 是量度單位的實例, then "1 的兆分之�@ " 等於 " unit(s)".

(=>
      (instance ?UNIT UnitOfMeasure)
      (equal
            (PicoFn ?UNIT)
            (MeasureFn 0.000000000001 ?UNIT)))

If number 是實數的實例 and unit 是量度單位的實例, then "1 的級數" 等於 number.

(=>
      (and
            (instance ?NUMBER RealNumber)
            (instance ?UNIT UnitOfMeasure))
      (equal
            (MagnitudeFn
                  (MeasureFn ?NUMBER ?UNIT))
            ?NUMBER))

If object 的測量是 "在方向 direction 中的 ref 每 time 有 distance", then object 的測量是 "每 time 有 distance".

(=>
      (measure
            ?OBJECT
            (VelocityFn ?DISTANCE ?TIME ?REF ?DIRECTION))
      (measure
            ?OBJECT
            (SpeedFn ?DISTANCE ?TIME)))

If number 是實數的實例, then "number 公分(s)" 等於 ""number*" 公尺(s)".

(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER Centimeter)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 0.01)
                  Meter)))

If number 是實數的實例, then "number 攝氏(s)" 等於 ""(number-)" 絕對溫標(s)".

(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER CelsiusDegree)
            (MeasureFn
                  (SubtractionFn ?NUMBER 273.15)
                  KelvinDegree)))

If number 是實數的實例, then "number 攝氏(s)" 等於 """(number-)"/" 華氏-度(s)".

(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER CelsiusDegree)
            (MeasureFn
                  (DivisionFn
                        (SubtractionFn ?NUMBER 32)
                        1.8)
                  FahrenheitDegree)))

If number 是實數的實例, then "number 日計(s)" 等於 ""number*" 時計(s)".

(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER DayDuration)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 24)
                  HourDuration)))

If number 是實數的實例, then "number 時計(s)" 等於 ""number*" 分計(s)".

(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER HourDuration)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 60)
                  MinuteDuration)))

If number 是實數的實例, then "number 分計(s)" 等於 ""number*" 秒計(s)".

(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER MinuteDuration)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 60)
                  SecondDuration)))

If number 是實數的實例, then "number 周計(s)" 等於 ""number*" 日計(s)".

(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER WeekDuration)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 7)
                  DayDuration)))

If number 是實數的實例, then "number 年計(s)" 等於 ""number*" 日計(s)".

(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER YearDuration)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 365)
                  DayDuration)))

If number 是實數的實例, then "number 原子質量單位(s)" 等於 ""number**" 克(s)".

(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER Amu)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 1.6605402 E-24)
                  Gram)))

If number 是實數的實例, then "number 電壓單位-電伏特(s)" 等於 ""number**" 功或能的單位-焦爾(s)".

(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER ElectronVolt)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 1.60217733 E-19)
                  Joule)))

If number 是實數的實例, then "number 光譜線波長單位(s)" 等於 ""number**" 公尺(s)".

(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER Angstrom)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 1.0 E-10)
                  Meter)))

If number 是實數的實例, then "number 英尺(s)" 等於 ""number*" 公尺(s)".

(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER Foot)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 0.3048)
                  Meter)))

If number 是實數的實例, then "number 英吋(s)" 等於 ""number*" 公尺(s)".

(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER Inch)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 0.0254)
                  Meter)))

If number 是實數的實例, then "number 英里(s)" 等於 ""number*" 公尺(s)".

(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER Mile)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 1609.344)
                  Meter)))

If number 是實數的實例, then "number 美制液量單位-加侖(s)" 等於 ""number*" 公升(s)".

(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER UnitedStatesGallon)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 3.785411784)
                  Liter)))

If number 是實數的實例, then "number 容量或液量單位(s)" 等於 ""number/" 美制液量單位-加侖(s)".

(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER Quart)
            (MeasureFn
                  (DivisionFn ?NUMBER 4)
                  UnitedStatesGallon)))

If number 是實數的實例, then "number 品脫(s)" 等於 ""number/" 容量或液量單位(s)".

(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER Pint)
            (MeasureFn
                  (DivisionFn ?NUMBER 2)
                  Quart)))

If number 是實數的實例, then "number 半品脫之量(s)" 等於 ""number/" 品脫(s)".

(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER Cup)
            (MeasureFn
                  (DivisionFn ?NUMBER 2)
                  Pint)))

If number 是實數的實例, then "number 盎司(s)" 等於 ""number/" 半品脫之量(s)".

(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER Ounce)
            (MeasureFn
                  (DivisionFn ?NUMBER 8)
                  Cup)))

If number 是實數的實例, then "number 英制液量單位-加侖(s)" 等於 ""number*" 公升(s)".

(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER UnitedKingdomGallon)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 4.54609)
                  Liter)))

If number 是實數的實例, then "number 磅(s)" 等於 ""number*" 克(s)".

(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER PoundMass)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 453.59237)
                  Gram)))

If number 是實數的實例, then "number 質量單位(s)" 等於 ""number*" 克(s)".

(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER Slug)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 14593.90)
                  Gram)))

If number 是實數的實例, then "number 摩擦角度(s)" 等於 ""number*" 絕對溫標(s)".

(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER RankineDegree)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 1.8)
                  KelvinDegree)))

If number 是實數的實例, then "number 力量單位(s)" 等於 ""number*" 力的單位-牛頓(s)".

(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER PoundForce)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 4.448222)
                  Newton)))

If number 是實數的實例, then "number 熱量的單位-卡路里(s)" 等於 ""number*" 功或能的單位-焦爾(s)".

(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER Calorie)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 4.1868)
                  Joule)))

If number 是實數的實例, then "number 英國熱量單位-BTU(s)" 等於 ""number*" 功或能的單位-焦爾(s)".

(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER BritishThermalUnit)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 1055.05585262)
                  Joule)))

If number 是實數的實例, then "number 角度(s)" 等於 ""number*"圓周率/"" 弧度(s)".

(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER AngularDegree)
            (MeasureFn
                  (MultiplicationFn
                        ?NUMBER
                        (DivisionFn Pi 180))
                  Radian)))

If number 是實數的實例, then "number 美元一分(s)" 等於 ""number*" 美元一元(s)".

(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER UnitedStatesCent)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 0.01)
                  UnitedStatesDollar)))

If number 是實數的實例, then "number 歐元一分(s)" 等於 ""number*" 歐元一元(s)".

(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER EuroCent)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 0.01)
                  EuroDollar)))

If number 是實數的實例, then "number 位元組(s)" 等於 ""number*" 位元(s)".

(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER Byte)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 8)
                  Bit)))

If number 是實數的實例, then "number 千位元組(s)" 等於 ""number*" 位元組(s)".

(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER KiloByte)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 1024)
                  Byte)))

If number 是實數的實例, then "number 百萬位元組(s)" 等於 ""number*" 千位元組(s)".

(=>
      (instance ?NUMBER RealNumber)
      (equal
            (MeasureFn ?NUMBER MegaByte)
            (MeasureFn
                  (MultiplicationFn ?NUMBER 1024)
                  KiloByte)))

If obj1 和 obj2 之間距離是 quant, then obj2 和 obj1 之間距離是 quant.

(=>
      (distance ?OBJ1 ?OBJ2 ?QUANT)
      (distance ?OBJ2 ?OBJ1 ?QUANT))

If 標高(obj1,obj2,height) holds, then obj1 對 obj2 是在...之上.

(=>
      (altitude ?OBJ1 ?OBJ2 ?HEIGHT)
      (orientation ?OBJ1 ?OBJ2 Above))

If 標高(obj1,obj2,height) holds, then there exists top so that obj1 的頂端是 top and top 和 obj2 之間距離是 height.

(=>
      (altitude ?OBJ1 ?OBJ2 ?HEIGHT)
      (exists
            (?TOP)
            (and
                  (top ?TOP ?OBJ1)
                  (distance ?TOP ?OBJ2 ?HEIGHT))))

If 深度, then obj1 對 obj2 是在...之下.

(=>
      (depth ?OBJ1 ?OBJ2 ?DEPTH)
      (orientation ?OBJ1 ?OBJ2 Below))

If 深度, then there exists bottom so that obj1 的底部是 bottom and bottom 和 obj2 之間距離是 depth.

(=>
      (depth ?OBJ1 ?OBJ2 ?DEPTH)
      (exists
            (?BOTTOM)
            (and
                  (bottom ?BOTTOM ?OBJ1)
                  (distance ?BOTTOM ?OBJ2 ?DEPTH))))

if obj1 大於 obj2,
then for all quant1,quant2 holds: if obj1 的測量是 "quant1 長度單位(s)" and obj2 的測量是 "quant2 長度單位(s)", then quant1 (不) 大於 quant2

(=>
      (larger ?OBJ1 ?OBJ2)
      (forall
            (?QUANT1 ?QUANT2)
            (=>
                  (and
                        (measure
                              ?OBJ1
                              (MeasureFn ?QUANT1 LengthMeasure))
                        (measure
                              ?OBJ2
                              (MeasureFn ?QUANT2 LengthMeasure)))
                  (greaterThan ?QUANT1 ?QUANT2))))

If point 是時點的實例 and point 等於時間終點/永遠, then point (沒) 發生?{s} 在時間終點/永遠之前.

(=>
      (and
            (instance ?POINT TimePoint)
            (not
                  (equal ?POINT PositiveInfinity)))
      (before ?POINT PositiveInfinity))

If point 是時點的實例 and point 等於時間終點/永遠, then there exists otherpoint so that otherpoint 在 point 和時間終點/永遠之間 .

(=>
      (and
            (instance ?POINT TimePoint)
            (not
                  (equal ?POINT PositiveInfinity)))
      (exists
            (?OTHERPOINT)
            (temporallyBetween ?POINT ?OTHERPOINT PositiveInfinity)))

If point 是時點的實例 and point 等於時間起點/亙古, then 時間起點/亙古 (沒) 發生?{s} 在 point 之前.

(=>
      (and
            (instance ?POINT TimePoint)
            (not
                  (equal ?POINT NegativeInfinity)))
      (before NegativeInfinity ?POINT))

If point 是時點的實例 and point 等於時間起點/亙古, then there exists otherpoint so that otherpoint 在時間起點/亙古和 point 之間 .

(=>
      (and
            (instance ?POINT TimePoint)
            (not
                  (equal ?POINT NegativeInfinity)))
      (exists
            (?OTHERPOINT)
            (temporallyBetween NegativeInfinity ?OTHERPOINT ?POINT)))

if 每 time1 發生 proc,
then for all time2 holds: if time2 的持續是 time1, then there exists position so that position 是 time2 的部分 and there exists inst so that inst 是 proc 的實例 positiona(之中) position

(=>
      (frequency ?PROC ?TIME1)
      (forall
            (?TIME2)
            (=>
                  (duration ?TIME2 ?TIME1)
                  (exists
                        (?POSITION)
                        (and
                              (temporalPart ?POSITION ?TIME2)
                              (holdsDuring
                                    ?POSITION
                                    (exists
                                          (?INST)
                                          (instance ?INST ?PROC))))))))

If point 是時點的實例, then there exists 時段 interval so that point 是 interval 的部分.

(=>
      (instance ?POINT TimePoint)
      (exists
            (?INTERVAL)
            (and
                  (instance ?INTERVAL TimeInterval)
                  (temporalPart ?POINT ?INTERVAL))))

If interval 是時段的實例, then there exists 時點 point so that point 是 interval 的部分.

(=>
      (instance ?INTERVAL TimeInterval)
      (exists
            (?POINT)
            (and
                  (instance ?POINT TimePoint)
                  (temporalPart ?POINT ?INTERVAL))))

If situation (沒) 為真 time1a(之中) time1 and time2 是 time1 的部分, then situation (沒) 為真 time2a(之中) time2.

(=>
      (and
            (holdsDuring ?TIME1 ?SITUATION)
            (temporalPart ?TIME2 ?TIME1))
      (holdsDuring ?TIME2 ?SITUATION))

If rel(inst1,inst2) (不) 成立s intervala(之中) interval and inst1 是物質的的實例 and inst2 是物質的的實例, then inst1 (不) 存在s interval 期間 and inst2 (不) 存在s interval 期間.

(=>
      (and
            (holdsDuring
                  ?INTERVAL
                  (holds ?REL ?INST1 ?INST2))
            (instance ?INST1 Physical)
            (instance ?INST2 Physical))
      (and
            (time ?INST1 ?INTERVAL)
            (time ?INST2 ?INTERVAL)))

if "interval 的 �}始" 等於 point,
then for all otherpoint holds: if otherpoint 是 interval 的部分 and otherpoint 等於 point, then point (沒) 發生?{s} 在 otherpoint 之前

(=>
      (equal
            (BeginFn ?INTERVAL)
            ?POINT)
      (forall
            (?OTHERPOINT)
            (=>
                  (and
                        (temporalPart ?OTHERPOINT ?INTERVAL)
                        (not
                              (equal ?OTHERPOINT ?POINT)))
                  (before ?POINT ?OTHERPOINT))))

If process (不) �_源s 於 obj, then "process 在 ""process 存在的時間" 的 �}始" 的 ""process 存在的時間" 的 �}始"位置" 位於 "obj 在 ""obj 存在的時間" 的 �}始" 的 ""obj 存在的時間" 的 �}始"位置".

(=>
      (origin ?PROCESS ?OBJ)
      (located
            (WhereFn
                  ?PROCESS
                  (BeginFn
                        (WhenFn ?PROCESS)))
            (WhereFn
                  ?OBJ
                  (BeginFn
                        (WhenFn ?OBJ)))))

if "interval 的結束" 等於 point,
then for all otherpoint holds: if otherpoint 是 interval 的部分 and otherpoint 等於 point, then otherpoint (沒) 發生?{s} 在 point 之前

(=>
      (equal
            (EndFn ?INTERVAL)
            ?POINT)
      (forall
            (?OTHERPOINT)
            (=>
                  (and
                        (temporalPart ?OTHERPOINT ?INTERVAL)
                        (not
                              (equal ?OTHERPOINT ?POINT)))
                  (before ?OTHERPOINT ?POINT))))

if obj 是物體的實例,
then there exist 時點 time1,時點 time2 so that time1 (沒) 發生?{s} 在 time2 之前 and for all time holds: if time1 (沒) 發生?{s} 在 time 或之前 and time (沒) 發生?{s} 在 time2 或之前, then obj (不) 存在s time 期間

(=>
      (instance ?OBJ Object)
      (exists
            (?TIME1 ?TIME2)
            (and
                  (instance ?TIME1 TimePoint)
                  (instance ?TIME2 TimePoint)
                  (before ?TIME1 ?TIME2)
                  (forall
                        (?TIME)
                        (=>
                              (and
                                    (beforeOrEqual ?TIME1 ?TIME)
                                    (beforeOrEqual ?TIME ?TIME2))
                              (time ?OBJ ?TIME))))))

if obj 是 proc 的結果,
then for all time holds: if time (沒) 發生?{s} 在 ""proc 存在的時間" 的 �}始" 之前, then obj not(不) 存在 time 期間

(=>
      (result ?PROC ?OBJ)
      (forall
            (?TIME)
            (=>
                  (before
                        ?TIME
                        (BeginFn
                              (WhenFn ?PROC)))
                  (not
                        (time ?OBJ ?TIME)))))

If point1 (沒) 發生?{s} 在 point2 或之前, then point1 (沒) 發生?{s} 在 point2 之前 or point1 等於 point2.

(=>
      (beforeOrEqual ?POINT1 ?POINT2)
      (or
            (before ?POINT1 ?POINT2)
            (equal ?POINT1 ?POINT2)))

If rel 是空間關係的實例 and rel(obj1,obj2) (不) 成立s, then "obj2 存在的時間" (沒) 與 1 ?重疊s.

(=>
      (and
            (instance ?REL SpatialRelation)
            (holds ?REL ?OBJ1 ?OBJ2))
      (overlapsTemporally
            (WhenFn ?OBJ1)
            (WhenFn ?OBJ2)))

If interval1 (沒) 發生not(s) 在 interval2 期間, then "interval1 的結束" (沒) 發生?{s} 在 "interval2 的結束" 之前 and "interval2 的 �}始" (沒) 發生?{s} 在 "interval1 的 �}始" 之前.

(=>
      (during ?INTERVAL1 ?INTERVAL2)
      (and
            (before
                  (EndFn ?INTERVAL1)
                  (EndFn ?INTERVAL2))
            (before
                  (BeginFn ?INTERVAL2)
                  (BeginFn ?INTERVAL1))))

If "interval1 的 �}始" 等於 "interval2 的 �}始" and "interval1 的結束" 等於 "interval2 的結束", then interval1 等於 interval2.

(=>
      (and
            (equal
                  (BeginFn ?INTERVAL1)
                  (BeginFn ?INTERVAL2))
            (equal
                  (EndFn ?INTERVAL1)
                  (EndFn ?INTERVAL2)))
      (equal ?INTERVAL1 ?INTERVAL2))

If "point1 和 point2 的間距" 等於 interval, then "interval 的 �}始" 等於 point1 and "interval 的結束" 等於 point2.

(=>
      (equal
            (TimeIntervalFn ?POINT1 ?POINT2)
            ?INTERVAL)
      (and
            (equal
                  (BeginFn ?INTERVAL)
                  ?POINT1)
            (equal
                  (EndFn ?INTERVAL)
                  ?POINT2)))

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))))

If interval 是 "從 timeclass1 到 timeclass2 的 �^歸間隔" 的實例, then there exist timeclass1 time1,timeclass2 time2 so that time1 (沒) �}始s interval and time2 (沒) 完成s interval.

(=>
      (instance
            ?INTERVAL
            (RecurrentTimeIntervalFn ?TIMECLASS1 ?TIMECLASS2))
      (exists
            (?TIME1 ?TIME2)
            (and
                  (instance ?TIME1 ?TIMECLASS1)
                  (instance ?TIME2 ?TIMECLASS2)
                  (starts ?TIME1 ?INTERVAL)
                  (finishes ?TIME2 ?INTERVAL))))

If thing 是物質的的實例, then ""thing 存在的時間" 的 �}始" (沒) 發生?{s} 在 ""thing 存在的時間" 的結束" 之前.

(=>
      (instance ?THING Physical)
      (before
            (BeginFn
                  (WhenFn ?THING))
            (EndFn
                  (WhenFn ?THING))))

If thing 是物質的的實例, then ""thing 存在的時間" 之前" (沒) 相接s "thing 存在的時間".

(=>
      (instance ?THING Physical)
      (meetsTemporally
            (PastFn
                  (WhenFn ?THING))
            (WhenFn ?THING)))

If process 是物質的的實例, then ""process 存在的時間" 之前" 等於 "時間起點/亙古和 ""process 存在的時間" 的 �}始" 的間距".

(=>
      (instance ?PROCESS Physical)
      (equal
            (PastFn
                  (WhenFn ?PROCESS))
            (TimeIntervalFn
                  NegativeInfinity
                  (BeginFn
                        (WhenFn ?PROCESS)))))

If thing 是物質的的實例, then ""thing 存在的時間" 不久之前" (沒) 完成s ""thing 存在的時間" 之前".

(=>
      (instance ?THING Physical)
      (finishes
            (ImmediatePastFn
                  (WhenFn ?THING))
            (PastFn
                  (WhenFn ?THING))))

If obj 對 proc 是資源 and obj 的測量是 quant1 ""proc 存在的時間" 不久之前"a(之中) "proc 存在的時間" 不久之前 and obj 的測量是 quant2 ""proc 存在的時間" 不久之後"a(之中) "proc 存在的時間" 不久之後, then quant1 (不) 大於 quant2.

(=>
      (and
            (resource ?PROC ?OBJ)
            (holdsDuring
                  (ImmediatePastFn
                        (WhenFn ?PROC))
                  (measure ?OBJ ?QUANT1))
            (holdsDuring
                  (ImmediateFutureFn
                        (WhenFn ?PROC))
                  (measure ?OBJ ?QUANT2)))
      (greaterThan ?QUANT1 ?QUANT2))

If thing 是物質的的實例, then "thing 存在的時間" (沒) 相接s ""thing 存在的時間" 之後".

(=>
      (instance ?THING Physical)
      (meetsTemporally
            (WhenFn ?THING)
            (FutureFn
                  (WhenFn ?THING))))

If process 是物質的的實例, then ""process 存在的時間" 之後" 等於 """process 存在的時間" 的結束" 和時間終點/永遠的間距".

(=>
      (instance ?PROCESS Physical)
      (equal
            (FutureFn
                  (WhenFn ?PROCESS))
            (TimeIntervalFn
                  (EndFn
                        (WhenFn ?PROCESS))
                  PositiveInfinity)))

If thing 是物質的的實例, then ""thing 存在的時間" 不久之後" (沒) �}始s ""thing 存在的時間" 之後".

(=>
      (instance ?THING Physical)
      (starts
            (ImmediateFutureFn
                  (WhenFn ?THING))
            (FutureFn
                  (WhenFn ?THING))))

If day 是 "日 number" 的實例, then number 小於或等於 .

(=>
      (instance
            ?DAY
            (DayFn ?NUMBER ?MONTH))
      (lessThanOrEqualTo ?NUMBER 31))

If day1 是 "日 number1" 的實例 and day2 是 "日 number2" 的實例 and "(number2-number1)" 等於 , then day1 (沒) 相接s day2.

(=>
      (and
            (instance
                  ?DAY1
                  (DayFn ?NUMBER1 ?MONTH))
            (instance
                  ?DAY2
                  (DayFn ?NUMBER2 ?MONTH))
            (equal
                  (SubtractionFn ?NUMBER2 ?NUMBER1)
                  1))
      (meetsTemporally ?DAY1 ?DAY2))

If hour 是 "小時 number" 的實例, then number 小於 .

(=>
      (instance
            ?HOUR
            (HourFn ?NUMBER ?DAY))
      (lessThan ?NUMBER 24))

If hour1 是 "小時 number1" 的實例 and hour2 是 "小時 number2" 的實例 and "(number2-number1)" 等於 , then hour1 (沒) 相接s hour2.

(=>
      (and
            (instance
                  ?HOUR1
                  (HourFn ?NUMBER1 ?DAY))
            (instance
                  ?HOUR2
                  (HourFn ?NUMBER2 ?DAY))
            (equal
                  (SubtractionFn ?NUMBER2 ?NUMBER1)
                  1))
      (meetsTemporally ?HOUR1 ?HOUR2))

If minute 是 "分鐘 number" 的實例, then number 小於 .

(=>
      (instance
            ?MINUTE
            (MinuteFn ?NUMBER ?HOUR))
      (lessThan ?NUMBER 60))

If minute1 是 "分鐘 number1" 的實例 and minute2 是 "分鐘 number2" 的實例 and "(number2-number1)" 等於 , then minute1 (沒) 相接s minute2.

(=>
      (and
            (instance
                  ?MINUTE1
                  (MinuteFn ?NUMBER1 ?HOUR))
            (instance
                  ?MINUTE2
                  (MinuteFn ?NUMBER2 ?HOUR))
            (equal
                  (SubtractionFn ?NUMBER2 ?NUMBER1)
                  1))
      (meetsTemporally ?MINUTE1 ?MINUTE2))

If second 是 "秒鐘函數(number,minute)" 的實例, then number 小於 .

(=>
      (instance
            ?SECOND
            (SecondFn ?NUMBER ?MINUTE))
      (lessThan ?NUMBER 60))

If second1 是 "秒鐘函數(number1,minute)" 的實例 and second2 是 "秒鐘函數(number2,minute)" 的實例 and "(number2-number1)" 等於 , then second1 (沒) 相接s second2.

(=>
      (and
            (instance
                  ?SECOND1
                  (SecondFn ?NUMBER1 ?MINUTE))
            (instance
                  ?SECOND2
                  (SecondFn ?NUMBER2 ?MINUTE))
            (equal
                  (SubtractionFn ?NUMBER2 ?NUMBER1)
                  1))
      (meetsTemporally ?SECOND1 ?SECOND2))

If year 是年的實例, then year 的持續是 " 年計(s)".

(=>
      (instance ?YEAR Year)
      (duration
            ?YEAR
            (MeasureFn 1 YearDuration)))

If year1 是年的實例 and year2 是年的實例 and "(year2-year1)" 等於 , then year1 (沒) 相接s year2.

(=>
      (and
            (instance ?YEAR1 Year)
            (instance ?YEAR2 Year)
            (equal
                  (SubtractionFn ?YEAR2 ?YEAR1)
                  1))
      (meetsTemporally ?YEAR1 ?YEAR2))

If leap 是閏年的實例 and leap 等於 "number 年(s)", then

"number 取餘數 " 等於 and "number 取餘數 " 等於
"number 取餘數 " 等於

(=>
      (and
            (instance ?LEAP LeapYear)
            (equal
                  ?LEAP
                  (MeasureFn ?NUMBER Year)))
      (or
            (and
                  (equal
                        (RemainderFn ?NUMBER 4)
                        0)
                  (not
                        (equal
                              (RemainderFn ?NUMBER 100)
                              0)))
            (equal
                  (RemainderFn ?NUMBER 400)
                  0)))

If month 是一月的實例, then month 的持續是 " 日計(s)".

(=>
      (instance ?MONTH January)
      (duration
            ?MONTH
            (MeasureFn 31 DayDuration)))

If month1 等於 "月份一月" and month2 等於 "月份二月", then month1 (沒) 相接s month2.

(=>
      (and
            (equal
                  ?MONTH1
                  (MonthFn January ?YEAR))
            (equal
                  ?MONTH2
                  (MonthFn February ?YEAR)))
      (meetsTemporally ?MONTH1 ?MONTH2))

If "月份二月" 等於 month and year 是閏年的實例, then month 的持續是 " 日計(s)".

(=>
      (and
            (equal
                  (MonthFn February ?YEAR)
                  ?MONTH)
            (not
                  (instance ?YEAR LeapYear)))
      (duration
            ?MONTH
            (MeasureFn 28 DayDuration)))

If "月份二月" 等於 month and year 是閏年的實例, then month 的持續是 " 日計(s)".

(=>
      (and
            (equal
                  (MonthFn February ?YEAR)
                  ?MONTH)
            (instance ?YEAR LeapYear))
      (duration
            ?MONTH
            (MeasureFn 29 DayDuration)))

If month1 等於 "月份二月" and month2 等於 "月份三月", then month1 (沒) 相接s month2.

(=>
      (and
            (equal
                  ?MONTH1
                  (MonthFn February ?YEAR))
            (equal
                  ?MONTH2
                  (MonthFn March ?YEAR)))
      (meetsTemporally ?MONTH1 ?MONTH2))

If month 是三月的實例, then month 的持續是 " 日計(s)".

(=>
      (instance ?MONTH March)
      (duration
            ?MONTH
            (MeasureFn 31 DayDuration)))

If month1 等於 "月份三月" and month2 等於 "月份四月", then month1 (沒) 相接s month2.

(=>
      (and
            (equal
                  ?MONTH1
                  (MonthFn March ?YEAR))
            (equal
                  ?MONTH2
                  (MonthFn April ?YEAR)))
      (meetsTemporally ?MONTH1 ?MONTH2))

If month 是四月的實例, then month 的持續是 " 日計(s)".

(=>
      (instance ?MONTH April)
      (duration
            ?MONTH
            (MeasureFn 30 DayDuration)))

If month1 等於 "月份四月" and month2 等於 "月份五月", then month1 (沒) 相接s month2.

(=>
      (and
            (equal
                  ?MONTH1
                  (MonthFn April ?YEAR))
            (equal
                  ?MONTH2
                  (MonthFn May ?YEAR)))
      (meetsTemporally ?MONTH1 ?MONTH2))

If month 是五月的實例, then month 的持續是 " 日計(s)".

(=>
      (instance ?MONTH May)
      (duration
            ?MONTH
            (MeasureFn 31 DayDuration)))

If month1 等於 "月份五月" and month2 等於 "月份六月", then month1 (沒) 相接s month2.

(=>
      (and
            (equal
                  ?MONTH1
                  (MonthFn May ?YEAR))
            (equal
                  ?MONTH2
                  (MonthFn June ?YEAR)))
      (meetsTemporally ?MONTH1 ?MONTH2))

If month 是六月的實例, then month 的持續是 " 日計(s)".

(=>
      (instance ?MONTH June)
      (duration
            ?MONTH
            (MeasureFn 30 DayDuration)))

If month1 等於 "月份六月" and month2 等於 "月份七月", then month1 (沒) 相接s month2.

(=>
      (and
            (equal
                  ?MONTH1
                  (MonthFn June ?YEAR))
            (equal
                  ?MONTH2
                  (MonthFn July ?YEAR)))
      (meetsTemporally ?MONTH1 ?MONTH2))

If month 是七月的實例, then month 的持續是 " 日計(s)".

(=>
      (instance ?MONTH July)
      (duration
            ?MONTH
            (MeasureFn 31 DayDuration)))

If month1 等於 "月份七月" and month2 等於 "月份八月", then month1 (沒) 相接s month2.

(=>
      (and
            (equal
                  ?MONTH1
                  (MonthFn July ?YEAR))
            (equal
                  ?MONTH2
                  (MonthFn August ?YEAR)))
      (meetsTemporally ?MONTH1 ?MONTH2))

If month 是八月的實例, then month 的持續是 " 日計(s)".

(=>
      (instance ?MONTH August)
      (duration
            ?MONTH
            (MeasureFn 31 DayDuration)))

If month1 等於 "月份八月" and month2 等於 "月份九月", then month1 (沒) 相接s month2.

(=>
      (and
            (equal
                  ?MONTH1
                  (MonthFn August ?YEAR))
            (equal
                  ?MONTH2
                  (MonthFn September ?YEAR)))
      (meetsTemporally ?MONTH1 ?MONTH2))

If month 是九月的實例, then month 的持續是 " 日計(s)".

(=>
      (instance ?MONTH September)
      (duration
            ?MONTH
            (MeasureFn 30 DayDuration)))

If month1 等於 "月份九月" and month2 等於 "月份十月", then month1 (沒) 相接s month2.

(=>
      (and
            (equal
                  ?MONTH1
                  (MonthFn September ?YEAR))
            (equal
                  ?MONTH2
                  (MonthFn October ?YEAR)))
      (meetsTemporally ?MONTH1 ?MONTH2))

If month 是十月的實例, then month 的持續是 " 日計(s)".

(=>
      (instance ?MONTH October)
      (duration
            ?MONTH
            (MeasureFn 31 DayDuration)))

If month1 等於 "月份十月" and month2 等於 "月份十一月", then month1 (沒) 相接s month2.

(=>
      (and
            (equal
                  ?MONTH1
                  (MonthFn October ?YEAR))
            (equal
                  ?MONTH2
                  (MonthFn November ?YEAR)))
      (meetsTemporally ?MONTH1 ?MONTH2))

If month 是十一月的實例, then month 的持續是 " 日計(s)".

(=>
      (instance ?MONTH November)
      (duration
            ?MONTH
            (MeasureFn 30 DayDuration)))

If month1 等於 "月份十一月" and month2 等於 "月份十二月", then month1 (沒) 相接s month2.

(=>
      (and
            (equal
                  ?MONTH1
                  (MonthFn November ?YEAR))
            (equal
                  ?MONTH2
                  (MonthFn December ?YEAR)))
      (meetsTemporally ?MONTH1 ?MONTH2))

If month 是十二月的實例, then month 的持續是 " 日計(s)".

(=>
      (instance ?MONTH December)
      (duration
            ?MONTH
            (MeasureFn 31 DayDuration)))

If month1 等於 "月份十二月" and month2 等於 "月份一月" and year1 (沒) 相接s year2, then month1 (沒) 相接s month2.

(=>
      (and
            (equal
                  ?MONTH1
                  (MonthFn December ?YEAR1))
            (equal
                  ?MONTH2
                  (MonthFn January ?YEAR2))
            (meetsTemporally ?YEAR1 ?YEAR2))
      (meetsTemporally ?MONTH1 ?MONTH2))

If day 是日的實例, then day 的持續是 " 日計(s)".

(=>
      (instance ?DAY Day)
      (duration
            ?DAY
            (MeasureFn 1 DayDuration)))

If day1 是星期一的實例 and day2 是星期二的實例 and week 是週的實例 and day1 是 week 的部分 and day2 是 week 的部分, then day1 (沒) 相接s day2.

(=>
      (and
            (instance ?DAY1 Monday)
            (instance ?DAY2 Tuesday)
            (instance ?WEEK Week)
            (temporalPart ?DAY1 ?WEEK)
            (temporalPart ?DAY2 ?WEEK))
      (meetsTemporally ?DAY1 ?DAY2))

If day1 是星期二的實例 and day2 是星期三的實例 and week 是週的實例 and day1 是 week 的部分 and day2 是 week 的部分, then day1 (沒) 相接s day2.

(=>
      (and
            (instance ?DAY1 Tuesday)
            (instance ?DAY2 Wednesday)
            (instance ?WEEK Week)
            (temporalPart ?DAY1 ?WEEK)
            (temporalPart ?DAY2 ?WEEK))
      (meetsTemporally ?DAY1 ?DAY2))

If day1 是星期三的實例 and day2 是星期四的實例 and week 是週的實例 and day1 是 week 的部分 and day2 是 week 的部分, then day1 (沒) 相接s day2.

(=>
      (and
            (instance ?DAY1 Wednesday)
            (instance ?DAY2 Thursday)
            (instance ?WEEK Week)
            (temporalPart ?DAY1 ?WEEK)
            (temporalPart ?DAY2 ?WEEK))
      (meetsTemporally ?DAY1 ?DAY2))

If day1 是星期四的實例 and day2 是星期五的實例 and week 是週的實例 and day1 是 week 的部分 and day2 是 week 的部分, then day1 (沒) 相接s day2.

(=>
      (and
            (instance ?DAY1 Thursday)
            (instance ?DAY2 Friday)
            (instance ?WEEK Week)
            (temporalPart ?DAY1 ?WEEK)
            (temporalPart ?DAY2 ?WEEK))
      (meetsTemporally ?DAY1 ?DAY2))

If day1 是星期五的實例 and day2 是星期六的實例 and week 是週的實例 and day1 是 week 的部分 and day2 是 week 的部分, then day1 (沒) 相接s day2.

(=>
      (and
            (instance ?DAY1 Friday)
            (instance ?DAY2 Saturday)
            (instance ?WEEK Week)
            (temporalPart ?DAY1 ?WEEK)
            (temporalPart ?DAY2 ?WEEK))
      (meetsTemporally ?DAY1 ?DAY2))

If day1 是星期六的實例 and day2 是星期日的實例 and week 是週的實例 and day1 是 week 的部分 and day2 是 week 的部分, then day1 (沒) 相接s day2.

(=>
      (and
            (instance ?DAY1 Saturday)
            (instance ?DAY2 Sunday)
            (instance ?WEEK Week)
            (temporalPart ?DAY1 ?WEEK)
            (temporalPart ?DAY2 ?WEEK))
      (meetsTemporally ?DAY1 ?DAY2))

If day1 是星期日的實例 and day2 是星期一的實例 and week1 是週的實例 and week2 是週的實例 and day1 是 week1 的部分 and day2 是 week2 的部分 and week1 (沒) 相接s week2, then day1 (沒) 相接s day2.

(=>
      (and
            (instance ?DAY1 Sunday)
            (instance ?DAY2 Monday)
            (instance ?WEEK1 Week)
            (instance ?WEEK2 Week)
            (temporalPart ?DAY1 ?WEEK1)
            (temporalPart ?DAY2 ?WEEK2)
            (meetsTemporally ?WEEK1 ?WEEK2))
      (meetsTemporally ?DAY1 ?DAY2))

If week 是週的實例, then week 的持續是 " 周計(s)".

(=>
      (instance ?WEEK Week)
      (duration
            ?WEEK
            (MeasureFn 1 WeekDuration)))

If hour 是小時的實例, then hour 的持續是 " 時計(s)".

(=>
      (instance ?HOUR Hour)
      (duration
            ?HOUR
            (MeasureFn 1 HourDuration)))

If minute 是分的實例, then minute 的持續是 " 分計(s)".

(=>
      (instance ?MINUTE Minute)
      (duration
            ?MINUTE
            (MeasureFn 1 MinuteDuration)))

If second 是秒的實例, then second 的持續是 " 秒計(s)".

(=>
      (instance ?SECOND Second)
      (duration
            ?SECOND
            (MeasureFn 1 SecondDuration)))

if "interval 分解成 ? interval-types" 等於 class,
then for all time1,time2 holds: if time1 是 interval-type 的實例 and time2 是 class 的實例, then there exists duration so that time1 的持續是 duration and time2 的持續是 duration

(=>
      (equal
            (TemporalCompositionFn ?INTERVAL ?INTERVAL-TYPE)
            ?CLASS)
      (forall
            (?TIME1 ?TIME2)
            (=>
                  (and
                        (instance ?TIME1 ?INTERVAL-TYPE)
                        (instance ?TIME2 ?CLASS))
                  (exists
                        (?DURATION)
                        (and
                              (duration ?TIME1 ?DURATION)
                              (duration ?TIME2 ?DURATION))))))

if "interval 分解成 ? interval-types" 等於 class,
then for all time1,time2 holds: if time1 是 class 的實例 and time2 是 class 的實例 and time1 等於 time2, then time1 (沒) 相接s time2 or time2 (沒) 相接s time1 or time1 (沒) 比 time2 較早發生not(s) or time2 (沒) 比 time1 較早發生not(s)

(=>
      (equal
            (TemporalCompositionFn ?INTERVAL ?INTERVAL-TYPE)
            ?CLASS)
      (forall
            (?TIME1 ?TIME2)
            (=>
                  (and
                        (instance ?TIME1 ?CLASS)
                        (instance ?TIME2 ?CLASS)
                        (not
                              (equal ?TIME1 ?TIME2)))
                  (or
                        (meetsTemporally ?TIME1 ?TIME2)
                        (meetsTemporally ?TIME2 ?TIME1)
                        (earlier ?TIME1 ?TIME2)
                        (earlier ?TIME2 ?TIME1)))))

If "interval 分解成 ? interval-types" 等於 class, then there exists class time so that time (沒) �}始s interval.

(=>
      (equal
            (TemporalCompositionFn ?INTERVAL ?INTERVAL-TYPE)
            ?CLASS)
      (exists
            (?TIME)
            (and
                  (instance ?TIME ?CLASS)
                  (starts ?TIME ?INTERVAL))))

If "interval 分解成 ? interval-types" 等於 class, then there exists class time so that time (沒) 完成s interval.

(=>
      (equal
            (TemporalCompositionFn ?INTERVAL ?INTERVAL-TYPE)
            ?CLASS)
      (exists
            (?TIME)
            (and
                  (instance ?TIME ?CLASS)
                  (finishes ?TIME ?INTERVAL))))

if "interval 分解成 ? interval-types" 等於 class,
then for all time1 holds: if time1 是 class 的實例 and time1 not(沒) 完成 interval, then there exists class time2 so that time1 (沒) 相接s time2

(=>
      (equal
            (TemporalCompositionFn ?INTERVAL ?INTERVAL-TYPE)
            ?CLASS)
      (forall
            (?TIME1)
            (=>
                  (and
                        (instance ?TIME1 ?CLASS)
                        (not
                              (finishes ?TIME1 ?INTERVAL)))
                  (exists
                        (?TIME2)
                        (and
                              (instance ?TIME2 ?CLASS)
                              (meetsTemporally ?TIME1 ?TIME2))))))

if "interval 分解成 ? interval-types" 等於 class,
then for all time1 holds: if time1 是 class 的實例 and time1 not(沒) �}始 interval, then there exists class time2 so that time2 (沒) 相接s time1

(=>
      (equal
            (TemporalCompositionFn ?INTERVAL ?INTERVAL-TYPE)
            ?CLASS)
      (forall
            (?TIME1)
            (=>
                  (and
                        (instance ?TIME1 ?CLASS)
                        (not
                              (starts ?TIME1 ?INTERVAL)))
                  (exists
                        (?TIME2)
                        (and
                              (instance ?TIME2 ?CLASS)
                              (meetsTemporally ?TIME2 ?TIME1))))))

if "interval 分解成 ? interval-types" 等於 class,
then for all time holds: if time 是時點的實例 and time 是 interval 的部分, then there exists class instance so that time 是 instance 的部分

(=>
      (equal
            (TemporalCompositionFn ?INTERVAL ?INTERVAL-TYPE)
            ?CLASS)
      (forall
            (?TIME)
            (=>
                  (and
                        (instance ?TIME TimePoint)
                        (temporalPart ?TIME ?INTERVAL))
                  (exists
                        (?INSTANCE)
                        (and
                              (instance ?INSTANCE ?CLASS)
                              (temporalPart ?TIME ?INSTANCE))))))

If year 是年的實例, then ""year 分解成 ? 月s" 中實例的數目" 等於 .

(=>
      (instance ?YEAR Year)
      (equal
            (CardinalityFn
                  (TemporalCompositionFn ?YEAR Month))
            12))

If month 是月的實例 and month 的持續是 "number 日計(s)", then ""month 分解成 ? 日s" 中實例的數目" 等於 number.

(=>
      (and
            (instance ?MONTH Month)
            (duration
                  ?MONTH
                  (MeasureFn ?NUMBER DayDuration)))
      (equal
            (CardinalityFn
                  (TemporalCompositionFn ?MONTH Day))
            ?NUMBER))

If week 是週的實例, then ""week 分解成 ? 日s" 中實例的數目" 等於 .

(=>
      (instance ?WEEK Week)
      (equal
            (CardinalityFn
                  (TemporalCompositionFn ?WEEK Day))
            7))

If day 是日的實例, then ""day 分解成 ? 小時s" 中實例的數目" 等於 .

(=>
      (instance ?DAY Day)
      (equal
            (CardinalityFn
                  (TemporalCompositionFn ?DAY Hour))
            24))

If hour 是小時的實例, then ""hour 分解成 ? 分s" 中實例的數目" 等於 .

(=>
      (instance ?HOUR Hour)
      (equal
            (CardinalityFn
                  (TemporalCompositionFn ?HOUR Minute))
            60))

If minute 是分的實例, then ""minute 分解成 ? 秒s" 中實例的數目" 等於 .

(=>
      (instance ?MINUTE Minute)
      (equal
            (CardinalityFn
                  (TemporalCompositionFn ?MINUTE Second))
            60))

If obj1 與 obj2 相連, then obj1 (沒) 接觸s obj2 or obj1 (沒) 與 obj2 重�|s.

(=>
      (connected ?OBJ1 ?OBJ2)
      (or
            (meetsSpatially ?OBJ1 ?OBJ2)
            (overlapsSpatially ?OBJ1 ?OBJ2)))

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))))

If obj 部分位於 region, then obj (沒) 與 region 重�|s.

(=>
      (partlyLocated ?OBJ ?REGION)
      (overlapsSpatially ?OBJ ?REGION))

If obj1 是 coll的成員 and obj2 是 coll的成員 and obj1 等於 obj2, then obj1 not(沒) 與 obj2 重�|.

(=>
      (and
            (member ?OBJ1 ?COLL)
            (member ?OBJ2 ?COLL)
            (not
                  (equal ?OBJ1 ?OBJ2)))
      (not
            (overlapsSpatially ?OBJ1 ?OBJ2)))

If rel 是格位角色的實例 and rel(process,obj) (不) 成立s, then there exists time so that "process 在 time 的 time位置" (沒) 與 obj 重�|s.

(=>
      (and
            (instance ?REL CaseRole)
            (holds ?REL ?PROCESS ?OBJ))
      (exists
            (?TIME)
            (overlapsSpatially
                  (WhereFn ?PROCESS ?TIME)
                  ?OBJ)))

If obj1 是 obj2的 �~表部分, then obj1 是 obj2 的一內部 and there doesn't exist obj3 so that obj3 是 obj1 的一內部.

(=>
      (superficialPart ?OBJ1 ?OBJ2)
      (and
            (not
                  (interiorPart ?OBJ1 ?OBJ2))
            (not
                  (exists
                        (?OBJ3)
                        (interiorPart ?OBJ3 ?OBJ1)))))

if obj1 是 obj2 的表面,
then for all obj3 holds: if obj3 是 obj2的 �~表部分, then obj3 是 obj1 的部分)

(=>
      (surface ?OBJ1 ?OBJ2)
      (forall
            (?OBJ3)
            (=>
                  (superficialPart ?OBJ3 ?OBJ2)
                  (part ?OBJ3 ?OBJ1))))

if obj1 是 obj2 的一內部,
then for all part holds: if part 是 obj2的 �~表部分, then obj1 not(沒) 與 part 重�|

(=>
      (interiorPart ?OBJ1 ?OBJ2)
      (forall
            (?PART)
            (=>
                  (superficialPart ?PART ?OBJ2)
                  (not
                        (overlapsSpatially ?OBJ1 ?PART)))))

If object 的底部是 bottom and part 是 object 的部分) and part 與 bottom 相連, then part 對 bottom 是在...之上.

(=>
      (and
            (bottom ?BOTTOM ?OBJECT)
            (part ?PART ?OBJECT)
            (not
                  (connected ?PART ?BOTTOM)))
      (orientation ?PART ?BOTTOM Above))

If object 的頂端是 top and part 是 object 的部分) and part 與 top 相連, then part 對 top 是在...之下.

(=>
      (and
            (top ?TOP ?OBJECT)
            (part ?PART ?OBJECT)
            (not
                  (connected ?PART ?TOP)))
      (orientation ?PART ?TOP Below))

If object 的側面是 side and part 是 object 的部分) and part 與 side 相連, then there exists direct so that side 對 part 是 direct.

(=>
      (and
            (side ?SIDE ?OBJECT)
            (part ?PART ?OBJECT)
            (not
                  (connected ?PART ?SIDE)))
      (exists
            (?DIRECT)
            (orientation ?SIDE ?PART ?DIRECT)))

If object 的高度是 height and object 的頂端是 top and object 的底部是 bottom, then top 和 bottom 之間距離是 height.

(=>
      (and
            (height ?OBJECT ?HEIGHT)
            (top ?TOP ?OBJECT)
            (bottom ?BOTTOM ?OBJECT))
      (distance ?TOP ?BOTTOM ?HEIGHT))

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))))))

If hole 在 obj 是 �}, then obj 是洞的實例.

(=>
      (hole ?HOLE ?OBJ)
      (not
            (instance ?OBJ Hole)))

If hole 在 obj 是 �}, then hole not(沒) 與 obj 重�|.

(=>
      (hole ?HOLE ?OBJ)
      (not
            (overlapsSpatially ?HOLE ?OBJ)))

If hole 在 obj1 是 �} and hole 在 obj2 是 �}, then there exists obj3 so that obj3 是 "obj1 和 obj2 的交集" 的正部分 and hole 在 obj3 是 �}.

(=>
      (and
            (hole ?HOLE ?OBJ1)
            (hole ?HOLE ?OBJ2))
      (exists
            (?OBJ3)
            (and
                  (properPart
                        ?OBJ3
                        (MereologicalProductFn ?OBJ1 ?OBJ2))
                  (hole ?HOLE ?OBJ3))))

if hole1 在 obj 是 �} and hole2 在 obj 是 �},
then for all hole3 holds: if hole3 是 "hole1 和 hole2 的聯集" 的部分), then hole3 在 obj 是 �}

(=>
      (and
            (hole ?HOLE1 ?OBJ)
            (hole ?HOLE2 ?OBJ))
      (forall
            (?HOLE3)
            (=>
                  (part
                        ?HOLE3
                        (MereologicalSumFn ?HOLE1 ?HOLE2))
                  (hole ?HOLE3 ?OBJ))))

If hole 在 obj1 是 �} and obj1 是 obj2 的部分), then hole (沒) 與 obj2 重�|s or hole 在 obj2 是 �}.

(=>
      (and
            (hole ?HOLE ?OBJ1)
            (part ?OBJ1 ?OBJ2))
      (or
            (overlapsSpatially ?HOLE ?OBJ2)
            (hole ?HOLE ?OBJ2)))

If hole1 在 obj1 是 �} and hole2 在 obj2 是 �} and hole1 (沒) 與 hole2 重�|s, then obj1 (沒) 與 obj2 重�|s.

(=>
      (and
            (hole ?HOLE1 ?OBJ1)
            (hole ?HOLE2 ?OBJ2)
            (overlapsSpatially ?HOLE1 ?HOLE2))
      (overlapsSpatially ?OBJ1 ?OBJ2))

If hole1 是洞的實例, then there exists hole2 so that hole2 是 hole1 的正部分.

(=>
      (instance ?HOLE1 Hole)
      (exists
            (?HOLE2)
            (properPart ?HOLE2 ?HOLE1)))

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))))))

If hole 在 obj 是 �}, then hole 與 obj 相連.

(=>
      (hole ?HOLE ?OBJ)
      (connected ?HOLE ?OBJ))

If hole1 是洞的實例 and hole2 是 hole1 的正部分, then there exists obj so that hole1 (沒) 接觸s obj and hole2 not(沒) 接觸 obj.

(=>
      (and
            (instance ?HOLE1 Hole)
            (properPart ?HOLE2 ?HOLE1))
      (exists
            (?OBJ)
            (and
                  (meetsSpatially ?HOLE1 ?OBJ)
                  (not
                        (meetsSpatially ?HOLE2 ?OBJ)))))

If there exists time so that obj (沒) 填充s hole timea(之中) time, then 可填充的是 hole 的屬性.

(=>
      (exists
            (?TIME)
            (holdsDuring
                  ?TIME
                  (fills ?OBJ ?HOLE)))
      (attribute ?HOLE Fillable))

If obj (沒) 部分填充s hole1, then there exists hole2 so that hole2 是 hole1 的部分) and obj (沒) 填充s hole2.

(=>
      (partiallyFills ?OBJ ?HOLE1)
      (exists
            (?HOLE2)
            (and
                  (part ?HOLE2 ?HOLE1)
                  (completelyFills ?OBJ ?HOLE2))))

If obj (沒) 適當填充s hole1, then there exists hole2 so that hole2 是 hole1 的部分) and obj (沒) 填充s hole2.

(=>
      (properlyFills ?OBJ ?HOLE1)
      (exists
            (?HOLE2)
            (and
                  (part ?HOLE2 ?HOLE1)
                  (fills ?OBJ ?HOLE2))))

If obj1 (沒) 填充s hole, then there exists obj2 so that obj2 是 obj1 的部分) and obj2 (沒) 填充s hole.

(=>
      (completelyFills ?OBJ1 ?HOLE)
      (exists
            (?OBJ2)
            (and
                  (part ?OBJ2 ?OBJ1)
                  (fills ?OBJ2 ?HOLE))))

If obj1 (沒) 填充s hole and 可填充的是 obj2 的屬性, then obj1 not(沒) 與 obj2 重�|.

(=>
      (and
            (fills ?OBJ1 ?HOLE)
            (attribute ?OBJ2 Fillable))
      (not
            (overlapsSpatially ?OBJ1 ?OBJ2)))

if obj1 (沒) 填充s hole,
then for all obj2 holds: if obj2 與 hole 相連, then obj2 與 obj1 相連

(=>
      (completelyFills ?OBJ1 ?HOLE)
      (forall
            (?OBJ2)
            (=>
                  (connected ?OBJ2 ?HOLE)
                  (connected ?OBJ2 ?OBJ1))))

If obj1 (沒) 適當填充s hole and obj2 與 obj1 相連, then hole 與 obj2 相連.

(=>
      (and
            (properlyFills ?OBJ1 ?HOLE)
            (connected ?OBJ2 ?OBJ1))
      (connected ?HOLE ?OBJ2))

If obj (沒) 填充s hole1 and hole2 是 hole1 的正部分, then obj (沒) 填充s hole2.

(=>
      (and
            (fills ?OBJ ?HOLE1)
            (properPart ?HOLE2 ?HOLE1))
      (completelyFills ?OBJ ?HOLE2))

If obj1 (沒) 填充s hole and obj2 是 obj1 的正部分, then obj2 (沒) 適當填充s hole.

(=>
      (and
            (fills ?OBJ1 ?HOLE)
            (properPart ?OBJ2 ?OBJ1))
      (properlyFills ?OBJ2 ?HOLE))

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))))))

If subproc 是 proc 的次歷�{, then "subproc 存在的時間" 等於 "proc 存在的時間" or "subproc 存在的時間" (沒) 發生not(s) 在 "proc 存在的時間" 期間.

(=>
      (subProcess ?SUBPROC ?PROC)
      (or
            (equal
                  (WhenFn ?SUBPROC)
                  (WhenFn ?PROC))
            (during
                  (WhenFn ?SUBPROC)
                  (WhenFn ?PROC))))

if subproc 是 proc 的次歷�{,
then for all region holds: if proc 位於 region, then subproc 位於 region

(=>
      (subProcess ?SUBPROC ?PROC)
      (forall
            (?REGION)
            (=>
                  (located ?PROC ?REGION)
                  (located ?SUBPROC ?REGION))))

If proc 是歷程的實例 and subproc 是 proc 的次歷�{, then there exists time so that subproc (不) 存在s time 期間.

(=>
      (and
            (instance ?PROC Process)
            (subProcess ?SUBPROC ?PROC))
      (exists
            (?TIME)
            (time ?SUBPROC ?TIME)))

If proc 是生物歷程的實例, then there exists 生物體 obj so that proc 位於 obj.

(=>
      (instance ?PROC BiologicalProcess)
      (exists
            (?OBJ)
            (and
                  (instance ?OBJ Organism)
                  (located ?PROC ?OBJ))))

If proc 是生物歷程的實例 and org (沒) 體驗not(s) proc, then org 是生物體的實例.

(=>
      (and
            (instance ?PROC BiologicalProcess)
            (experiencer ?PROC ?ORG))
      (instance ?ORG Organism))

If birth 是誕生的實例 and agent (沒) 體驗not(s) birth, then there exists 死亡 death so that agent (沒) 體驗not(s) death.

(=>
      (and
            (instance ?BIRTH Birth)
            (experiencer ?BIRTH ?AGENT))
      (exists
            (?DEATH)
            (and
                  (instance ?DEATH Death)
                  (experiencer ?DEATH ?AGENT))))

If death 是死亡的實例 and agent (沒) 體驗not(s) death, then 死是 agent 的屬性 ""death 存在的時間" 之後"a(之中) "death 存在的時間" 之後.

(=>
      (and
            (instance ?DEATH Death)
            (experiencer ?DEATH ?AGENT))
      (holdsDuring
            (FutureFn
                  (WhenFn ?DEATH))
            (attribute ?AGENT Dead)))

If death 是死亡的實例 and birth 是誕生的實例 and agent (沒) 體驗not(s) death and agent (沒) 體驗not(s) birth, then there exists time so that "birth 存在的時間" (沒) 相接s time and time (沒) 相接s "death 存在的時間" and 活的是 agent 的屬性 timea(之中) time.

(=>
      (and
            (instance ?DEATH Death)
            (instance ?BIRTH Birth)
            (experiencer ?DEATH ?AGENT)
            (experiencer ?BIRTH ?AGENT))
      (exists
            (?TIME)
            (and
                  (meetsTemporally
                        (WhenFn ?BIRTH)
                        ?TIME)
                  (meetsTemporally
                        ?TIME
                        (WhenFn ?DEATH))
                  (holdsDuring
                        ?TIME
                        (attribute ?AGENT Living)))))

If act 是攝食的實例 and food 是 act 的受事者, then food 是食物的實例.

(=>
      (and
            (instance ?ACT Ingesting)
            (patient ?ACT ?FOOD))
      (instance ?FOOD Food))

If act 是吃的實例 and food 是 act 的受事者, then 固體的是 food 的屬性.

(=>
      (and
            (instance ?ACT Eating)
            (patient ?ACT ?FOOD))
      (attribute ?FOOD Solid))

If digest 是消化的實例 and digest 是 organism 的施事者, then there exists 攝食 ingest so that ingest 是 organism 的施事者 and "digest 存在的時間" (沒) 與 1 ?重疊s.

(=>
      (and
            (instance ?DIGEST Digesting)
            (agent ?DIGEST ?ORGANISM))
      (exists
            (?INGEST)
            (and
                  (instance ?INGEST Ingesting)
                  (agent ?INGEST ?ORGANISM)
                  (overlapsTemporally
                        (WhenFn ?INGEST)
                        (WhenFn ?DIGEST)))))

If digest 是消化的實例, then there exists 化學分解 decomp so that decomp 是 digest 的次歷�{.

(=>
      (instance ?DIGEST Digesting)
      (exists
            (?DECOMP)
            (and
                  (instance ?DECOMP ChemicalDecomposition)
                  (subProcess ?DECOMP ?DIGEST))))

If rep 是複製的實例 and rep 是 parent 的施事者 and child 是 rep 的結果, then parent 是 child 的雙親.

(=>
      (and
            (instance ?REP Replication)
            (agent ?REP ?PARENT)
            (result ?REP ?CHILD))
      (parent ?CHILD ?PARENT))

If rep 是複製的實例, then there exists 生殖構造 body so that body 是 rep 的結果.

(=>
      (instance ?REP Replication)
      (exists
            (?BODY)
            (and
                  (instance ?BODY ReproductiveBody)
                  (result ?REP ?BODY))))

If rep 是有性生殖的實例 and organism 是 rep 的結果, then there don't exist mother,father so that mother 是 organism 的母親 and father 是 organism 的父親.

(=>
      (and
            (instance ?REP SexualReproduction)
            (result ?REP ?ORGANISM))
      (not
            (exists
                  (?MOTHER ?FATHER)
                  (and
                        (mother ?ORGANISM ?MOTHER)
                        (father ?ORGANISM ?FATHER)))))

If rep 是無性生殖的實例 and organism 是 rep 的結果, then there don't exist parent1,parent2 so that parent1 是 organism 的雙親 and parent2 是 organism 的雙親 and parent1 等於 parent2.

(=>
      (and
            (instance ?REP AsexualReproduction)
            (result ?REP ?ORGANISM))
      (not
            (exists
                  (?PARENT1 ?PARENT2)
                  (and
                        (parent ?ORGANISM ?PARENT1)
                        (parent ?ORGANISM ?PARENT2)
                        (not
                              (equal ?PARENT1 ?PARENT2))))))

If process 是心理歷程的實例, then there exists 動物 animal so that animal (沒) 體驗not(s) process.

(=>
      (instance ?PROCESS PsychologicalProcess)
      (exists
            (?ANIMAL)
            (and
                  (instance ?ANIMAL Animal)
                  (experiencer ?PROCESS ?ANIMAL))))

If proc 是器官或組織歷程的實例, then there exists thing so that proc 位於 thing and thing 是器官的實例 or thing 是組織的實例.

(=>
      (instance ?PROC OrganOrTissueProcess)
      (exists
            (?THING)
            (and
                  (located ?PROC ?THING)
                  (or
                        (instance ?THING Organ)
                        (instance ?THING Tissue)))))

If path 是病理歷程的實例 and org (沒) 體驗not(s) path, then there exist part,疾病或症候群 disease so that part 是 org 的部分) and disease 是 part 的屬性.

(=>
      (and
            (instance ?PATH PathologicProcess)
            (experiencer ?PATH ?ORG))
      (exists
            (?PART ?DISEASE)
            (and
                  (part ?PART ?ORG)
                  (instance ?DISEASE DiseaseOrSyndrome)
                  (attribute ?PART ?DISEASE))))

If inj 是傷害的實例, then there exists 解剖構造 struct so that struct 是 inj 的受事者.

(=>
      (instance ?INJ Injuring)
      (exists
            (?STRUCT)
            (and
                  (instance ?STRUCT AnatomicalStructure)
                  (patient ?INJ ?STRUCT))))

If poison 是中毒的實例, then there exists thing so that thing 是 poison 的受事者 and thing 是生物體的實例 or thing 是解剖構造的實例.

(=>
      (instance ?POISON Poisoning)
      (exists
            (?THING)
            (and
                  (patient ?POISON ?THING)
                  (or
                        (instance ?THING Organism)
                        (instance ?THING AnatomicalStructure)))))

If poison 是中毒的實例, then there exists 活性生物物質 substance so that substance 對 poison 是工具.

(=>
      (instance ?POISON Poisoning)
      (exists
            (?SUBSTANCE)
            (and
                  (instance ?SUBSTANCE BiologicallyActiveSubstance)
                  (instrument ?POISON ?SUBSTANCE))))

If proc 是意向性歷程的實例 and proc 是 agent 的施事者, then there exists purp so that proc 對agent 有意圖 purp.

(=>
      (and
            (instance ?PROC IntentionalProcess)
            (agent ?PROC ?AGENT))
      (exists
            (?PURP)
            (hasPurposeForAgent ?PROC ?PURP ?AGENT)))

If proc 是意向性歷程的實例, then there exists 具認知力施事者 agent so that proc 是 agent 的施事者.

(=>
      (instance ?PROC IntentionalProcess)
      (exists
            (?AGENT)
            (and
                  (instance ?AGENT CognitiveAgent)
                  (agent ?PROC ?AGENT))))

If act 是組織性的歷程的實例 and act 是 agent 的施事者, then

agent 是組織的實例
there exists 組織 org so that agent 是 org的成員

(=>
      (and
            (instance ?ACT OrganizationalProcess)
            (agent ?ACT ?AGENT))
      (or
            (instance ?AGENT Organization)
            (exists
                  (?ORG)
                  (and
                        (instance ?ORG Organization)
                        (member ?AGENT ?ORG)))))

If act 是宗教歷程的實例 and act 是 agent 的施事者, then

agent 是宗教組織的實例
there exists 宗教組織 org so that agent 是 org的成員

(=>
      (and
            (instance ?ACT ReligiousProcess)
            (agent ?ACT ?AGENT))
      (or
            (instance ?AGENT ReligiousOrganization)
            (exists
                  (?ORG)
                  (and
                        (member ?AGENT ?ORG)
                        (instance ?ORG ReligiousOrganization)))))

If join 是加入組織的實例 and org 是組織的實例 and join 是 org 的施事者 and person 是 join 的受事者, then person 是 org的成員 ""join 存在的時間" 不久之後"a(之中) "join 存在的時間" 不久之後.

(=>
      (and
            (instance ?JOIN JoiningAnOrganization)
            (instance ?ORG Organization)
            (agent ?JOIN ?ORG)
            (patient ?JOIN ?PERSON))
      (holdsDuring
            (ImmediateFutureFn
                  (WhenFn ?JOIN))
            (member ?PERSON ?ORG)))

If leave 是脫離組織的實例 and org 是組織的實例 and leave 是 org 的施事者 and person 是 leave 的受事者, then person 是 org的成員 ""leave 存在的時間" 不久之後"a(之中) "leave 存在的時間" 不久之後.

(=>
      (and
            (instance ?LEAVE LeavingAnOrganization)
            (instance ?ORG Organization)
            (agent ?LEAVE ?ORG)
            (patient ?LEAVE ?PERSON))
      (holdsDuring
            (ImmediateFutureFn
                  (WhenFn ?LEAVE))
            (not
                  (member ?PERSON ?ORG))))

If grad 是畢業的實例 and grad 是 org 的施事者 and person 是 grad 的受事者, then org 是教育組織的實例.

(=>
      (and
            (instance ?GRAD Graduation)
            (agent ?GRAD ?ORG)
            (patient ?GRAD ?PERSON))
      (instance ?ORG EducationalOrganization))

If mat 是正式入學的實例 and mat 是 org 的施事者 and person 是 mat 的受事者, then org 是教育組織的實例.

(=>
      (and
            (instance ?MAT Matriculation)
            (agent ?MAT ?ORG)
            (patient ?MAT ?PERSON))
      (instance ?ORG EducationalOrganization))

If hire 是僱用的實例 and org 是組織的實例 and hire 是 org 的施事者 and person 是 hire 的受事者, then org (沒) 雇用not(s) person ""hire 存在的時間" 不久之後"a(之中) "hire 存在的時間" 不久之後.

(=>
      (and
            (instance ?HIRE Hiring)
            (instance ?ORG Organization)
            (agent ?HIRE ?ORG)
            (patient ?HIRE ?PERSON))
      (holdsDuring
            (ImmediateFutureFn
                  (WhenFn ?HIRE))
            (employs ?ORG ?PERSON)))

If fire 是解僱的實例 and org 是組織的實例 and fire 是 org 的施事者 and person 是 fire 的受事者, then org not(沒) 雇用(s) person ""fire 存在的時間" 不久之後"a(之中) "fire 存在的時間" 不久之後.

(=>
      (and
            (instance ?FIRE TerminatingEmployment)
            (instance ?ORG Organization)
            (agent ?FIRE ?ORG)
            (patient ?FIRE ?PERSON))
      (holdsDuring
            (ImmediateFutureFn
                  (WhenFn ?FIRE))
            (not
                  (employs ?ORG ?PERSON))))

If proc 是政治歷程的實例, then there exists 政府 gov so that proc 是 gov 的施事者 or gov 是 proc 的受事者.

(=>
      (instance ?PROC PoliticalProcess)
      (exists
            (?GOV)
            (and
                  (instance ?GOV Government)
                  (or
                        (agent ?PROC ?GOV)
                        (patient ?PROC ?GOV)))))

If increase 是增加的實例 and obj 是 increase 的受事者, then there exist unit,quant1,quant2 so that "obj unit(s)" 等於 quant1 ""increase 存在的時間" 不久之前"a(之中) "increase 存在的時間" 不久之前 and "obj unit(s)" 等於 quant2 ""increase 存在的時間" 不久之後"a(之中) "increase 存在的時間" 不久之後 and quant2 (不) 大於 quant1.

(=>
      (and
            (instance ?INCREASE Increasing)
            (patient ?INCREASE ?OBJ))
      (exists
            (?UNIT ?QUANT1 ?QUANT2)
            (and
                  (holdsDuring
                        (ImmediatePastFn
                              (WhenFn ?INCREASE))
                        (equal
                              (MeasureFn ?OBJ ?UNIT)
                              ?QUANT1))
                  (holdsDuring
                        (ImmediateFutureFn
                              (WhenFn ?INCREASE))
                        (equal
                              (MeasureFn ?OBJ ?UNIT)
                              ?QUANT2))
                  (greaterThan ?QUANT2 ?QUANT1))))

If heat 是加溫的實例 and obj 是 heat 的受事者, then there exist 溫度單位 unit,quant1,quant2 so that "obj unit(s)" 等於 quant1 ""heat 存在的時間" 不久之前"a(之中) "heat 存在的時間" 不久之前 and "obj unit(s)" 等於 quant2 ""heat 存在的時間" 不久之後"a(之中) "heat 存在的時間" 不久之後 and quant2 (不) 大於 quant1.

(=>
      (and
            (instance ?HEAT Heating)
            (patient ?HEAT ?OBJ))
      (exists
            (?UNIT ?QUANT1 ?QUANT2)
            (and
                  (instance ?UNIT TemperatureMeasure)
                  (holdsDuring
                        (ImmediatePastFn
                              (WhenFn ?HEAT))
                        (equal
                              (MeasureFn ?OBJ ?UNIT)
                              ?QUANT1))
                  (holdsDuring
                        (ImmediateFutureFn
                              (WhenFn ?HEAT))
                        (equal
                              (MeasureFn ?OBJ ?UNIT)
                              ?QUANT2))
                  (greaterThan ?QUANT2 ?QUANT1))))

If decrease 是減少的實例 and obj 是 decrease 的受事者, then there exist unit,quant1,quant2 so that "obj unit(s)" 等於 quant1 ""decrease 存在的時間" 不久之前"a(之中) "decrease 存在的時間" 不久之前 and "obj unit(s)" 等於 quant2 ""decrease 存在的時間" 不久之後"a(之中) "decrease 存在的時間" 不久之後 and quant2 小於 quant1.

(=>
      (and
            (instance ?DECREASE Decreasing)
            (patient ?DECREASE ?OBJ))
      (exists
            (?UNIT ?QUANT1 ?QUANT2)
            (and
                  (holdsDuring
                        (ImmediatePastFn
                              (WhenFn ?DECREASE))
                        (equal
                              (MeasureFn ?OBJ ?UNIT)
                              ?QUANT1))
                  (holdsDuring
                        (ImmediateFutureFn
                              (WhenFn ?DECREASE))
                        (equal
                              (MeasureFn ?OBJ ?UNIT)
                              ?QUANT2))
                  (lessThan ?QUANT2 ?QUANT1))))

If cool 是降溫的實例 and obj 是 cool 的受事者, then there exist 溫度單位 unit,quant1,quant2 so that "obj unit(s)" 等於 quant1 ""cool 存在的時間" 不久之前"a(之中) "cool 存在的時間" 不久之前 and "obj unit(s)" 等於 quant2 ""cool 存在的時間" 不久之後"a(之中) "cool 存在的時間" 不久之後 and quant2 小於 quant1.

(=>
      (and
            (instance ?COOL Cooling)
            (patient ?COOL ?OBJ))
      (exists
            (?UNIT ?QUANT1 ?QUANT2)
            (and
                  (instance ?UNIT TemperatureMeasure)
                  (holdsDuring
                        (ImmediatePastFn
                              (WhenFn ?COOL))
                        (equal
                              (MeasureFn ?OBJ ?UNIT)
                              ?QUANT1))
                  (holdsDuring
                        (ImmediateFutureFn
                              (WhenFn ?COOL))
                        (equal
                              (MeasureFn ?OBJ ?UNIT)
                              ?QUANT2))
                  (lessThan ?QUANT2 ?QUANT1))))

If motion 是移動的實例 and obj 是 motion 的受事者 and motion (不) �_源s 於 place, then obj 位於 place ""motion 存在的時間" 不久之前"a(之中) "motion 存在的時間" 不久之前.

(=>
      (and
            (instance ?MOTION Motion)
            (patient ?MOTION ?OBJ)
            (origin ?MOTION ?PLACE))
      (holdsDuring
            (ImmediatePastFn
                  (WhenFn ?MOTION))
            (located ?OBJ ?PLACE)))

If motion 是移動的實例 and obj 是 motion 的受事者 and motion (不) 終結not(s) place, then obj 位於 place ""motion 存在的時間" 不久之後"a(之中) "motion 存在的時間" 不久之後.

(=>
      (and
            (instance ?MOTION Motion)
            (patient ?MOTION ?OBJ)
            (destination ?MOTION ?PLACE))
      (holdsDuring
            (ImmediateFutureFn
                  (WhenFn ?MOTION))
            (located ?OBJ ?PLACE)))

if
- path1 伴隨 process 發生的 process路徑
- process (不) �_源s 於 source
- process (不) 終結not(s) dest
- path1 的長度是 measure1
- there don't exist path2,measure2 so that path2 伴隨 process 發生的 process路徑 and process (不) �_源s 於 origin and process (不) 終結not(s) dest and path2 的長度是 measure2 and measure2 小於 measure1
,
then for all obj holds: if obj 是 path1 的部分), then obj 介於 source 和 dest 中間

(=>
      (and
            (path ?PROCESS ?PATH1)
            (origin ?PROCESS ?SOURCE)
            (destination ?PROCESS ?DEST)
            (length ?PATH1 ?MEASURE1)
            (not
                  (exists
                        (?PATH2 ?MEASURE2)
                        (and
                              (path ?PROCESS ?PATH2)
                              (origin ?PROCESS ?ORIGIN)
                              (destination ?PROCESS ?DEST)
                              (length ?PATH2 ?MEASURE2)
                              (lessThan ?MEASURE2 ?MEASURE1)))))
      (forall
            (?OBJ)
            (=>
                  (part ?OBJ ?PATH1)
                  (between ?SOURCE ?OBJ ?DEST))))

If motion 是身體移動的實例, then there exist 軀體部件 obj,生物體 agent so that obj 是 motion 的受事者 and motion 是 agent 的施事者.

(=>
      (instance ?MOTION BodyMotion)
      (exists
            (?OBJ ?AGENT)
            (and
                  (instance ?OBJ BodyPart)
                  (patient ?MOTION ?OBJ)
                  (instance ?AGENT Organism)
                  (agent ?MOTION ?AGENT))))

If walk 是行走的實例 and walk 是 agent 的施事者, then there exists 陸地 area so that agent 位於 area.

(=>
      (and
            (instance ?WALK Walking)
            (agent ?WALK ?AGENT))
      (exists
            (?AREA)
            (and
                  (instance ?AREA LandArea)
                  (located ?AGENT ?AREA))))

If swim 是遊泳的實例 and swim 是 agent 的施事者, then there exists 水域 area so that agent 位於 area.

(=>
      (and
            (instance ?SWIM Swimming)
            (agent ?SWIM ?AGENT))
      (exists
            (?AREA)
            (and
                  (instance ?AREA WaterArea)
                  (located ?AGENT ?AREA))))

If proc 是方向的改變的實例, then there exists 方向屬性 attr so that

proc 以方式 attr 執行 ""proc 存在的時間" 不久之前"a(之中) "proc 存在的時間" 不久之前 and proc 以方式 attr 執行 ""proc 存在的時間" 不久之後"a(之中) "proc 存在的時間" 不久之後
proc 以方式 attr 執行 ""proc 存在的時間" 不久之後"a(之中) "proc 存在的時間" 不久之後 and proc 以方式 attr 執行 ""proc 存在的時間" 不久之前"a(之中) "proc 存在的時間" 不久之前

(=>
      (instance ?PROC DirectionChange)
      (exists
            (?ATTR)
            (and
                  (instance ?ATTR DirectionalAttribute)
                  (or
                        (and
                              (holdsDuring
                                    (ImmediatePastFn
                                          (WhenFn ?PROC))
                                    (manner ?PROC ?ATTR))
                              (holdsDuring
                                    (ImmediateFutureFn
                                          (WhenFn ?PROC))
                                    (not
                                          (manner ?PROC ?ATTR))))
                        (and
                              (holdsDuring
                                    (ImmediateFutureFn
                                          (WhenFn ?PROC))
                                    (manner ?PROC ?ATTR))
                              (holdsDuring
                                    (ImmediatePastFn
                                          (WhenFn ?PROC))
                                    (not
                                          (manner ?PROC ?ATTR))))))))

If transfer 是轉移或轉換的實例 and transfer 是 agent 的施事者 and patient 是 transfer 的受事者, then agent 等於 patient.

(=>
      (and
            (instance ?TRANSFER Transfer)
            (agent ?TRANSFER ?AGENT)
            (patient ?TRANSFER ?PATIENT))
      (not
            (equal ?AGENT ?PATIENT)))

If remove 是移除的實例 and remove (不) �_源s 於 place and obj 是 remove 的受事者, then obj 位於 place ""remove 存在的時間" 不久之前"a(之中) "remove 存在的時間" 不久之前 and obj 位於 place ""remove 存在的時間" 不久之後"a(之中) "remove 存在的時間" 不久之後.

(=>
      (and
            (instance ?REMOVE Removing)
            (origin ?REMOVE ?PLACE)
            (patient ?REMOVE ?OBJ))
      (and
            (holdsDuring
                  (ImmediatePastFn
                        (WhenFn ?REMOVE))
                  (located ?OBJ ?PLACE))
            (holdsDuring
                  (ImmediateFutureFn
                        (WhenFn ?REMOVE))
                  (not
                        (located ?OBJ ?PLACE)))))

If put 是放置的實例 and put (不) 終結not(s) place and obj 是 put 的受事者, then obj 位於 place ""put 存在的時間" 不久之前"a(之中) "put 存在的時間" 不久之前 and obj 位於 place ""put 存在的時間" 不久之後"a(之中) "put 存在的時間" 不久之後.

(=>
      (and
            (instance ?PUT Putting)
            (destination ?PUT ?PLACE)
            (patient ?PUT ?OBJ))
      (and
            (holdsDuring
                  (ImmediatePastFn
                        (WhenFn ?PUT))
                  (not
                        (located ?OBJ ?PLACE)))
            (holdsDuring
                  (ImmediateFutureFn
                        (WhenFn ?PUT))
                  (located ?OBJ ?PLACE))))

If sub 是替換的實例, then there exist 放置 put,移除 remove,obj1,obj2,place so that put 是 sub 的次歷�{ and remove 是 sub 的次歷�{ and obj1 是 remove 的受事者 and remove (不) �_源s 於 place and obj2 是 put 的受事者 and put (不) 終結not(s) place and obj1 等於 obj2.

(=>
      (instance ?SUB Substituting)
      (exists
            (?PUT ?REMOVE ?OBJ1 ?OBJ2 ?PLACE)
            (and
                  (instance ?PUT Putting)
                  (instance ?REMOVE Removing)
                  (subProcess ?PUT ?SUB)
                  (subProcess ?REMOVE ?SUB)
                  (patient ?REMOVE ?OBJ1)
                  (origin ?REMOVE ?PLACE)
                  (patient ?PUT ?OBJ2)
                  (destination ?PUT ?PLACE)
                  (not
                        (equal ?OBJ1 ?OBJ2)))))

If touch 是觸動的實例 and touch 是 obj1 的施事者 and obj2 是 touch 的受事者, then obj1 與 obj2 相連 ""touch 存在的時間" 不久之後"a(之中) "touch 存在的時間" 不久之後.

(=>
      (and
            (instance ?TOUCH Touching)
            (agent ?TOUCH ?OBJ1)
            (patient ?TOUCH ?OBJ2))
      (holdsDuring
            (ImmediateFutureFn
                  (WhenFn ?TOUCH))
            (connected ?OBJ1 ?OBJ2)))

If impact 是影響的實例 and obj 是 impact 的受事者, then there exists 穿透 impel so that obj 是 impel 的受事者 and "impel 存在的時間" (沒) 比 "impact 存在的時間" 較早發生not(s).

(=>
      (and
            (instance ?IMPACT Impacting)
            (patient ?IMPACT ?OBJ))
      (exists
            (?IMPEL)
            (and
                  (instance ?IMPEL Impelling)
                  (patient ?IMPEL ?OBJ)
                  (earlier
                        (WhenFn ?IMPEL)
                        (WhenFn ?IMPACT)))))

If trans 是運輸的實例, then there exists 運輸工具 device so that device 對 trans 是工具.

(=>
      (instance ?TRANS Transportation)
      (exists
            (?DEVICE)
            (and
                  (instance ?DEVICE TransportationDevice)
                  (instrument ?TRANS ?DEVICE))))

If steer 是引導的實例, then there exists 運輸工具 vehicle so that vehicle 是 steer 的受事者.

(=>
      (instance ?STEER Steering)
      (exists
            (?VEHICLE)
            (and
                  (instance ?VEHICLE TransportationDevice)
                  (patient ?STEER ?VEHICLE))))

If education 是教育歷程的實例 and person 是 education 的受事者, then education 有意圖 "there exists 學習 learn so that person 是 learn 的受事者".

(=>
      (and
            (instance ?EDUCATION EducationalProcess)
            (patient ?EDUCATION ?PERSON))
      (hasPurpose
            ?EDUCATION
            (exists
                  (?LEARN)
                  (and
                        (instance ?LEARN Learning)
                        (patient ?LEARN ?PERSON)))))

If change 是擁有權的轉移的實例 and obj 是 change 的受事者 and agent1 (沒) 擁有not(s) obj ""change 存在的時間" 不久之前"a(之中) "change 存在的時間" 不久之前 and agent2 (沒) 擁有not(s) obj ""change 存在的時間" 不久之後"a(之中) "change 存在的時間" 不久之後, then agent1 等於 agent2.

(=>
      (and
            (instance ?CHANGE ChangeOfPossession)
            (patient ?CHANGE ?OBJ)
            (holdsDuring
                  (ImmediatePastFn
                        (WhenFn ?CHANGE))
                  (possesses ?AGENT1 ?OBJ))
            (holdsDuring
                  (ImmediateFutureFn
                        (WhenFn ?CHANGE))
                  (possesses ?AGENT2 ?OBJ)))
      (not
            (equal ?AGENT1 ?AGENT2)))

If change 是擁有權的轉移的實例 and change (不) �_源s 於 agent1 and change (不) 終結not(s) agent2 and agent2 是施事者的實例 and obj 是 change 的受事者, then agent1 (沒) 擁有not(s) obj ""change 存在的時間" 不久之前"a(之中) "change 存在的時間" 不久之前 and agent2 (沒) 擁有not(s) obj ""change 存在的時間" 不久之後"a(之中) "change 存在的時間" 不久之後.

(=>
      (and
            (instance ?CHANGE ChangeOfPossession)
            (origin ?CHANGE ?AGENT1)
            (destination ?CHANGE ?AGENT2)
            (instance ?AGENT2 Agent)
            (patient ?CHANGE ?OBJ))
      (and
            (holdsDuring
                  (ImmediatePastFn
                        (WhenFn ?CHANGE))
                  (possesses ?AGENT1 ?OBJ))
            (holdsDuring
                  (ImmediateFutureFn
                        (WhenFn ?CHANGE))
                  (possesses ?AGENT2 ?OBJ))))

If give 是給與的實例 and give 是 agent1 的施事者 and give (不) 終結not(s) agent2 and agent2 是施事者的實例 and obj 是 give 的受事者, then there exists 獲取 get so that get 是 agent2 的施事者 and get (不) �_源s 於 agent1 and obj 是 get 的受事者.

(=>
      (and
            (instance ?GIVE Giving)
            (agent ?GIVE ?AGENT1)
            (destination ?GIVE ?AGENT2)
            (instance ?AGENT2 Agent)
            (patient ?GIVE ?OBJ))
      (exists
            (?GET)
            (and
                  (instance ?GET Getting)
                  (agent ?GET ?AGENT2)
                  (origin ?GET ?AGENT1)
                  (patient ?GET ?OBJ))))

If give 是給與的實例 and give 是 agent 的施事者, then give (不) �_源s 於 agent.

(=>
      (and
            (instance ?GIVE Giving)
            (agent ?GIVE ?AGENT))
      (origin ?GIVE ?AGENT))

If give 是單方面的給與的實例, then there doesn't exist 交易 trans so that give 是 trans 的次歷�{.

(=>
      (instance ?GIVE UnilateralGiving)
      (not
            (exists
                  (?TRANS)
                  (and
                        (instance ?TRANS Transaction)
                        (subProcess ?GIVE ?TRANS)))))

If get 是獲取的實例 and get 是 agent 的施事者, then get (不) 終結not(s) agent.

(=>
      (and
            (instance ?GET Getting)
            (agent ?GET ?AGENT))
      (destination ?GET ?AGENT))

If get 是單方面的獲取的實例, then there doesn't exist 交易 trans so that get 是 trans 的次歷�{.

(=>
      (instance ?GET UnilateralGetting)
      (not
            (exists
                  (?TRANS)
                  (and
                        (instance ?TRANS Transaction)
                        (subProcess ?GET ?TRANS)))))

If trans 是交易的實例, then there exist agent1,agent2,給與 give1,給與 give2,obj1,obj2 so that give1 是 trans 的次歷�{ and give2 是 trans 的次歷�{ and give1 是 agent1 的施事者 and give2 是 agent2 的施事者 and obj1 是 give1 的受事者 and obj2 是 give2 的受事者 and give1 (不) 終結not(s) agent2 and give2 (不) 終結not(s) agent1 and agent1 等於 agent2 and obj1 等於 obj2.

(=>
      (instance ?TRANS Transaction)
      (exists
            (?AGENT1 ?AGENT2 ?GIVE1 ?GIVE2 ?OBJ1 ?OBJ2)
            (and
                  (instance ?GIVE1 Giving)
                  (instance ?GIVE2 Giving)
                  (subProcess ?GIVE1 ?TRANS)
                  (subProcess ?GIVE2 ?TRANS)
                  (agent ?GIVE1 ?AGENT1)
                  (agent ?GIVE2 ?AGENT2)
                  (patient ?GIVE1 ?OBJ1)
                  (patient ?GIVE2 ?OBJ2)
                  (destination ?GIVE1 ?AGENT2)
                  (destination ?GIVE2 ?AGENT1)
                  (not
                        (equal ?AGENT1 ?AGENT2))
                  (not
                        (equal ?OBJ1 ?OBJ2)))))

If trans 是金融交易的實例, then there exists 匯率單位 obj so that obj 是 trans 的受事者.

(=>
      (instance ?TRANS FinancialTransaction)
      (exists
            (?OBJ)
            (and
                  (patient ?TRANS ?OBJ)
                  (instance ?OBJ CurrencyMeasure))))

If buy 是買的實例 and buy 是 agent 的施事者, then buy (不) 終結not(s) agent.

(=>
      (and
            (instance ?BUY Buying)
            (agent ?BUY ?AGENT))
      (destination ?BUY ?AGENT))

If sell 是銷售的實例 and sell 是 agent 的施事者, then sell (不) �_源s 於 agent.

(=>
      (and
            (instance ?SELL Selling)
            (agent ?SELL ?AGENT))
      (origin ?SELL ?AGENT))

If learn 是學習的實例 and learn 是 agent 的施事者, then agent 是具認知力施事者的實例.

(=>
      (and
            (instance ?LEARN Learning)
            (agent ?LEARN ?AGENT))
      (instance ?AGENT CognitiveAgent))

If there exists 學習 learn so that learn 是 agent 的施事者 and prop 是 learn 的受事者 timea(之中) time, then agent (不)相信 prop "time 不久之後"a(之中) time 不久之後.

(=>
      (holdsDuring
            ?TIME
            (exists
                  (?LEARN)
                  (and
                        (instance ?LEARN Learning)
                        (agent ?LEARN ?AGENT)
                        (patient ?LEARN ?PROP))))
      (holdsDuring
            (ImmediateFutureFn ?TIME)
            (believes ?AGENT ?PROP)))

If agent 是具認知力施事者的實例, then agent 可以任角色施事者做推理.

(=>
      (instance ?AGENT CognitiveAgent)
      (capability Reasoning agent ?AGENT))

If meas 是測量的實例 and meas 是 agent 的施事者 and obj 是 meas 的受事者, then there exist quant,unit so that agent (不）知道s) %2 ""meas 存在的時間" 不久之後"a(之中) "meas 存在的時間" 不久之後.

(=>
      (and
            (instance ?MEAS Measuring)
            (agent ?MEAS ?AGENT)
            (patient ?MEAS ?OBJ))
      (exists
            (?QUANT ?UNIT)
            (holdsDuring
                  (ImmediateFutureFn
                        (WhenFn ?MEAS))
                  (knows
                        ?AGENT
                        (measure
                              ?OBJ
                              (MeasureFn ?QUANT ?UNIT))))))

If count 是計數的實例 and count 是 agent 的施事者 and entity 是 count 的受事者, then there exists number so that agent (不）知道s) %2.

(=>
      (and
            (instance ?COUNT Counting)
            (agent ?COUNT ?AGENT)
            (patient ?COUNT ?ENTITY))
      (exists
            (?NUMBER)
            (knows
                  ?AGENT
                  (equal
                        (CardinalityFn ?ENTITY)
                        ?NUMBER))))

If predict 是預測的實例 and formula 是 predict 的受事者, then there exists time so that formula (沒) 為真 timea(之中) time and time (沒) 發生?{s} 在 "predict 存在的時間" 之前 or time (沒) 比 "predict 存在的時間" 較早發生not(s).

(=>
      (and
            (instance ?PREDICT Predicting)
            (patient ?PREDICT ?FORMULA))
      (exists
            (?TIME)
            (and
                  (holdsDuring ?TIME ?FORMULA)
                  (or
                        (before
                              ?TIME
                              (WhenFn ?PREDICT))
                        (earlier
                              ?TIME
                              (WhenFn ?PREDICT))))))

If remember 是記憶的實例 and formula 是 remember 的受事者, then there exists time so that formula (沒) 為真 timea(之中) time and time (沒) 發生?{s} 在 "remember 存在的時間" 之前 or time (沒) 比 "remember 存在的時間" 較早發生not(s).

(=>
      (and
            (instance ?REMEMBER Remembering)
            (patient ?REMEMBER ?FORMULA))
      (exists
            (?TIME)
            (and
                  (holdsDuring ?TIME ?FORMULA)
                  (or
                        (before
                              ?TIME
                              (WhenFn ?REMEMBER))
                        (earlier
                              ?TIME
                              (WhenFn ?REMEMBER))))))

If keep 是保有的實例 and keep 是 agent 的施事者 and obj 是 keep 的受事者, then there exists 放置 put so that put 是 agent 的施事者 and obj 是 put 的受事者 and "put 存在的時間" (沒) 比 "keep 存在的時間" 較早發生not(s).

(=>
      (and
            (instance ?KEEP Keeping)
            (agent ?KEEP ?AGENT)
            (patient ?KEEP ?OBJ))
      (exists
            (?PUT)
            (and
                  (instance ?PUT Putting)
                  (agent ?PUT ?AGENT)
                  (patient ?PUT ?OBJ)
                  (earlier
                        (WhenFn ?PUT)
                        (WhenFn ?KEEP)))))

if keep 是保有的實例 and obj 是 keep 的受事者,
then there exists place so that for all time holds: if time 是 "keep 存在的時間" 的部分, then obj 位於 place timea(之中) time

(=>
      (and
            (instance ?KEEP Keeping)
            (patient ?KEEP ?OBJ))
      (exists
            (?PLACE)
            (forall
                  (?TIME)
                  (=>
                        (temporalPart
                              ?TIME
                              (WhenFn ?KEEP))
                        (holdsDuring
                              ?TIME
                              (located ?OBJ ?PLACE))))))

If confine 是限定的實例, then there exists 人類 human so that human 是 confine 的受事者.

(=>
      (instance ?CONFINE Confining)
      (exists
            (?HUMAN)
            (and
                  (instance ?HUMAN Human)
                  (patient ?CONFINE ?HUMAN))))

If confine 是限定的實例 and person 是 confine 的受事者, then person not(不) 冀求(s) "person 是 confine 的受事者".

(=>
      (and
            (instance ?CONFINE Confining)
            (patient ?CONFINE ?PERSON))
      (not
            (desires
                  ?PERSON
                  (patient ?CONFINE ?PERSON))))

If repair 是修護的實例 and obj 是 repair 的受事者, then there exists 損害 damage so that obj 是 damage 的受事者 and "damage 存在的時間" (沒) 比 "repair 存在的時間" 較早發生not(s).

(=>
      (and
            (instance ?REPAIR Repairing)
            (patient ?REPAIR ?OBJ))
      (exists
            (?DAMAGE)
            (and
                  (instance ?DAMAGE Damaging)
                  (patient ?DAMAGE ?OBJ)
                  (earlier
                        (WhenFn ?DAMAGE)
                        (WhenFn ?REPAIR)))))

If proc 是治療歷程的實例 and bio 是 proc 的受事者, then

bio 是生物體的實例
there exists 生物體 org so that bio 是 org 的部分)

(=>
      (and
            (instance ?PROC TherapeuticProcess)
            (patient ?PROC ?BIO))
      (or
            (instance ?BIO Organism)
            (exists
                  (?ORG)
                  (and
                        (instance ?ORG Organism)
                        (part ?BIO ?ORG)))))

If act 是外科手術的實例 and animal 是 act 的受事者, then there exists 切割 subact so that animal 是動物的實例 and cutting 是 animal 的受事者 and subact 是 act 的次歷�{.

(=>
      (and
            (instance ?ACT Surgery)
            (patient ?ACT ?ANIMAL))
      (exists
            (?SUBACT)
            (and
                  (instance ?SUBACT Cutting)
                  (instance ?ANIMAL Animal)
                  (patient ?ANIMAL ?CUTTING)
                  (subProcess ?SUBACT ?ACT))))

If kill 是殺害的實例 and kill 是 agent 的施事者 and patient 是 kill 的受事者, then agent 是生物體的實例 and patient 是生物體的實例.

(=>
      (and
            (instance ?KILL Killing)
            (agent ?KILL ?AGENT)
            (patient ?KILL ?PATIENT))
      (and
            (instance ?AGENT Organism)
            (instance ?PATIENT Organism)))

If kill 是殺害的實例 and patient 是 kill 的受事者, then 活的是 patient 的屬性 ""kill 存在的時間" 不久之前"a(之中) "kill 存在的時間" 不久之前 and 死是 patient 的屬性 ""kill 存在的時間" 之後"a(之中) "kill 存在的時間" 之後.

(=>
      (and
            (instance ?KILL Killing)
            (patient ?KILL ?PATIENT))
      (and
            (holdsDuring
                  (ImmediatePastFn
                        (WhenFn ?KILL))
                  (attribute ?PATIENT Living))
            (holdsDuring
                  (FutureFn
                        (WhenFn ?KILL))
                  (attribute ?PATIENT Dead))))

If poke 是戳的實例 and poke 是 agent 的施事者 and obj 是 poke 的受事者 and inst 對 poke 是工具, then inst 連結 agent 和 obj "poke 存在的時間"a(之中) poke 存在的時間.

(=>
      (and
            (instance ?POKE Poking)
            (agent ?POKE ?AGENT)
            (patient ?POKE ?OBJ)
            (instrument ?POKE ?INST))
      (holdsDuring
            (WhenFn ?POKE)
            (connects ?INST ?AGENT ?OBJ)))

If attach 是貼附的實例 and obj1 是 attach 的受事者 and obj2 是 attach 的受事者, then obj1 與 obj2 相連 ""attach 存在的時間" 不久之前"a(之中) "attach 存在的時間" 不久之前 and obj1 與 obj2 相連 ""attach 存在的時間" 不久之後"a(之中) "attach 存在的時間" 不久之後.

(=>
      (and
            (instance ?ATTACH Attaching)
            (patient ?ATTACH ?OBJ1)
            (patient ?ATTACH ?OBJ2))
      (and
            (holdsDuring
                  (ImmediatePastFn
                        (WhenFn ?ATTACH))
                  (not
                        (connected ?OBJ1 ?OBJ2)))
            (holdsDuring
                  (ImmediateFutureFn
                        (WhenFn ?ATTACH))
                  (connected ?OBJ1 ?OBJ2))))

If detach 是脫離的實例 and obj1 是 detach 的受事者 and obj2 是 detach 的受事者, then obj1 與 obj2 相連 ""detach 存在的時間" 不久之前"a(之中) "detach 存在的時間" 不久之前 and obj1 與 obj2 相連 ""detach 存在的時間" 不久之後"a(之中) "detach 存在的時間" 不久之後.

(=>
      (and
            (instance ?DETACH Detaching)
            (patient ?DETACH ?OBJ1)
            (patient ?DETACH ?OBJ2))
      (and
            (holdsDuring
                  (ImmediatePastFn
                        (WhenFn ?DETACH))
                  (connected ?OBJ1 ?OBJ2))
            (holdsDuring
                  (ImmediateFutureFn
                        (WhenFn ?DETACH))
                  (not
                        (connected ?OBJ1 ?OBJ2)))))

proc 是化學歷程的實例
stuff 對 proc 是資源 or stuff 是 proc 的結果

, then stuff 是純物質的實例.

(=>
      (and
            (instance ?PROC ChemicalProcess)
            (or
                  (resource ?PROC ?STUFF)
                  (result ?PROC ?STUFF)))
      (instance ?STUFF PureSubstance))

If substance1 對 proc 是資源 and substance2 是 proc 的結果 and substance1 是基本物質的實例 and substance2 是化合物的實例, then proc 是化學合成的實例.

(=>
      (and
            (resource ?PROC ?SUBSTANCE1)
            (result ?PROC ?SUBSTANCE2)
            (instance ?SUBSTANCE1 ElementalSubstance)
            (instance ?SUBSTANCE2 CompoundSubstance))
      (instance ?PROC ChemicalSynthesis))

If substance1 對 proc 是資源 and substance2 是 proc 的結果 and substance1 是化合物的實例 and substance2 是基本物質的實例, then proc 是化學分解的實例.

(=>
      (and
            (resource ?PROC ?SUBSTANCE1)
            (result ?PROC ?SUBSTANCE2)
            (instance ?SUBSTANCE1 CompoundSubstance)
            (instance ?SUBSTANCE2 ElementalSubstance))
      (instance ?PROC ChemicalDecomposition))

If combustion 是燃燒的實例, then there exist 加溫 heat,光線 light so that heat 是 combustion 的次歷�{ and light 是 combustion 的次歷�{.

(=>
      (instance ?COMBUSTION Combustion)
      (exists
            (?HEAT ?LIGHT)
            (and
                  (instance ?HEAT Heating)
                  (instance ?LIGHT RadiatingLight)
                  (subProcess ?HEAT ?COMBUSTION)
                  (subProcess ?LIGHT ?COMBUSTION))))

If change 是內在改變的實例 and obj 是 change 的受事者, then there exists property so that

property 是 obj 的屬性 ""change 存在的時間" 不久之前"a(之中) "change 存在的時間" 不久之前 and property 是 obj 的屬性 ""change 存在的時間" 不久之後"a(之中) "change 存在的時間" 不久之後
property 是 obj 的屬性 ""change 存在的時間" 不久之前"a(之中) "change 存在的時間" 不久之前 and property 是 obj 的屬性 ""change 存在的時間" 不久之後"a(之中) "change 存在的時間" 不久之後

(=>
      (and
            (instance ?CHANGE InternalChange)
            (patient ?CHANGE ?OBJ))
      (exists
            (?PROPERTY)
            (or
                  (and
                        (holdsDuring
                              (ImmediatePastFn
                                    (WhenFn ?CHANGE))
                              (attribute ?OBJ ?PROPERTY))
                        (holdsDuring
                              (ImmediateFutureFn
                                    (WhenFn ?CHANGE))
                              (not
                                    (attribute ?OBJ ?PROPERTY))))
                  (and
                        (holdsDuring
                              (ImmediatePastFn
                                    (WhenFn ?CHANGE))
                              (not
                                    (attribute ?OBJ ?PROPERTY)))
                        (holdsDuring
                              (ImmediateFutureFn
                                    (WhenFn ?CHANGE))
                              (attribute ?OBJ ?PROPERTY))))))

If alt 是表面改變的實例 and obj 是 alt 的受事者, then there exist part,property so that part 是 obj的 �~表部分 and property 是 part 的屬性 ""alt 存在的時間" 不久之前"a(之中) "alt 存在的時間" 不久之前 and property 是 part 的屬性 ""alt 存在的時間" 不久之後"a(之中) "alt 存在的時間" 不久之後.

(=>
      (and
            (instance ?ALT SurfaceChange)
            (patient ?ALT ?OBJ))
      (exists
            (?PART ?PROPERTY)
            (and
                  (superficialPart ?PART ?OBJ)
                  (holdsDuring
                        (ImmediatePastFn
                              (WhenFn ?ALT))
                        (attribute ?PART ?PROPERTY))
                  (holdsDuring
                        (ImmediateFutureFn
                              (WhenFn ?ALT))
                        (not
                              (attribute ?PART ?PROPERTY))))))

If alt 是形狀改變的實例 and obj 是 alt 的受事者, then there exists 形狀屬性 property so that

property 是 obj 的屬性 ""alt 存在的時間" 不久之前"a(之中) "alt 存在的時間" 不久之前 and property 是 obj 的屬性 ""alt 存在的時間" 不久之後"a(之中) "alt 存在的時間" 不久之後
property 是 obj 的屬性 ""alt 存在的時間" 不久之前"a(之中) "alt 存在的時間" 不久之前 and property 是 obj 的屬性 ""alt 存在的時間" 不久之後"a(之中) "alt 存在的時間" 不久之後

(=>
      (and
            (instance ?ALT ShapeChange)
            (patient ?ALT ?OBJ))
      (exists
            (?PROPERTY)
            (and
                  (instance ?PROPERTY ShapeAttribute)
                  (or
                        (and
                              (holdsDuring
                                    (ImmediatePastFn
                                          (WhenFn ?ALT))
                                    (attribute ?OBJ ?PROPERTY))
                              (holdsDuring
                                    (ImmediateFutureFn
                                          (WhenFn ?ALT))
                                    (not
                                          (attribute ?OBJ ?PROPERTY))))
                        (and
                              (holdsDuring
                                    (ImmediatePastFn
                                          (WhenFn ?ALT))
                                    (not
                                          (attribute ?OBJ ?PROPERTY)))
                              (holdsDuring
                                    (ImmediateFutureFn
                                          (WhenFn ?ALT))
                                    (attribute ?OBJ ?PROPERTY)))))))

If coloring 是著色的實例 and obj 是 coloring 的受事者, then there exists 顏色屬性 property so that property 是 obj 的屬性 ""coloring 存在的時間" 不久之前"a(之中) "coloring 存在的時間" 不久之前 and property 是 obj 的屬性 ""coloring 存在的時間" 不久之後"a(之中) "coloring 存在的時間" 不久之後.

(=>
      (and
            (instance ?COLORING Coloring)
            (patient ?COLORING ?OBJ))
      (exists
            (?PROPERTY)
            (and
                  (instance ?PROPERTY ColorAttribute)
                  (holdsDuring
                        (ImmediatePastFn
                              (WhenFn ?COLORING))
                        (attribute ?OBJ ?PROPERTY))
                  (holdsDuring
                        (ImmediateFutureFn
                              (WhenFn ?COLORING))
                        (not
                              (attribute ?OBJ ?PROPERTY))))))

If develop 是內容發展的實例, then there exists 內容載體 obj so that obj 是 develop 的受事者.

(=>
      (instance ?DEVELOP ContentDevelopment)
      (exists
            (?OBJ)
            (and
                  (instance ?OBJ ContentBearingObject)
                  (patient ?DEVELOP ?OBJ))))

If read 是閱讀的實例, then there exist 文本 text,prop so that text (不) �]含s) 訊息 %2 and read 表達 prop 的內容.

(=>
      (instance ?READ Reading)
      (exists
            (?TEXT ?PROP)
            (and
                  (instance ?TEXT Text)
                  (containsInformation ?TEXT ?PROP)
                  (realization ?READ ?PROP))))

If decode 是解碼的實例 and doc1 是 decode 的受事者, then there exist encode,doc2,time so that doc2 (不) �]含s) 訊息 %2 and doc1 (不) �]含s) 訊息 %2 and time 是 ""decode 存在的時間" 之前" 的部分 and encode 是編碼的實例 and doc2 是 encode 的受事者 timea(之中) time.

(=>
      (and
            (instance ?DECODE Decoding)
            (patient ?DECODE ?DOC1))
      (exists
            (?ENCODE ?DOC2 ?TIME)
            (and
                  (containsInformation ?DOC2 ?PROP)
                  (containsInformation ?DOC1 ?PROP)
                  (temporalPart
                        ?TIME
                        (PastFn
                              (WhenFn ?DECODE)))
                  (holdsDuring
                        ?TIME
                        (and
                              (instance ?ENCODE Encoding)
                              (patient ?ENCODE ?DOC2))))))

If wet 是濕潤的實例 and obj 是 wet 的受事者, then 濕的是 obj 的屬性 or 潮濕是 obj 的屬性 ""wet 存在的時間" 不久之後"a(之中) "wet 存在的時間" 不久之後.

(=>
      (and
            (instance ?WET Wetting)
            (patient ?WET ?OBJ))
      (holdsDuring
            (ImmediateFutureFn
                  (WhenFn ?WET))
            (or
                  (attribute ?OBJ Wet)
                  (attribute ?OBJ Damp))))

If wet 是濕潤的實例, then there exists obj so that 液體的是 obj 的屬性 and obj 是 wet 的受事者.

(=>
      (instance ?WET Wetting)
      (exists
            (?OBJ)
            (and
                  (attribute ?OBJ Liquid)
                  (patient ?WET ?OBJ))))

If dry 是乾燥的實例 and obj 是 dry 的受事者, then 乾的是 obj 的屬性 ""dry 存在的時間" 不久之後"a(之中) "dry 存在的時間" 不久之後.

(=>
      (and
            (instance ?DRY Drying)
            (patient ?DRY ?OBJ))
      (holdsDuring
            (ImmediateFutureFn
                  (WhenFn ?DRY))
            (attribute ?OBJ Dry)))

If action 是產生的實例, then there exists result so that result 是 action 的結果.

(=>
      (instance ?ACTION Creation)
      (exists
            (?RESULT)
            (result ?ACTION ?RESULT)))

If pub 是出版的實例 and text 是 pub 的受事者, then text 是文本的次種類.

(=>
      (and
            (instance ?PUB Publication)
            (patient ?PUB ?TEXT))
      (subclass ?TEXT Text))

If cook 是烹飪的實例, then there exists 食物 food so that food 是 cook 的結果.

(=>
      (instance ?COOK Cooking)
      (exists
            (?FOOD)
            (and
                  (instance ?FOOD Food)
                  (result ?COOK ?FOOD))))

If search 是探尋的實例 and search 是 agent 的施事者 and entity 是 search 的受事者, then agent 在 entity 範圍中.

(=>
      (and
            (instance ?SEARCH Searching)
            (agent ?SEARCH ?AGENT)
            (patient ?SEARCH ?ENTITY))
      (inScopeOfInterest ?AGENT ?ENTITY))

If pursue 是追的實例 and pursue 是 agent 的施事者 and obj 是 pursue 的受事者, then agent (不) 想要not(s) obj pursuea(之中) pursue.

(=>
      (and
            (instance ?PURSUE Pursuing)
            (agent ?PURSUE ?AGENT)
            (patient ?PURSUE ?OBJ))
      (holdsDuring
            ?PURSUE
            (wants ?AGENT ?OBJ)))

If pursue 是追的實例 and pursue 是 agent 的施事者 and obj 是 pursue 的受事者, then agent not(沒) 擁有(s) obj pursuea(之中) pursue.

(=>
      (and
            (instance ?PURSUE Pursuing)
            (agent ?PURSUE ?AGENT)
            (patient ?PURSUE ?OBJ))
      (holdsDuring
            ?PURSUE
            (not
                  (possesses ?AGENT ?OBJ))))

If investigate 是調查的實例 and prop 是 investigate 的受事者, then prop 是 SUO-KIF表述式的實例.

(=>
      (and
            (instance ?INVESTIGATE Investigating)
            (patient ?INVESTIGATE ?PROP))
      (instance ?PROP Formula))

If investigate 是調查的實例 and investigate 是 agent 的施事者 and prop 是 investigate 的受事者, then agent not(不）知道 "investigate 存在的時間"a(之中) investigate 存在的時間.

(=>
      (and
            (instance ?INVESTIGATE Investigating)
            (agent ?INVESTIGATE ?AGENT)
            (patient ?INVESTIGATE ?PROP))
      (holdsDuring
            (WhenFn ?INVESTIGATE)
            (not
                  (knows ?AGENT ?PROP))))

If proc 是診斷歷程的實例 and proc 是 agent 的施事者, then there exists cause so that proc 對agent 有意圖 "agent (不）知道s) %2".

(=>
      (and
            (instance ?PROC DiagnosticProcess)
            (agent ?PROC ?AGENT))
      (exists
            (?CAUSE)
            (hasPurposeForAgent
                  ?PROC
                  (knows
                        ?AGENT
                        (causes ?CAUSE ?PROC))
                  ?AGENT)))

If interaction 是人際互動的實例, then there exist agent1,agent2 so that interaction 是 agent1 的施事者 and interaction 是 agent2 的施事者 and agent1 等於 agent2.

(=>
      (instance ?INTERACTION SocialInteraction)
      (exists
            (?AGENT1 ?AGENT2)
            (and
                  (agent ?INTERACTION ?AGENT1)
                  (agent ?INTERACTION ?AGENT2)
                  (not
                        (equal ?AGENT1 ?AGENT2)))))

If pretend 是偽裝的實例, then there exist person,prop so that pretend 有意圖 "person (不)相信 prop" and prop &$是真的.

(=>
      (instance ?PRETEND Pretending)
      (exists
            (?PERSON ?PROP)
            (and
                  (hasPurpose
                        ?PRETEND
                        (believes ?PERSON ?PROP))
                  (true ?PROP True))))

If communicate 是溝通的實例, then there exist 內容載體 obj,具認知力施事者 agent1,具認知力施事者 agent2 so that obj 是 communicate 的受事者 and communicate 是 agent1 的施事者 and communicate (不) 終結not(s) agent2.

(=>
      (instance ?COMMUNICATE Communication)
      (exists
            (?OBJ ?AGENT1 ?AGENT2)
            (and
                  (instance ?OBJ ContentBearingObject)
                  (patient ?COMMUNICATE ?OBJ)
                  (instance ?AGENT1 CognitiveAgent)
                  (agent ?COMMUNICATE ?AGENT1)
                  (instance ?AGENT2 CognitiveAgent)
                  (destination ?COMMUNICATE ?AGENT2))))

If disseminate 是散佈的實例, then there exist 具認知力施事者 agent1,具認知力施事者 agent2 so that disseminate (不) 終結not(s) agent1 and disseminate (不) 終結not(s) agent2 and agent1 等於 agent2.

(=>
      (instance ?DISSEMINATE Disseminating)
      (exists
            (?AGENT1 ?AGENT2)
            (and
                  (destination ?DISSEMINATE ?AGENT1)
                  (instance ?AGENT1 CognitiveAgent)
                  (destination ?DISSEMINATE ?AGENT2)
                  (instance ?AGENT2 CognitiveAgent)
                  (not
                        (equal ?AGENT1 ?AGENT2)))))

If advert 是廣告的實例, then there exists obj so that advert 參照 obj and advert 有意圖 "there exists 銷售 sale so that obj 是 sale 的受事者".

(=>
      (instance ?ADVERT Advertising)
      (exists
            (?OBJ)
            (and
                  (refers ?ADVERT ?OBJ)
                  (hasPurpose
                        ?ADVERT
                        (exists
                              (?SALE)
                              (and
                                    (instance ?SALE Selling)
                                    (patient ?SALE ?OBJ)))))))

If communicate 是語言溝通的實例, then there exists 語言表式 obj so that obj 是 communicate 的受事者.

(=>
      (instance ?COMMUNICATE LinguisticCommunication)
      (exists
            (?OBJ)
            (and
                  (instance ?OBJ LinguisticExpression)
                  (patient ?COMMUNICATE ?OBJ))))

If state 是敘述的實例 and state 是 agent 的施事者 and formula 是 state 的受事者 and formula 是 SUO-KIF表述式的實例, then agent (不)相信 formula "state 存在的時間"a(之中) state 存在的時間.

(=>
      (and
            (instance ?STATE Stating)
            (agent ?STATE ?AGENT)
            (patient ?STATE ?FORMULA)
            (instance ?FORMULA Formula))
      (holdsDuring
            (WhenFn ?STATE)
            (believes ?AGENT ?FORMULA)))

If order 是命令的實例 and formula 是 order 的受事者, then 陳述 formula 有義務的型態意義.

(=>
      (and
            (instance ?ORDER Ordering)
            (patient ?ORDER ?FORMULA))
      (modalAttribute ?FORMULA Obligation))

If request 是請求的實例 and request 是 agent 的施事者 and formula 是 request 的受事者 and formula 是 SUO-KIF表述式的實例, then agent (不) 冀求not(s) formula.

(=>
      (and
            (instance ?REQUEST Requesting)
            (agent ?REQUEST ?AGENT)
            (patient ?REQUEST ?FORMULA)
            (instance ?FORMULA Formula))
      (desires ?AGENT ?FORMULA))

If question 是詢問的實例 and question 是 agent 的施事者 and formula 是 question 的受事者 and formula 是 SUO-KIF表述式的實例, then agent not(不）知道 "question 存在的時間"a(之中) question 存在的時間.

(=>
      (and
            (instance ?QUESTION Questioning)
            (agent ?QUESTION ?AGENT)
            (patient ?QUESTION ?FORMULA)
            (instance ?FORMULA Formula))
      (holdsDuring
            (WhenFn ?QUESTION)
            (not
                  (knows ?AGENT ?FORMULA))))

If commit 是承諾的實例 and formula 是 commit 的受事者 and formula 是 SUO-KIF表述式的實例, then 陳述 formula 有承諾的型態意義.

(=>
      (and
            (instance ?COMMIT Committing)
            (patient ?COMMIT ?FORMULA)
            (instance ?FORMULA Formula))
      (modalAttribute ?FORMULA Promise))

If express 是表達的實例 and express 是 agent 的施事者, then there exists 心理狀態 state so that state 是 agent 的屬性 and express 表達 state.

(=>
      (and
            (instance ?EXPRESS Expressing)
            (agent ?EXPRESS ?AGENT))
      (exists
            (?STATE)
            (and
                  (instance ?STATE StateOfMind)
                  (attribute ?AGENT ?STATE)
                  (represents ?EXPRESS ?STATE))))

If declare 是宣告的實例 and declare 是 agent1 的施事者, then there exist proc,agent2 so that declare 賦予 agent2 權力執行類型 proc 任務 or declare 賦予 agent2 義務執行類型 proc 任務.

(=>
      (and
            (instance ?DECLARE Declaring)
            (agent ?DECLARE ?AGENT1))
      (exists
            (?PROC ?AGENT2)
            (or
                  (confersRight ?PROC ?DECLARE ?AGENT2)
                  (confersObligation ?PROC ?DECLARE ?AGENT2))))

if cooperate 是合作的實例,
then there exists purp so that for all agent holds: if cooperate 是 agent 的施事者, then cooperate 對agent 有意圖 purp

(=>
      (instance ?COOPERATE Cooperation)
      (exists
            (?PURP)
            (forall
                  (?AGENT)
                  (=>
                        (agent ?COOPERATE ?AGENT)
                        (hasPurposeForAgent ?COOPERATE ?PURP ?AGENT)))))

If meet 是會面的實例 and meet 是 agent1 的施事者 and meet 是 agent2 的施事者, then agent1 對 agent2 是接近 "meet 存在的時間"a(之中) meet 存在的時間.

(=>
      (and
            (instance ?MEET Meeting)
            (agent ?MEET ?AGENT1)
            (agent ?MEET ?AGENT2))
      (holdsDuring
            (WhenFn ?MEET)
            (orientation ?AGENT1 ?AGENT2 Near)))

If meet 是會面的實例, then there exist agent1,agent2 so that meet 是 agent1 的施事者 and meet 是 agent2 的施事者 and meet 有意圖 "there exists 溝通 comm so that comm 是 agent1 的施事者 and comm 是 agent2 的施事者".

(=>
      (instance ?MEET Meeting)
      (exists
            (?AGENT1 ?AGENT2)
            (and
                  (agent ?MEET ?AGENT1)
                  (agent ?MEET ?AGENT2)
                  (hasPurpose
                        ?MEET
                        (exists
                              (?COMM)
                              (and
                                    (instance ?COMM Communication)
                                    (agent ?COMM ?AGENT1)
                                    (agent ?COMM ?AGENT2)))))))

If contest 是競爭的實例, then there exist agent1,agent2,purp1,purp2 so that contest 是 agent1 的施事者 and contest 是 agent2 的施事者 and contest 對agent1 有意圖 purp1 and contest 對agent2 有意圖 purp2 and agent1 等於 agent2 and purp1 等於 purp2.

(=>
      (instance ?CONTEST Contest)
      (exists
            (?AGENT1 ?AGENT2 ?PURP1 ?PURP2)
            (and
                  (agent ?CONTEST ?AGENT1)
                  (agent ?CONTEST ?AGENT2)
                  (hasPurposeForAgent ?CONTEST ?PURP1 ?AGENT1)
                  (hasPurposeForAgent ?CONTEST ?PURP2 ?AGENT2)
                  (not
                        (equal ?AGENT1 ?AGENT2))
                  (not
                        (equal ?PURP1 ?PURP2)))))

If war 是戰爭的實例, then there exists 戰役 battle so that battle 是 war 的次歷�{.

(=>
      (instance ?WAR War)
      (exists
            (?BATTLE)
            (and
                  (instance ?BATTLE Battle)
                  (subProcess ?BATTLE ?WAR))))

if war 是戰爭的實例 and war 是 agent 的施事者,
then
- agent 是國家的實例
- - agent 是組織的實例
  - for all member holds: if member 是 agent的成員, then member 是國家的實例

(=>
      (and
            (instance ?WAR War)
            (agent ?WAR ?AGENT))
      (or
            (instance ?AGENT Nation)
            (and
                  (instance ?AGENT Organization)
                  (forall
                        (?MEMBER)
                        (=>
                              (member ?MEMBER ?AGENT)
                              (instance ?MEMBER Nation))))))

If battle 是戰役的實例, then there exists 戰爭 war so that battle 是 war 的次歷�{.

(=>
      (instance ?BATTLE Battle)
      (exists
            (?WAR)
            (and
                  (instance ?WAR War)
                  (subProcess ?BATTLE ?WAR))))

If battle 是戰役的實例, then there exists 暴力性的競爭 attack so that attack 是 battle 的次歷�{.

(=>
      (instance ?BATTLE Battle)
      (exists
            (?ATTACK)
            (and
                  (instance ?ATTACK ViolentContest)
                  (subProcess ?ATTACK ?BATTLE))))

If move 是調遣的實例, then there exists 競爭 contest so that move 是 contest 的次歷�{.

(=>
      (instance ?MOVE Maneuver)
      (exists
            (?CONTEST)
            (and
                  (instance ?CONTEST Contest)
                  (subProcess ?MOVE ?CONTEST))))

If percept 是知覺的實例 and percept 是 agent 的施事者, then agent 是動物的實例.

(=>
      (and
            (instance ?PERCEPT Perception)
            (agent ?PERCEPT ?AGENT))
      (instance ?AGENT Animal))

If percept 是知覺的實例 and percept 是 agent 的施事者 and object 是 percept 的受事者, then agent (沒) �`意到not(s) object.

(=>
      (and
            (instance ?PERCEPT Perception)
            (agent ?PERCEPT ?AGENT)
            (patient ?PERCEPT ?OBJECT))
      (notices ?AGENT ?OBJECT))

If agent 是能知覺的行為主體的實例, then agent 可以任角色經驗者做知覺.

(=>
      (instance ?AGENT SentientAgent)
      (capability Perception experiencer ?AGENT))

If see 是看的實例 and see 是 agent 的施事者 and obj 是 see 的受事者, then

被光照的是 obj 的屬性
there exists 顏色屬性 prop so that agent (不）知道s) %2

(=>
      (and
            (instance ?SEE Seeing)
            (agent ?SEE ?AGENT)
            (patient ?SEE ?OBJ))
      (and
            (attribute ?OBJ Illuminated)
            (exists
                  (?PROP)
                  (and
                        (instance ?PROP ColorAttribute)
                        (knows
                              ?AGENT
                              (attribute ?OBJ ?PROP))))))

If smell 是聞的實例 and obj 是 smell 的受事者, then there exists 嗅覺屬性 attr so that attr 是 obj 的屬性.

(=>
      (and
            (instance ?SMELL Smelling)
            (patient ?SMELL ?OBJ))
      (exists
            (?ATTR)
            (and
                  (instance ?ATTR OlfactoryAttribute)
                  (attribute ?OBJ ?ATTR))))

If taste 是味覺的實例 and obj 是 taste 的受事者, then there exists 味覺屬性 attr so that attr 是 obj 的屬性.

(=>
      (and
            (instance ?TASTE Tasting)
            (patient ?TASTE ?OBJ))
      (exists
            (?ATTR)
            (and
                  (instance ?ATTR TasteAttribute)
                  (attribute ?OBJ ?ATTR))))

If hear 是聽的實例 and obj 是 hear 的受事者, then there exists 聲音屬性 attr so that attr 是 obj 的屬性.

(=>
      (and
            (instance ?HEAR Hearing)
            (patient ?HEAR ?OBJ))
      (exists
            (?ATTR)
            (and
                  (instance ?ATTR SoundAttribute)
                  (attribute ?OBJ ?ATTR))))

If tactile 是觸覺的實例, then there exists 觸動 touch so that touch 是 tactile 的次歷�{.

(=>
      (instance ?TACTILE TactilePerception)
      (exists
            (?TOUCH)
            (and
                  (instance ?TOUCH Touching)
                  (subProcess ?TOUCH ?TACTILE))))

If emit 是聲音的實例 and emit 是 sound 的施事者, then there exists 聲音屬性 attr so that attr 是 sound 的屬性.

(=>
      (and
            (instance ?EMIT RadiatingSound)
            (agent ?EMIT ?SOUND))
      (exists
            (?ATTR)
            (and
                  (instance ?ATTR SoundAttribute)
                  (attribute ?SOUND ?ATTR))))

If process 是狀態改變的實例 and obj 是 process 的受事者, then there exist part,物理狀態 state1,物理狀態 state2 so that part 是 obj 的部分) and state1 等於 state2 and state1 是 part 的屬性 ""process 存在的時間" 不久之前"a(之中) "process 存在的時間" 不久之前 and state2 是 part 的屬性 ""freeze 存在的時間" 不久之後"a(之中) "freeze 存在的時間" 不久之後.

(=>
      (and
            (instance ?PROCESS StateChange)
            (patient ?PROCESS ?OBJ))
      (exists
            (?PART ?STATE1 ?STATE2)
            (and
                  (part ?PART ?OBJ)
                  (instance ?STATE1 PhysicalState)
                  (instance ?STATE2 PhysicalState)
                  (not
                        (equal ?STATE1 ?STATE2))
                  (holdsDuring
                        (ImmediatePastFn
                              (WhenFn ?PROCESS))
                        (attribute ?PART ?STATE1))
                  (holdsDuring
                        (ImmediateFutureFn
                              (WhenFn ?FREEZE))
                        (attribute ?PART ?STATE2)))))

If melt 是熔化的實例, then there exists 加溫 heat so that heat 是 melt 的次歷�{.

(=>
      (instance ?MELT Melting)
      (exists
            (?HEAT)
            (and
                  (instance ?HEAT Heating)
                  (subProcess ?HEAT ?MELT))))

If melt 是熔化的實例 and obj 是 melt 的受事者, then there exists part so that part 是 obj 的部分) and 固體的是 part 的屬性 ""melt 存在的時間" 不久之前"a(之中) "melt 存在的時間" 不久之前 and 液體的是 part 的屬性 ""melt 存在的時間" 不久之後"a(之中) "melt 存在的時間" 不久之後.

(=>
      (and
            (instance ?MELT Melting)
            (patient ?MELT ?OBJ))
      (exists
            (?PART)
            (and
                  (part ?PART ?OBJ)
                  (holdsDuring
                        (ImmediatePastFn
                              (WhenFn ?MELT))
                        (attribute ?PART Solid))
                  (holdsDuring
                        (ImmediateFutureFn
                              (WhenFn ?MELT))
                        (attribute ?PART Liquid)))))

If boil 是沸騰的實例, then there exists 加溫 heat so that heat 是 boil 的次歷�{.

(=>
      (instance ?BOIL Boiling)
      (exists
            (?HEAT)
            (and
                  (instance ?HEAT Heating)
                  (subProcess ?HEAT ?BOIL))))

If boil 是沸騰的實例 and obj 是 boil 的受事者, then there exists part so that part 是 obj 的部分) and 液體的是 part 的屬性 ""boil 存在的時間" 不久之前"a(之中) "boil 存在的時間" 不久之前 and 氣體是 part 的屬性 ""boil 存在的時間" 不久之後"a(之中) "boil 存在的時間" 不久之後.

(=>
      (and
            (instance ?BOIL Boiling)
            (patient ?BOIL ?OBJ))
      (exists
            (?PART)
            (and
                  (part ?PART ?OBJ)
                  (holdsDuring
                        (ImmediatePastFn
                              (WhenFn ?BOIL))
                        (attribute ?PART Liquid))
                  (holdsDuring
                        (ImmediateFutureFn
                              (WhenFn ?BOIL))
                        (attribute ?PART Gas)))))

If cond 是凝結的實例, then there exists 降溫 cool so that cool 是 cond 的次歷�{.

(=>
      (instance ?COND Condensing)
      (exists
            (?COOL)
            (and
                  (instance ?COOL Cooling)
                  (subProcess ?COOL ?COND))))

If cond 是凝結的實例 and obj 是 cond 的受事者, then there exists part so that part 是 obj 的部分) and 氣體是 part 的屬性 ""cond 存在的時間" 不久之前"a(之中) "cond 存在的時間" 不久之前 and 液體的是 part 的屬性 ""cond 存在的時間" 不久之後"a(之中) "cond 存在的時間" 不久之後.

(=>
      (and
            (instance ?COND Condensing)
            (patient ?COND ?OBJ))
      (exists
            (?PART)
            (and
                  (part ?PART ?OBJ)
                  (holdsDuring
                        (ImmediatePastFn
                              (WhenFn ?COND))
                        (attribute ?PART Gas))
                  (holdsDuring
                        (ImmediateFutureFn
                              (WhenFn ?COND))
                        (attribute ?PART Liquid)))))

If freeze 是凝固的實例, then there exists 降溫 cool so that cool 是 freeze 的次歷�{.

(=>
      (instance ?FREEZE Freezing)
      (exists
            (?COOL)
            (and
                  (instance ?COOL Cooling)
                  (subProcess ?COOL ?FREEZE))))

If freeze 是凝固的實例 and obj 是 freeze 的受事者, then there exists part so that part 是 obj 的部分) and 液體的是 part 的屬性 ""freeze 存在的時間" 不久之前"a(之中) "freeze 存在的時間" 不久之前 and 固體的是 part 的屬性 ""freeze 存在的時間" 不久之後"a(之中) "freeze 存在的時間" 不久之後.

(=>
      (and
            (instance ?FREEZE Freezing)
            (patient ?FREEZE ?OBJ))
      (exists
            (?PART)
            (and
                  (part ?PART ?OBJ)
                  (holdsDuring
                        (ImmediatePastFn
                              (WhenFn ?FREEZE))
                        (attribute ?PART Liquid))
                  (holdsDuring
                        (ImmediateFutureFn
                              (WhenFn ?FREEZE))
                        (attribute ?PART Solid)))))

If area 是水域的實例, then there exist bed,hole,水 water so that "洞 hole 的主體" 等於 bed and water (沒) 適當填充s hole and "bed 和 water 的聯集" 等於 area.

(=>
      (instance ?AREA WaterArea)
      (exists
            (?BED ?HOLE ?WATER)
            (and
                  (equal
                        (PrincipalHostFn ?HOLE)
                        ?BED)
                  (instance ?WATER Water)
                  (properlyFills ?WATER ?HOLE)
                  (equal
                        (MereologicalSumFn ?BED ?WATER)
                        ?AREA))))

If land1 是陸地的實例, then there exists land2 so that land1 是 land2 的部分) and land2 是大陸的實例 or land2 是島嶼的實例.

(=>
      (instance ?LAND1 LandArea)
      (exists
            (?LAND2)
            (and
                  (part ?LAND1 ?LAND2)
                  (or
                        (instance ?LAND2 Continent)
                        (instance ?LAND2 Island)))))

If island 是島嶼的實例, then there don't exist 陸地 area,part1,part2 so that part1 是 island 的部分) and part2 是 area 的部分) and island 是 area 的部分) and area 是 island 的部分) and part1 與 part2 相連.

(=>
      (instance ?ISLAND Island)
      (not
            (exists
                  (?AREA ?PART1 ?PART2)
                  (and
                        (instance ?AREA LandArea)
                        (part ?PART1 ?ISLAND)
                        (part ?PART2 ?AREA)
                        (not
                              (part ?ISLAND ?AREA))
                        (not
                              (part ?AREA ?ISLAND))
                        (connected ?PART1 ?PART2)))))

If state 是州或省的實例, then there exists 國家 land so that state 是 land 的正部分.

(=>
      (instance ?STATE StateOrProvince)
      (exists
            (?LAND)
            (and
                  (instance ?LAND Nation)
                  (properPart ?STATE ?LAND))))

If obj 的發展形式是 attr1 time1a(之中) time1 and attr2 是 attr1 的封閉續接屬性, then there exists time2 so that time2 (沒) 比 time1 較早發生not(s) and obj 的發展形式是 attr2 time2a(之中) time2.

(=>
      (and
            (holdsDuring
                  ?TIME1
                  (developmentalForm ?OBJ ?ATTR1))
            (successorAttributeClosure ?ATTR2 ?ATTR1))
      (exists
            (?TIME2)
            (and
                  (earlier ?TIME2 ?TIME1)
                  (holdsDuring
                        ?TIME2
                        (developmentalForm ?OBJ ?ATTR2)))))

If organism 是生物體的實例, then there exists 誕生 birth so that organism (沒) 體驗not(s) birth.

(=>
      (instance ?ORGANISM Organism)
      (exists
            (?BIRTH)
            (and
                  (instance ?BIRTH Birth)
                  (experiencer ?BIRTH ?ORGANISM))))

If organism 住s 在 obj, then there exists time so that organism 位於 obj timea(之中) time.

(=>
      (inhabits ?ORGANISM ?OBJ)
      (exists
            (?TIME)
            (holdsDuring
                  ?TIME
                  (located ?ORGANISM ?OBJ))))

If parent 是 child 的雙親, then ""parent 存在的時間" 的 �}始" (沒) 發生?{s} 在 ""child 存在的時間" 的 �}始" 之前.

(=>
      (parent ?CHILD ?PARENT)
      (before
            (BeginFn
                  (WhenFn ?PARENT))
            (BeginFn
                  (WhenFn ?CHILD))))

If parent 是 child 的雙親 and class 是生物體的次種類 and parent 是 class 的實例, then child 是 class 的實例.

(=>
      (and
            (parent ?CHILD ?PARENT)
            (subclass ?CLASS Organism)
            (instance ?PARENT ?CLASS))
      (instance ?CHILD ?CLASS))

If parent 是 child 的雙親, then parent 是 child 的母親 or parent 是 child 的父親.

(=>
      (parent ?CHILD ?PARENT)
      (or
            (mother ?CHILD ?PARENT)
            (father ?CHILD ?PARENT)))

If organism 是生物體的實例, then there exists parent so that parent 是 organism 的雙親.

(=>
      (instance ?ORGANISM Organism)
      (exists
            (?PARENT)
            (parent ?ORGANISM ?PARENT)))

If mother 是 child 的母親, then 雌性是 mother 的屬性.

(=>
      (mother ?CHILD ?MOTHER)
      (attribute ?MOTHER Female))

If father 是 child 的父親, then 雄性是 father 的屬性.

(=>
      (father ?CHILD ?FATHER)
      (attribute ?FATHER Male))

If alga 是藻類的實例, then there exists 水 water so that alga 住s 在 water.

(=>
      (instance ?ALGA Alga)
      (exists
            (?WATER)
            (and
                  (inhabits ?ALGA ?WATER)
                  (instance ?WATER Water))))

If fungus 是真菌的實例 and fungus 住s 在 obj, then obj 是生物體的實例.

(=>
      (and
            (instance ?FUNGUS Fungus)
            (inhabits ?FUNGUS ?OBJ))
      (instance ?OBJ Organism))

if bacterium 是細菌的實例,
then there exists 細胞 cell1 so that cell1 是 bacterium 的元件 and for all cell2 holds: if cell2 是 bacterium 的元件 and cell2 是細胞的實例, then cell1 等於 cell2

(=>
      (instance ?BACTERIUM Bacterium)
      (exists
            (?CELL1)
            (and
                  (component ?CELL1 ?BACTERIUM)
                  (instance ?CELL1 Cell)
                  (forall
                        (?CELL2)
                        (=>
                              (and
                                    (component ?CELL2 ?BACTERIUM)
                                    (instance ?CELL2 Cell))
                              (equal ?CELL1 ?CELL2))))))

If bacterium 是細菌的實例 and bacterium 住s 在 obj, then obj 是生物體的實例.

(=>
      (and
            (instance ?BACTERIUM Bacterium)
            (inhabits ?BACTERIUM ?OBJ))
      (instance ?OBJ Organism))

if virus 是病毒的實例,
then there exists 分子 mol1 so that mol1 是 virus 的元件 and for all mol2 holds: if mol2 是 virus 的元件 and mol2 是分子的實例, then mol1 等於 mol2

(=>
      (instance ?VIRUS Virus)
      (exists
            (?MOL1)
            (and
                  (component ?MOL1 ?VIRUS)
                  (instance ?MOL1 Molecule)
                  (forall
                        (?MOL2)
                        (=>
                              (and
                                    (component ?MOL2 ?VIRUS)
                                    (instance ?MOL2 Molecule))
                              (equal ?MOL1 ?MOL2))))))

If virus 是病毒的實例 and virus 住s 在 obj, then obj 是生物體的實例.

(=>
      (and
            (instance ?VIRUS Virus)
            (inhabits ?VIRUS ?OBJ))
      (instance ?OBJ Organism))

If virus 是病毒的實例 and proc 是複製的實例 and proc 是 virus 的施事者, then there exists 細胞 cell so that proc 位於 cell.

(=>
      (and
            (instance ?VIRUS Virus)
            (instance ?PROC Replication)
            (agent ?PROC ?VIRUS))
      (exists
            (?CELL)
            (and
                  (located ?PROC ?CELL)
                  (instance ?CELL Cell))))

If fish 是魚類的實例, then there exists 水 water so that fish 住s 在 water.

(=>
      (instance ?FISH Fish)
      (exists
            (?WATER)
            (and
                  (inhabits ?FISH ?WATER)
                  (instance ?WATER Water))))

If organism 是毒性生物的實例, then there exists 活性生物物質 substance so that substance 是 organism 的部分).

(=>
      (instance ?ORGANISM ToxicOrganism)
      (exists
            (?SUBSTANCE)
            (and
                  (instance ?SUBSTANCE BiologicallyActiveSubstance)
                  (part ?SUBSTANCE ?ORGANISM))))

If food 是食物的實例, then there exists 養份 nutrient so that nutrient 是 food 的部分).

(=>
      (instance ?FOOD Food)
      (exists
            (?NUTRIENT)
            (and
                  (instance ?NUTRIENT Nutrient)
                  (part ?NUTRIENT ?FOOD))))

if food 是食物的實例,
then for all part1 holds: if part1 是 food 的部分), then there exist part2,動物 animal so that part1 是 part2 的部分) and part2 是 animal 的部分)

(=>
      (instance ?FOOD Food)
      (forall
            (?PART1)
            (=>
                  (part ?PART1 ?FOOD)
                  (exists
                        (?PART2 ?ANIMAL)
                        (and
                              (part ?PART1 ?PART2)
                              (part ?PART2 ?ANIMAL)
                              (instance ?ANIMAL Animal))))))

if meat 是肉的實例,
then for all part holds: if part 是 meat 的部分), then there exist subpart,time,animal so that subpart 是 part 的部分) and animal 是動物的實例 and subpart 是 animal 的部分) timea(之中) time

(=>
      (instance ?MEAT Meat)
      (forall
            (?PART)
            (=>
                  (part ?PART ?MEAT)
                  (exists
                        (?SUBPART ?TIME ?ANIMAL)
                        (and
                              (part ?SUBPART ?PART)
                              (holdsDuring
                                    ?TIME
                                    (and
                                          (instance ?ANIMAL Animal)
                                          (part ?SUBPART ?ANIMAL))))))))

if veg 是蔬果的實例,
then for all part holds: if part 是 veg 的部分), then there exist subpart,time,plant so that subpart 是 part 的部分) and plant 是植物的實例 and subpart 是 plant 的部分) timea(之中) time

(=>
      (instance ?VEG FruitOrVegetable)
      (forall
            (?PART)
            (=>
                  (part ?PART ?VEG)
                  (exists
                        (?SUBPART ?TIME ?PLANT)
                        (and
                              (part ?SUBPART ?PART)
                              (holdsDuring
                                    ?TIME
                                    (and
                                          (instance ?PLANT Plant)
                                          (part ?SUBPART ?PLANT))))))))

If bev 是飲料的實例, then 液體的是 bev 的屬性.

(=>
      (instance ?BEV Beverage)
      (attribute ?BEV Liquid))

If drink 是喝的實例 and bev 是 drink 的受事者, then bev 是飲料的實例.

(=>
      (and
            (instance ?DRINK Drinking)
            (patient ?DRINK ?BEV))
      (instance ?BEV Beverage))

If anat 是解剖構造的實例, then there exists 生物體 organism so that anat 是 organism 的部分).

(=>
      (instance ?ANAT AnatomicalStructure)
      (exists
            (?ORGANISM)
            (and
                  (instance ?ORGANISM Organism)
                  (part ?ANAT ?ORGANISM))))

If part 是解剖構造的實例, then there exists 細胞 cell so that cell 是 part 的部分).

(=>
      (instance ?PART AnatomicalStructure)
      (exists
            (?CELL)
            (and
                  (instance ?CELL Cell)
                  (part ?CELL ?PART))))

If part 是軀體部件的實例, then there doesn't exist 病理歷程 proc so that part 是 proc 的結果.

(=>
      (instance ?PART BodyPart)
      (not
            (exists
                  (?PROC)
                  (and
                        (instance ?PROC PathologicProcess)
                        (result ?PROC ?PART)))))

If cover 是軀體表面（覆蓋物）的實例, then there exists body so that cover 是 body的 �~表部分 and body 是生物體的實例 or body 是軀體部件的實例.

(=>
      (instance ?COVER BodyCovering)
      (exists
            (?BODY)
            (and
                  (superficialPart ?COVER ?BODY)
                  (or
                        (instance ?BODY Organism)
                        (instance ?BODY BodyPart)))))

If junct 是軀體接點的實例, then there exists 軀體部件 struct so that junct 是 struct 的元件.

(=>
      (instance ?JUNCT BodyJunction)
      (exists
            (?STRUCT)
            (and
                  (instance ?STRUCT BodyPart)
                  (component ?JUNCT ?STRUCT))))

If junct 是軀體接點的實例, then there exist 軀體部件 struct1,軀體部件 struct2 so that junct 與 struct1 相連 and junct 與 struct2 相連 and struct1 等於 struct2.

(=>
      (instance ?JUNCT BodyJunction)
      (exists
            (?STRUCT1 ?STRUCT2)
            (and
                  (connected ?JUNCT ?STRUCT1)
                  (connected ?JUNCT ?STRUCT2)
                  (instance ?STRUCT1 BodyPart)
                  (instance ?STRUCT2 BodyPart)
                  (not
                        (equal ?STRUCT1 ?STRUCT2)))))

If organ 是器官的實例, then there exists purp so that organ 有意圖 purp.

(=>
      (instance ?ORGAN Organ)
      (exists
            (?PURP)
            (hasPurpose ?ORGAN ?PURP)))

If stuff 是組織的實例, then there exists 細胞 part so that part 是 stuff 的部分).

(=>
      (instance ?STUFF Tissue)
      (exists
            (?PART)
            (and
                  (instance ?PART Cell)
                  (part ?PART ?STUFF))))

If stuff 是組織的實例, then there exists 生物體 organism so that stuff 是 organism 的部分).

(=>
      (instance ?STUFF Tissue)
      (exists
            (?ORGANISM)
            (and
                  (instance ?ORGANISM Organism)
                  (part ?STUFF ?ORGANISM))))

If bone 是骨骼的實例, then there exists 脊椎動物 vert so that bone 是 vert 的部分).

(=>
      (instance ?BONE Bone)
      (exists
            (?VERT)
            (and
                  (instance ?VERT Vertebrate)
                  (part ?BONE ?VERT))))

If morph 是詞素的實例, then there doesn't exist 詞素 othermorph so that othermorph 是 morph 的部分) and othermorph 等於 morph.

(=>
      (instance ?MORPH Morpheme)
      (not
            (exists
                  (?OTHERMORPH)
                  (and
                        (instance ?OTHERMORPH Morpheme)
                        (part ?OTHERMORPH ?MORPH)
                        (not
                              (equal ?OTHERMORPH ?MORPH))))))

If morph 是詞素的實例, then there exists 詞 word so that morph 是 word 的部分).

(=>
      (instance ?MORPH Morpheme)
      (exists
            (?WORD)
            (and
                  (instance ?WORD Word)
                  (part ?MORPH ?WORD))))

If word 是詞的實例, then there exists 詞素 part so that part 是 word 的部分).

(=>
      (instance ?WORD Word)
      (exists
            (?PART)
            (and
                  (part ?PART ?WORD)
                  (instance ?PART Morpheme))))

If phrase 是詞組的實例, then there exist 詞 part1,詞 part2 so that part1 是 phrase 的部分) and part2 是 phrase 的部分) and part1 等於 part2.

(=>
      (instance ?PHRASE Phrase)
      (exists
            (?PART1 ?PART2)
            (and
                  (part ?PART1 ?PHRASE)
                  (part ?PART2 ?PHRASE)
                  (instance ?PART1 Word)
                  (instance ?PART2 Word)
                  (not
                        (equal ?PART1 ?PART2)))))

If sentence 是句子的實例, then there exist 名詞詞組 phrase1,動詞詞組 phrase2 so that phrase1 是 sentence 的部分) and phrase2 是 sentence 的部分).

(=>
      (instance ?SENTENCE Sentence)
      (exists
            (?PHRASE1 ?PHRASE2)
            (and
                  (instance ?PHRASE1 NounPhrase)
                  (instance ?PHRASE2 VerbPhrase)
                  (part ?PHRASE1 ?SENTENCE)
                  (part ?PHRASE2 ?SENTENCE))))

If text 是文本的實例, then there exists 命題 prop so that text (不) �]含s) 訊息 %2.

(=>
      (instance ?TEXT Text)
      (exists
            (?PROP)
            (and
                  (instance ?PROP Proposition)
                  (containsInformation ?TEXT ?PROP))))

If text 是文本的實例, then there exists 句子 part so that part 是 text 的部分).

(=>
      (instance ?TEXT Text)
      (exists
            (?PART)
            (and
                  (part ?PART ?TEXT)
                  (instance ?PART Sentence))))

If text 是文本的實例, then there exists 寫作 write so that text 是 write 的結果.

(=>
      (instance ?TEXT Text)
      (exists
            (?WRITE)
            (and
                  (instance ?WRITE Writing)
                  (result ?WRITE ?TEXT))))

If sent 是句子的實例, then there exist 名詞詞組 noun,動詞詞組 verb so that noun 是 sent 的部分) and verb 是 sent 的部分).

(=>
      (instance ?SENT Sentence)
      (exists
            (?NOUN ?VERB)
            (and
                  (instance ?NOUN NounPhrase)
                  (instance ?VERB VerbPhrase)
                  (part ?NOUN ?SENT)
                  (part ?VERB ?SENT))))

If 作者(agent,text) holds, then there exist process,text instance so that process 是 agent 的施事者 and text 是 process 的結果.

(=>
      (authors ?AGENT ?TEXT)
      (exists
            (?PROCESS ?INSTANCE)
            (and
                  (agent ?PROCESS ?AGENT)
                  (instance ?INSTANCE ?TEXT)
                  (result ?PROCESS ?TEXT))))

If "text 的版本 int1 " 等於 edition1 and "text 的版本 int2 " 等於 edition2 and int2 (不) 大於 int1 and pub1 是出版的實例 and pub2 是出版的實例 and edition1 是 pub1 的受事者 and edition2 是 pub2 的受事者 and pub1 的日期是 date1 and pub2 的日期是 date2, then "date1 的結束" (沒) 發生?{s} 在 "date2 的結束" 之前.

(=>
      (and
            (equal
                  (EditionFn ?TEXT ?INT1)
                  ?EDITION1)
            (equal
                  (EditionFn ?TEXT ?INT2)
                  ?EDITION2)
            (greaterThan ?INT2 ?INT1)
            (instance ?PUB1 Publication)
            (instance ?PUB2 Publication)
            (patient ?PUB1 ?EDITION1)
            (patient ?PUB2 ?EDITION2)
            (date ?PUB1 ?DATE1)
            (date ?PUB2 ?DATE2))
      (before
            (EndFn ?DATE1)
            (EndFn ?DATE2)))

If "text1 的版本 number " 等於 text2, then text1 �]容 text2.

(=>
      (equal
            (EditionFn ?TEXT1 ?NUMBER)
            ?TEXT2)
      (subsumesContentClass ?TEXT1 ?TEXT2))

If text 是期刊的次種類 and "冊 int1 在系列數 text" 等於 volume1 and "冊 int2 在系列數 text" 等於 volume2 and int2 (不) 大於 int1 and pub1 是出版的實例 and pub2 是出版的實例 and volume1 是 pub1 的受事者 and volume2 是 pub2 的受事者 and pub1 的日期是 date1 and pub2 的日期是 date2, then "date1 的結束" (沒) 發生?{s} 在 "date2 的結束" 之前.

(=>
      (and
            (subclass ?TEXT Periodical)
            (equal
                  (SeriesVolumeFn ?TEXT ?INT1)
                  ?VOLUME1)
            (equal
                  (SeriesVolumeFn ?TEXT ?INT2)
                  ?VOLUME2)
            (greaterThan ?INT2 ?INT1)
            (instance ?PUB1 Publication)
            (instance ?PUB2 Publication)
            (patient ?PUB1 ?VOLUME1)
            (patient ?PUB2 ?VOLUME2)
            (date ?PUB1 ?DATE1)
            (date ?PUB2 ?DATE2))
      (before
            (EndFn ?DATE1)
            (EndFn ?DATE2)))

If "冊 number 在系列數 series" 等於 volume, then series �]容 volume.

(=>
      (equal
            (SeriesVolumeFn ?SERIES ?NUMBER)
            ?VOLUME)
      (subsumesContentClass ?SERIES ?VOLUME))

If "periodical 的期刊數 number" 等於 issue, then periodical �]容 issue.

(=>
      (equal
            (PeriodicalIssueFn ?PERIODICAL ?NUMBER)
            ?ISSUE)
      (subsumesContentClass ?PERIODICAL ?ISSUE))

If text 是摘要的實例, then there exists 文本 text2 so that text2 �]容 text.

(=>
      (instance ?TEXT Summary)
      (exists
            (?TEXT2)
            (and
                  (instance ?TEXT2 Text)
                  (subsumesContentInstance ?TEXT2 ?TEXT))))

If series 是系列刊物的實例, then there exist 書籍 book1,書籍 book2 so that series �]容 book1 and series �]容 book2 and book1 等於 book2.

(=>
      (instance ?SERIES Series)
      (exists
            (?BOOK1 ?BOOK2)
            (and
                  (instance ?BOOK1 Book)
                  (instance ?BOOK2 Book)
                  (subsumesContentInstance ?SERIES ?BOOK1)
                  (subsumesContentInstance ?SERIES ?BOOK2)
                  (not
                        (equal ?BOOK1 ?BOOK2)))))

If article 是文章的實例, then there exists 書籍 book so that book �]容 article.

(=>
      (instance ?ARTICLE Article)
      (exists
            (?BOOK)
            (and
                  (instance ?BOOK Book)
                  (subsumesContentInstance ?BOOK ?ARTICLE))))

If doc 是證書的實例 and agent (沒) 擁有not(s) doc, then there exists proc so that doc 賦予 agent 權力執行類型 proc 任務 or doc 賦予 agent 義務執行類型 proc 任務.

(=>
      (and
            (instance ?DOC Certificate)
            (possesses ?AGENT ?DOC))
      (exists
            (?PROC)
            (or
                  (confersRight ?PROC ?DOC ?AGENT)
                  (confersObligation ?PROC ?DOC ?AGENT))))

If mole 是分子的實例, then there exist 原子 atom1,原子 atom2 so that atom1 是 mole 的部分) and atom2 是 mole 的部分) and atom1 等於 atom2.

(=>
      (instance ?MOLE Molecule)
      (exists
            (?ATOM1 ?ATOM2)
            (and
                  (instance ?ATOM1 Atom)
                  (instance ?ATOM2 Atom)
                  (part ?ATOM1 ?MOLE)
                  (part ?ATOM2 ?MOLE)
                  (not
                        (equal ?ATOM1 ?ATOM2)))))

If product 是產品的實例, then there exists 生產 manufacture so that product 是 manufacture 的結果.

(=>
      (instance ?PRODUCT Product)
      (exists
            (?MANUFACTURE)
            (and
                  (instance ?MANUFACTURE Manufacture)
                  (result ?MANUFACTURE ?PRODUCT))))

If artifact1 是 artifact2 的版本, then artifact1 是 artifact2 的次種類.

(=>
      (version ?ARTIFACT1 ?ARTIFACT2)
      (subclass ?ARTIFACT1 ?ARTIFACT2))

if artifact 是固定人造物的實例,
then there exists place so that for all time holds: if time (沒) 發生?{s} 在 ""artifact 存在的時間" 的結束" 或之前 and ""artifact 存在的時間" 的 �}始" (沒) 發生?{s} 在 time 或之前, then "artifact 在 time 的 time位置" 等於 place

(=>
      (instance ?ARTIFACT StationaryArtifact)
      (exists
            (?PLACE)
            (forall
                  (?TIME)
                  (=>
                        (and
                              (beforeOrEqual
                                    ?TIME
                                    (EndFn
                                          (WhenFn ?ARTIFACT)))
                              (beforeOrEqual
                                    (BeginFn
                                          (WhenFn ?ARTIFACT))
                                    ?TIME))
                        (equal
                              (WhereFn ?ARTIFACT ?TIME)
                              ?PLACE)))))

If building 是建築物的實例, then there exists 人類 human so that

human 住s 在 building
there exists act so that act 是 human 的施事者 and act 位於 building

(=>
      (instance ?BUILDING Building)
      (exists
            (?HUMAN)
            (and
                  (instance ?HUMAN Human)
                  (or
                        (inhabits ?HUMAN ?BUILDING)
                        (exists
                              (?ACT)
                              (and
                                    (agent ?ACT ?HUMAN)
                                    (located ?ACT ?BUILDING)))))))

If room 是房間的實例, then there exists 建築物 build so that room 是 build 的正部分.

(=>
      (instance ?ROOM Room)
      (exists
            (?BUILD)
            (and
                  (instance ?BUILD Building)
                  (properPart ?ROOM ?BUILD))))

If clothing 是衣物的實例, then there exists 織物 fabric so that fabric 是 clothing 的部分).

(=>
      (instance ?CLOTHING Clothing)
      (exists
            (?FABRIC)
            (and
                  (instance ?FABRIC Fabric)
                  (part ?FABRIC ?CLOTHING))))

If device 是裝置的實例, then there exists 歷程 proc so that device 可以任角色工具做 proc.

(=>
      (instance ?DEVICE Device)
      (exists
            (?PROC)
            (and
                  (subclass ?PROC Process)
                  (capability ?PROC instrument ?DEVICE))))

If device 是裝置的實例, then there exists 歷程 proc so that device 有意圖 "device 可以任角色工具做 proc".

(=>
      (instance ?DEVICE Device)
      (exists
            (?PROC)
            (and
                  (subclass ?PROC Process)
                  (hasPurpose
                        ?DEVICE
                        (capability ?PROC instrument ?DEVICE)))))

If instrument 是樂器的實例, then instrument 可以任角色工具做音樂.

(=>
      (instance ?INSTRUMENT MusicalInstrument)
      (capability Music instrument ?INSTRUMENT))

If device 是運輸工具的實例, then device 可以任角色工具做運輸.

(=>
      (instance ?DEVICE TransportationDevice)
      (capability Transportation instrument ?DEVICE))

If weapon 是武器的實例, then weapon 可以任角色工具做損害.

(=>
      (instance ?WEAPON Weapon)
      (capability Damaging instrument ?WEAPON))

If weapon 是武器的實例, then weapon 有意圖 "there exist 損害 dest,patient so that patient 是 dest 的受事者 and

patient 是固定人造物的實例
patient 是動物的實例
there exists 動物 animal so that animal 住s 在 patient

(=>
      (instance ?WEAPON Weapon)
      (hasPurpose
            ?WEAPON
            (exists
                  (?DEST ?PATIENT)
                  (and
                        (instance ?DEST Damaging)
                        (patient ?DEST ?PATIENT)
                        (or
                              (instance ?PATIENT StationaryArtifact)
                              (instance ?PATIENT Animal)
                              (exists
                                    (?ANIMAL)
                                    (and
                                          (instance ?ANIMAL Animal)
                                          (inhabits ?ANIMAL ?PATIENT))))))))

if machine 是機器的實例,
then for all proc holds: if machine 對 proc 是工具, then there exist resource,result so that resource 對 proc 是資源 and result 是 proc 的結果

(=>
      (instance ?MACHINE Machine)
      (forall
            (?PROC)
            (=>
                  (instrument ?PROC ?MACHINE)
                  (exists
                        (?RESOURCE ?RESULT)
                        (and
                              (resource ?PROC ?RESOURCE)
                              (result ?PROC ?RESULT))))))

If comp 是工程元件的實例, then there exists 裝置 device so that comp 是 device 的元件.

(=>
      (instance ?COMP EngineeringComponent)
      (exists
            (?DEVICE)
            (and
                  (instance ?DEVICE Device)
                  (component ?COMP ?DEVICE))))

If comp1 與 comp2 連結, then comp1 是 comp2 的元件 and comp2 是 comp1 的元件.

(=>
      (connectedEngineeringComponents ?COMP1 ?COMP2)
      (and
            (not
                  (engineeringSubcomponent ?COMP1 ?COMP2))
            (not
                  (engineeringSubcomponent ?COMP2 ?COMP1))))

If comp1 與 comp2 連結, then comp1 是工程連結元件的實例 and comp2 是工程連結元件的實例.

(=>
      (connectedEngineeringComponents ?COMP1 ?COMP2)
      (not
            (or
                  (instance ?COMP1 EngineeringConnection)
                  (instance ?COMP2 EngineeringConnection))))

If connection 是工程連結元件的實例, then there exist comp1,comp2 so that connection 連結 comp1 和 comp2.

(=>
      (instance ?CONNECTION EngineeringConnection)
      (exists
            (?COMP1 ?COMP2)
            (connectsEngineeringComponents ?CONNECTION ?COMP1 ?COMP2)))

If group 是群體的實例 and memb 是 group的成員, then memb 是施事者的實例.

(=>
      (and
            (instance ?GROUP Group)
            (member ?MEMB ?GROUP))
      (instance ?MEMB Agent))

if group 是年齡層的實例,
then for all memb1,memb2,age1,age2 holds: if memb1 是 group的成員 and memb2 是 group的成員 and memb1 的 �~紀是 age1 and memb2 的 �~紀是 age2, then age1 等於 age2

(=>
      (instance ?GROUP AgeGroup)
      (forall
            (?MEMB1 ?MEMB2 ?AGE1 ?AGE2)
            (=>
                  (and
                        (member ?MEMB1 ?GROUP)
                        (member ?MEMB2 ?GROUP)
                        (age ?MEMB1 ?AGE1)
                        (age ?MEMB2 ?AGE2))
                  (equal ?AGE1 ?AGE2))))

if group 是親屬∕宗族的實例,
then for all memb1,memb2 holds: if memb1 是 group的成員 and memb2 是 group的成員, then memb1 和 memb2 相關

(=>
      (instance ?GROUP FamilyGroup)
      (forall
            (?MEMB1 ?MEMB2)
            (=>
                  (and
                        (member ?MEMB1 ?GROUP)
                        (member ?MEMB2 ?GROUP))
                  (familyRelation ?MEMB1 ?MEMB2))))

If organism1 和 organism2 相關, then there exists organism3 so that organism3 和 organism1 相關 and organism3 和 organism2 相關.

(=>
      (familyRelation ?ORGANISM1 ?ORGANISM2)
      (exists
            (?ORGANISM3)
            (and
                  (familyRelation ?ORGANISM3 ?ORGANISM1)
                  (familyRelation ?ORGANISM3 ?ORGANISM2))))

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)))

If org (沒) 雇用not(s) person, then person 是 org的成員.

(=>
      (employs ?ORG ?PERSON)
      (member ?PERSON ?ORG))

If pol 是政治組織的實例, then there exists 政治歷程 proc so that proc 是 pol 的施事者.

(=>
      (instance ?POL PoliticalOrganization)
      (exists
            (?PROC)
            (and
                  (instance ?PROC PoliticalProcess)
                  (agent ?PROC ?POL))))

If plan 是計畫的實例 and obj 是內容載體的實例 and obj (不) �]含s) 訊息 %2, then there exists 計畫 planning so that obj 是 planning 的結果.

(=>
      (and
            (instance ?PLAN Plan)
            (instance ?OBJ ContentBearingObject)
            (containsInformation ?OBJ ?PLAN))
      (exists
            (?PLANNING)
            (and
                  (instance ?PLANNING Planning)
                  (result ?PLANNING ?OBJ))))

If plan 是計畫的實例, then there exists purp so that plan 有意圖 purp.

(=>
      (instance ?PLAN Plan)
      (exists
            (?PURP)
            (hasPurpose ?PLAN ?PURP)))

If obj1 對 obj2 是 attr1 and 對立於 ? and attr1 是 "()" 的一成員 and attr2 是 "()" 的一成員 and attr1 等於 attr2, then obj1 對 obj2 是 not attr2.

(=>
      (and
            (orientation ?OBJ1 ?OBJ2 ?ATTR1)
            (contraryAttribute @ROW)
            (inList
                  ?ATTR1
                  (ListFn @ROW))
            (inList
                  ?ATTR2
                  (ListFn @ROW))
            (not
                  (equal ?ATTR1 ?ATTR2)))
      (not
            (orientation ?OBJ1 ?OBJ2 ?ATTR2)))

if 實體在歷程 proc 正移動 attr1 timea(之中) time,
then for all attr2 holds: if 實體在歷程 proc 正移動 attr2 timea(之中) time, then attr2 等於 attr1

(=>
      (holdsDuring
            ?TIME
            (direction ?PROC ?ATTR1))
      (forall
            (?ATTR2)
            (=>
                  (holdsDuring
                        ?TIME
                        (direction ?PROC ?ATTR2))
                  (equal ?ATTR2 ?ATTR1))))

if proc 面對 attr1 timea(之中) time,
then for all attr2 holds: if proc 面對 attr2 timea(之中) time, then attr2 等於 attr1

(=>
      (holdsDuring
            ?TIME
            (faces ?PROC ?ATTR1))
      (forall
            (?ATTR2)
            (=>
                  (holdsDuring
                        ?TIME
                        (faces ?PROC ?ATTR2))
                  (equal ?ATTR2 ?ATTR1))))

If item 有屬性 value and value 是真值的實例, then item 是句子的實例 or item 是命題的實例.

(=>
      (and
            (property ?ITEM ?VALUE)
            (instance ?VALUE TruthValue))
      (or
            (instance ?ITEM Sentence)
            (instance ?ITEM Proposition)))

If formula 有屬性可能的, then ""formula &$是真的" 的或然率" (不) 大於 ""formula &$是假的" 的或然率".

(=>
      (property ?FORMULA Likely)
      (greaterThan
            (ProbabilityFn
                  (true ?FORMULA True))
            (ProbabilityFn
                  (true ?FORMULA False))))

If formula 有屬性不太可能的, then ""formula &$是假的" 的或然率" (不) 大於 ""formula &$是真的" 的或然率".

(=>
      (property ?FORMULA Unlikely)
      (greaterThan
            (ProbabilityFn
                  (true ?FORMULA False))
            (ProbabilityFn
                  (true ?FORMULA True))))

If obj1 對 obj2 是 attr1 and attr1 是方向屬性的實例 and attr2 是方向屬性的實例 and attr1 等於 attr2, then obj1 對 obj2 是 not attr2.

(=>
      (and
            (orientation ?OBJ1 ?OBJ2 ?ATTR1)
            (instance ?ATTR1 DirectionalAttribute)
            (instance ?ATTR2 DirectionalAttribute)
            (not
                  (equal ?ATTR1 ?ATTR2)))
      (not
            (orientation ?OBJ1 ?OBJ2 ?ATTR2)))

If direct 是方向屬性的實例 and obj1 對 obj2 是 direct and obj2 對 obj3 是 direct, then obj2 介於 obj1 和 obj33 中間.

(=>
      (and
            (instance ?DIRECT DirectionalAttribute)
            (orientation ?OBJ1 ?OBJ2 ?DIRECT)
            (orientation ?OBJ2 ?OBJ3 ?DIRECT))
      (between ?OBJ1 ?OBJ2 ?OBJ33))

If obj1 對 obj2 是在...之上, then obj1 與 obj2 相連.

(=>
      (orientation ?OBJ1 ?OBJ2 Above)
      (not
            (connected ?OBJ1 ?OBJ2)))

If obj1 對 obj2 是在...之下, then obj2 對 obj1 是在...上 or obj2 對 obj1 是在...之上.

(=>
      (orientation ?OBJ1 ?OBJ2 Below)
      (or
            (orientation ?OBJ2 ?OBJ1 On)
            (orientation ?OBJ2 ?OBJ1 Above)))

If obj1 對 obj2 是鄰近的, then obj1 對 obj2 是接近 or obj1 與 obj2 相連.

(=>
      (orientation ?OBJ1 ?OBJ2 Adjacent)
      (or
            (orientation ?OBJ1 ?OBJ2 Near)
            (connected ?OBJ1 ?OBJ2)))

If obj1 對 obj2 是接近, then obj1 與 obj2 相連.

(=>
      (orientation ?OBJ1 ?OBJ2 Near)
      (not
            (connected ?OBJ1 ?OBJ2)))

If obj1 對 obj2 是接近, then obj2 對 obj1 是接近.

(=>
      (orientation ?OBJ1 ?OBJ2 Near)
      (orientation ?OBJ2 ?OBJ1 Near))

If obj1 對 obj2 是在...上, then obj1 與 obj2 相連.

(=>
      (orientation ?OBJ1 ?OBJ2 On)
      (connected ?OBJ1 ?OBJ2))

If obj1 對 obj2 是在...上, then obj1 位於 obj2.

(=>
      (orientation ?OBJ1 ?OBJ2 On)
      (located ?OBJ1 ?OBJ2))

If obj1 對 obj2 是在...上, then obj2 對 obj1 是 not 在...上.

(=>
      (orientation ?OBJ1 ?OBJ2 On)
      (not
            (orientation ?OBJ2 ?OBJ1 On)))

If "相對時間函數" 等於 time2, then time2 等於 "(time1+)".

(=>
      (equal
            (RelativeTimeFn ?TIME1 PacificTimeZone)
            ?TIME2)
      (equal
            ?TIME2
            (AdditionFn ?TIME1 8)))

If "相對時間函數" 等於 time2, then time2 等於 "(time1+)".

(=>
      (equal
            (RelativeTimeFn ?TIME1 MountainTimeZone)
            ?TIME2)
      (equal
            ?TIME2
            (AdditionFn ?TIME1 7)))

If "相對時間函數" 等於 time2, then time2 等於 "(time1+)".

(=>
      (equal
            (RelativeTimeFn ?TIME1 CentralTimeZone)
            ?TIME2)
      (equal
            ?TIME2
            (AdditionFn ?TIME1 6)))

If "相對時間函數" 等於 time2, then time2 等於 "(time1+)".

(=>
      (equal
            (RelativeTimeFn ?TIME1 EasternTimeZone)
            ?TIME2)
      (equal
            ?TIME2
            (AdditionFn ?TIME1 5)))

If attribute 是 person 的屬性 and attribute 是社會角色的實例, then person 是人類的實例.

(=>
      (and
            (attribute ?PERSON ?ATTRIBUTE)
            (instance ?ATTRIBUTE SocialRole))
      (instance ?PERSON Human))

If org (沒) 雇用not(s) person, then there exists position so that person 佔 position 的職位在 org.

(=>
      (employs ?ORG ?PERSON)
      (exists
            (?POSITION)
            (occupiesPosition ?PERSON ?POSITION ?ORG)))

If 陳述 formula1 有 prop 的型態意義 and 推知(formula1,formula2) holds, then 陳述 formula2 有 prop 的型態意義.

(=>
      (and
            (modalAttribute ?FORMULA1 ?PROP)
            (entails ?FORMULA1 ?FORMULA2))
      (modalAttribute ?FORMULA2 ?PROP))

If agent 有義務執行類型 process 任務, then 陳述 "there exists process instance so that instance 是 agent 的施事者" 有義務的型態意義.

(=>
      (holdsObligation ?PROCESS ?AGENT)
      (modalAttribute
            (exists
                  (?INSTANCE)
                  (and
                        (instance ?INSTANCE ?PROCESS)
                        (agent ?INSTANCE ?AGENT)))
            Obligation))

If agent 有權使 process 為真, then 陳述 "there exists process instance so that instance 是 agent 的施事者" 有許可的型態意義.

(=>
      (holdsRight ?PROCESS ?AGENT)
      (modalAttribute
            (exists
                  (?INSTANCE)
                  (and
                        (instance ?INSTANCE ?PROCESS)
                        (agent ?INSTANCE ?AGENT)))
            Permission))

If attr 是 obj 的屬性 and attr 是競爭屬性的實例, then there exists 競爭 contest so that contest 是 obj 的施事者 or obj 是 contest 的受事者.

(=>
      (and
            (attribute ?OBJ ?ATTR)
            (instance ?ATTR ContestAttribute))
      (exists
            (?CONTEST)
            (and
                  (instance ?CONTEST Contest)
                  (or
                        (agent ?CONTEST ?OBJ)
                        (patient ?CONTEST ?OBJ)))))

If 陳述 formula 有必要性的型態意義, then 陳述 formula 有可能性的型態意義.

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

If 陳述 formula 有義務的型態意義, then 陳述 formula 有許可的型態意義.

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

If entity 有屬性承諾, then entity 有屬性契約 or entity 有屬性單方承諾.

(=>
      (property ?ENTITY Promise)
      (or
            (property ?ENTITY Contract)
            (property ?ENTITY NakedPromise)))

If obj 是溶液的實例, then 液體的是 obj 的屬性.

(=>
      (instance ?OBJ Solution)
      (attribute ?OBJ Liquid))

If perception 是知覺的實例 and obj 是 perception 的受事者, then there exists 知覺屬性 prop so that prop 是 obj 的屬性.

(=>
      (and
            (instance ?PERCEPTION Perception)
            (patient ?PERCEPTION ?OBJ))
      (exists
            (?PROP)
            (and
                  (instance ?PROP PerceptualAttribute)
                  (attribute ?OBJ ?PROP))))

If obj 是食物的實例, then there exists 味覺屬性 attr so that attr 是 obj 的屬性.

(=>
      (instance ?OBJ Food)
      (exists
            (?ATTR)
            (and
                  (instance ?ATTR TasteAttribute)
                  (attribute ?OBJ ?ATTR))))

if 單色的是 obj 的屬性 and part 是 obj的 �~表部分 and color 是 part 的屬性 and color 是原色的實例,
then for all element holds: if element 是 obj的 �~表部分, then color 是 element 的屬性

(=>
      (and
            (attribute ?OBJ Monochromatic)
            (superficialPart ?PART ?OBJ)
            (attribute ?PART ?COLOR)
            (instance ?COLOR PrimaryColor))
      (forall
            (?ELEMENT)
            (=>
                  (superficialPart ?ELEMENT ?OBJ)
                  (attribute ?ELEMENT ?COLOR))))

If obj 是物體的實例, then 單色的是 obj 的屬性 or 多彩的是 obj 的屬性.

(=>
      (instance ?OBJ Object)
      (or
            (attribute ?OBJ Monochromatic)
            (attribute ?OBJ Polychromatic)))

If 多彩的是 obj 的屬性, then there exist part1,part2,顏色屬性 color1,顏色屬性 color2 so that part1 是 obj的 �~表部分 and part2 是 obj的 �~表部分 and color1 是 part1 的屬性 and color2 是 part2 的屬性 and color1 等於 color2.

(=>
      (attribute ?OBJ Polychromatic)
      (exists
            (?PART1 ?PART2 ?COLOR1 ?COLOR2)
            (and
                  (superficialPart ?PART1 ?OBJ)
                  (superficialPart ?PART2 ?OBJ)
                  (attribute ?PART1 ?COLOR1)
                  (attribute ?PART2 ?COLOR2)
                  (instance ?COLOR1 ColorAttribute)
                  (instance ?COLOR2 ColorAttribute)
                  (not
                        (equal ?COLOR1 ?COLOR2)))))

If there exists 形狀改變 change so that obj 是 change 的受事者, then 可變形的是 obj 的屬性.

(=>
      (exists
            (?CHANGE)
            (and
                  (instance ?CHANGE ShapeChange)
                  (patient ?CHANGE ?OBJ)))
      (attribute ?OBJ Pliable))

If obj 是自身連續物體的實例, then 可變形的是 obj 的屬性 or 不易彎曲的是 obj 的屬性.

(=>
      (instance ?OBJ SelfConnectedObject)
      (or
            (attribute ?OBJ Pliable)
            (attribute ?OBJ Rigid)))

If attribute 是（表面）質地屬性的實例 and attribute 是 obj 的屬性 and surface 是 obj 的表面, then attribute 是 surface 的屬性.

(=>
      (and
            (instance ?ATTRIBUTE TextureAttribute)
            (attribute ?OBJ ?ATTRIBUTE)
            (surface ?SURFACE ?OBJ))
      (attribute ?SURFACE ?ATTRIBUTE))

If 乾的是 obj 的屬性, then there doesn't exist subobj so that subobj 是 obj 的部分) and 液體的是 subobj 的屬性.

(=>
      (attribute ?OBJ Dry)
      (not
            (exists
                  (?SUBOBJ)
                  (and
                        (part ?SUBOBJ ?OBJ)
                        (attribute ?SUBOBJ Liquid)))))

if 濕的是 obj 的屬性,
then for all part holds: if part 是 obj 的部分), then there exists subpart so that subpart 是 part 的部分) and 液體的是 subpart 的屬性

(=>
      (attribute ?OBJ Wet)
      (forall
            (?PART)
            (=>
                  (part ?PART ?OBJ)
                  (exists
                        (?SUBPART)
                        (and
                              (part ?SUBPART ?PART)
                              (attribute ?SUBPART Liquid))))))

If 不易碎的是 obj 的屬性, then there doesn't exist 損害 damage so that obj 是 damage 的受事者.

(=>
      (attribute ?OBJ Unbreakable)
      (not
            (exists
                  (?DAMAGE)
                  (and
                        (instance ?DAMAGE Damaging)
                        (patient ?DAMAGE ?OBJ)))))

If att 是 org 的屬性 and att 是生物屬性的實例, then org 是生物體的實例.

(=>
      (and
            (attribute ?ORG ?ATT)
            (instance ?ATT BiologicalAttribute))
      (instance ?ORG Organism))

If organism 是生物體的實例 and process 是 organism 的施事者, then 活的是 organism 的屬性 "process 存在的時間"a(之中) process 存在的時間.

(=>
      (and
            (instance ?ORGANISM Organism)
            (agent ?PROCESS ?ORGANISM))
      (holdsDuring
            (WhenFn ?PROCESS)
            (attribute ?ORGANISM Living)))

If org 是生物體的實例, then there exists 有生屬性 attr so that attr 是 org 的屬性.

(=>
      (instance ?ORG Organism)
      (exists
            (?ATTR)
            (and
                  (instance ?ATTR AnimacyAttribute)
                  (attribute ?ORG ?ATTR))))

If body 是生殖構造的實例 and body 是 org 的部分) and org 是生物體的實例, then 雌性是 org 的屬性.

(=>
      (and
            (instance ?BODY ReproductiveBody)
            (part ?BODY ?ORG)
            (instance ?ORG Organism))
      (attribute ?ORG Female))

If animal 是動物的實例, then there exists 性別屬性 attr so that attr 是 animal 的屬性.

(=>
      (instance ?ANIMAL Animal)
      (exists
            (?ATTR)
            (and
                  (instance ?ATTR SexAttribute)
                  (attribute ?ANIMAL ?ATTR))))

If 完全形成的是 obj 的屬性, then there exists 生長 growth so that obj (沒) 體驗not(s) growth and 未完全形成的是 obj 的屬性 ""obj 存在的時間" 的 �}始"a(之中) "obj 存在的時間" 的 �}始.

(=>
      (attribute ?OBJ FullyFormed)
      (exists
            (?GROWTH)
            (and
                  (instance ?GROWTH Growth)
                  (experiencer ?GROWTH ?OBJ)
                  (holdsDuring
                        (BeginFn
                              (WhenFn ?OBJ))
                        (attribute ?OBJ NonFullyFormed)))))

If org 是生物體的實例, then there exists 發展屬性 attr so that attr 是 org 的屬性.

(=>
      (instance ?ORG Organism)
      (exists
            (?ATTR)
            (and
                  (instance ?ATTR DevelopmentalAttribute)
                  (attribute ?ORG ?ATTR))))

If 幼體的是 org 的屬性 timea(之中) time, then there exists 誕生 birth so that org (沒) 體驗not(s) birth "time 之前"a(之中) time 之前.

(=>
      (holdsDuring
            ?TIME
            (attribute ?ORG Larval))
      (holdsDuring
            (PastFn ?TIME)
            (exists
                  (?BIRTH)
                  (and
                        (instance ?BIRTH Birth)
                        (experiencer ?BIRTH ?ORG)))))

If 胚胎的是 org 的屬性, then there exists 生殖構造 body so that org 位於 body.

(=>
      (attribute ?ORG Embryonic)
      (exists
            (?BODY)
            (and
                  (instance ?BODY ReproductiveBody)
                  (located ?ORG ?BODY))))

If 胚胎的是 org 的屬性 timea(之中) time, then there doesn't exist 誕生 birth so that org (沒) 體驗not(s) birth timea(之中) time.

(=>
      (holdsDuring
            ?TIME
            (attribute ?ORG Embryonic))
      (holdsDuring
            ?TIME
            (not
                  (exists
                        (?BIRTH)
                        (and
                              (instance ?BIRTH Birth)
                              (experiencer ?BIRTH ?ORG))))))

if attr 是心理屬性的實例,
then if attr 是 organism 的屬性 timea(之中) time, then 活的是 organism 的屬性 timea(之中) time

(=>
      (instance ?ATTR PsychologicalAttribute)
      (=>
            (holdsDuring
                  ?TIME
                  (attribute ?ORGANISM ?ATTR))
            (holdsDuring
                  ?TIME
                  (attribute ?ORGANISM Living))))

If attr 是心理屬性的實例 and attr 是 agent 的屬性, then agent 是能知覺的行為主體的實例.

(=>
      (and
            (instance ?ATTR PsychologicalAttribute)
            (attribute ?AGENT ?ATTR))
      (instance ?AGENT SentientAgent))

If class1 是集合或種類的實例 and class2 是集合或種類的實例, then "class1 和 class2 的差異" 等於 "class1 和 "class2 的互補" 的聯集".

(=>
      (and
            (instance ?CLASS1 SetOrClass)
            (instance ?CLASS2 SetOrClass))
      (equal
            (RelativeComplementFn ?CLASS1 ?CLASS2)
            (IntersectionFn
                  ?CLASS1
                  (ComplementFn ?CLASS2))))

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))))