相等 (equal)
(equal entity1 entity2) is true just in case
entity1 is identical with entity2.
Ontology
SUMO / STRUCTURAL-ONTOLOGYClass(es)
Coordinate term(s)
加法函數
除法函數
指數函數
最大值函數
最小值函數
乘法函數
倒數函數
餘數函數
整數函數
減法函數
弧線重量
作者
先於或同時
肇因
次類肇因
公民
封閉於
相連的
包含訊息
共生
複製
日期
降低可能性
發展期形式
無交集
分配
文字說明
持續時間
較早
編者
元素
雇用
等同關係於
訊息等同類
訊息等同物
利用
以...語言表達
面對
家族關係
完成
次數
圖部分
大於
大於或等於
有意圖
有技巧
在...期間為真
須使...為真
有權使...為真
洞
同一元素
串列中
在注意範圍中
增加可能性
獨立或然率
居住
抑制
初始化序列
實例
倒序
非反射於...
大於
小於
小於或等於
物質
測量
時段相接
情態屬性
時段重疊
雙親
偏序於...
部分位於
路徑長
擁有
先決條件
避免
特性
出版
範圍
範圍次種類
提及
反射於...
SUMO內部相關概念
兄弟姊妹
小於
開始
次屬性
次聚集
次圖
次序列
次歷程
次命題
次種類
次關係
包含訊息種類
包含訊息實例
續接屬性
封閉續接屬性
時間部分
時間
全序於...
三分法
使用
（結合）價
人造物版本
Type restrictions
equal(實體, 實體)
Related WordNet synsets
- sameness
- the quality of being alike: "sameness of purpose kept them together"
- identity, identicalness, indistinguishability
- exact sameness; "they shared an identity of interests"
- equality
- the quality or state of being the same in quantity or measure or value or status
- equivalence
- essential equality and interchangeability
- equatability
- capability of being equated
- changelessness
- the property of remaining unchanged
- equivalent
- a person or thing equal to another in value or measure or force or effect or significance etc: "send two dollars or the equivalent in stamps"
- equate, correspond
- be equivalent or parallel, in mathematics
- equal, be
- be identical or equivalent to: "One dollar equals 1,000 rubles these days!"
- equal
- well matched; having the same quantity, value, or measure as another; "on equal terms"; "all men are equal before the law"
- like, equal, equivalent, same
- equal in amount or value; "like amounts"; "equivalent amounts"; "the same amount"; "gave one six blows and the other a like number"; "an equal number"; "the same number"
- same
- same in identity; "the same man I saw yesterday"; "never wore the same dress twice"; "this road is the same one we were on yesterday"; "on the same side of the street"
See more related synsets on a separate page.
Axioms (245)
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 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 被 function 歸回 的值 是 class的 次種類 and "function()" 等於 value, then value 是 class 的 次種類.
(=>
(and
(rangeSubclass ?FUNCTION ?CLASS)
(equal
(AssignmentFn ?FUNCTION @ROW)
?VALUE))
(subclass ?VALUE ?CLASS))
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 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 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 rel(,inst) (不) 成立s and rel 是 函數 的 實例, then "rel()" 等於 inst.
(=>
(and
(holds ?REL @ROW ?INST)
(instance ?REL Function))
(equal
(AssignmentFn ?REL @ROW)
?INST))
- 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 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 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)))))
"class 的 描述" 等於 attr if and only if for all inst holds: inst 是 class 的 實例 if and only if inst 有 屬性 attr.
(<=>
(equal
(AbstractionFn ?CLASS)
?ATTR)
(forall
(?INST)
(<=>
(instance ?INST ?CLASS)
(property ?INST ?ATTR))))
"種類 符合 attribute" 等於 class if and only if "class 的 描述" 等於 attribute.
(<=>
(equal
(ExtensionFn ?ATTRIBUTE)
?CLASS)
(equal
(AbstractionFn ?CLASS)
?ATTRIBUTE))
number1 小於或等於 number2 if and only if number1 等於 number2 or number1 小於 number2.
(<=>
(lessThanOrEqualTo ?NUMBER1 ?NUMBER2)
(or
(equal ?NUMBER1 ?NUMBER2)
(lessThan ?NUMBER1 ?NUMBER2)))
number1 大於或等於 number2 if and only if number1 等於 number2 or number1 (不) 大於 number2.
(<=>
(greaterThanOrEqualTo ?NUMBER1 ?NUMBER2)
(or
(equal ?NUMBER1 ?NUMBER2)
(greaterThan ?NUMBER1 ?NUMBER2)))
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)))))))
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 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 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 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))))
list 等於 空列 if and only if there doesn't exist item so that item 是 list 的 一 成員.
(<=>
(equal ?LIST NullList)
(not
(exists
(?ITEM)
(inList ?ITEM ?LIST))))
- 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 "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))))
""(,item)" 的 長度" 等於 "(""()" 的 長度"+1)".
(equal
(ListLengthFn
(ListFn @ROW ?ITEM))
(SuccessorFn
(ListLengthFn
(ListFn @ROW))))
""(,item)" 的 第二 元素" 等於 item.
(equal
(ListOrderFn
(ListFn @ROW ?ITEM)
(ListLengthFn
(ListFn @ROW ?ITEM)))
?ITEM)
- 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))))))
item 是 list 的 一 成員 if and only if there exists number so that "list 的 第二 元素" 等於 item.
(<=>
(inList ?ITEM ?LIST)
(exists
(?NUMBER)
(equal
(ListOrderFn ?LIST ?NUMBER)
?ITEM)))
- 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 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 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 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 分配(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 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))))))
"thing 在 time 的 time位置" 等於 region if and only if thing 精確位於 region timea(之中) time.
(<=>
(equal
(WhereFn ?THING ?TIME)
?REGION)
(holdsDuring
?TIME
(exactlyLocated ?THING ?REGION)))
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))
"(number+1)" 等於 "(number+)".
(equal
(SuccessorFn ?NUMBER)
(AdditionFn ?NUMBER 1))
"(number+2)" 等於 "(number-)".
(equal
(PredecessorFn ?NUMBER)
(SubtractionFn ?NUMBER 1))
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)))))
"number1 的 絕對 值" 等於 number2 and number1 是 實數 的 實例 and number2 是 實數 的 實例 if and only if - number1 是 非負實數 的 實例 and number1 等於 number2
or - number1 是 負實數 的 實例 and number2 等於 "(-number1)"
.
(<=>
(and
(equal
(AbsoluteValueFn ?NUMBER1)
?NUMBER2)
(instance ?NUMBER1 RealNumber)
(instance ?NUMBER2 RealNumber))
(or
(and
(instance ?NUMBER1 NonnegativeRealNumber)
(equal ?NUMBER1 ?NUMBER2))
(and
(instance ?NUMBER1 NegativeRealNumber)
(equal
?NUMBER2
(SubtractionFn 0 ?NUMBER1)))))
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
or - number 等於 number2 and number2 (不) 大於 number1
or - 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
or - number 等於 number2 and number2 小於 number1
or - 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))))
"number1 取餘數 number2" 等於 number if and only if "(""最大 整數 小於 或 等於 "number1/number2""*number2"+number)" 等於 number1.
(<=>
(equal
(RemainderFn ?NUMBER1 ?NUMBER2)
?NUMBER)
(equal
(AdditionFn
(MultiplicationFn
(FloorFn
(DivisionFn ?NUMBER1 ?NUMBER2))
?NUMBER2)
?NUMBER)
?NUMBER1))
If "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"
or - 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+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 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 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
or - path 是 graph 的 次圖
and - path 是 圖路徑 的 實例
and - "path 的 最初�`點" 等於 node1 and "path 的 最後�`點" 等於 node2
or - "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 是 圖路徑 的 實例 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)))))))
graph 是 圖形迴路 的 實例 if and only if there exists node so that "graph 的 最初�`點" 等於 node and "graph 的 最後�`點" 等於 node.
(<=>
(instance ?GRAPH GraphCircuit)
(exists
(?NODE)
(and
(equal
(BeginNodeFn ?GRAPH)
?NODE)
(equal
(EndNodeFn ?GRAPH)
?NODE))))
graph 是 多圖 的 實例 if and only if there exist arc1,arc2,node1,node2 so that arc1 是 graph 的 部分 and arc2 是 graph 的 部分 and node1 是 graph 的 部分 and node2 是 graph 的 部分 and arc1 (沒) 連結not(s) node1 和 node2 and arc2 (沒) 連結not(s) node1 和 node2 and arc1 等於 arc2.
(<=>
(instance ?GRAPH MultiGraph)
(exists
(?ARC1 ?ARC2 ?NODE1 ?NODE2)
(and
(graphPart ?ARC1 ?GRAPH)
(graphPart ?ARC2 ?GRAPH)
(graphPart ?NODE1 ?GRAPH)
(graphPart ?NODE2 ?GRAPH)
(links ?NODE1 ?NODE2 ?ARC1)
(links ?NODE1 ?NODE2 ?ARC2)
(not
(equal ?ARC1 ?ARC2)))))
If "arc 的 �_始節點" 等於 node and "arc 的 最終�`點" 等於 node, then arc 是 圖迴圈 的 實例.
(=>
(and
(equal
(InitialNodeFn ?ARC)
?NODE)
(equal
(TerminalNodeFn ?ARC)
?NODE))
(instance ?ARC GraphLoop))
- if
- "path 的 路�|長量值" 等於 sum
and - subpath 是 path 的 次圖
and - arc1 是 path 的 部分
and - arc1 的 弧線量 是 number1
and - 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
and - arc1 是 path 的 部分
and - arc2 是 path 的 部分
and - arc1 的 弧線量 是 number1
and - arc2 的 弧線量 是 number2
and - 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 為 兩 獨立 圖表 的 最小相交路�|" 等於 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 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 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)))
"person 的 財產 的 價值" 等於 amount if and only if "person 的 附屬物" 的 價值 是 amount.
(<=>
(equal
(WealthFn ?PERSON)
?AMOUNT)
(monetaryValue
(PropertyFn ?PERSON)
?AMOUNT))
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 "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 "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))))
interval1 (沒) �}始s interval2 if and only if "interval1 的 �}始" 等於 "interval2 的 �}始" and "interval1 的 結束" (沒) 發生?{s} 在 "interval2 的 結束" 之前.
(<=>
(starts ?INTERVAL1 ?INTERVAL2)
(and
(equal
(BeginFn ?INTERVAL1)
(BeginFn ?INTERVAL2))
(before
(EndFn ?INTERVAL1)
(EndFn ?INTERVAL2))))
interval1 (沒) 完成s interval2 if and only if "interval2 的 �}始" (沒) 發生?{s} 在 "interval1 的 �}始" 之前 and "interval2 的 結束" 等於 "interval1 的 結束".
(<=>
(finishes ?INTERVAL1 ?INTERVAL2)
(and
(before
(BeginFn ?INTERVAL2)
(BeginFn ?INTERVAL1))
(equal
(EndFn ?INTERVAL2)
(EndFn ?INTERVAL1))))
If point1 (沒) 發生?{s} 在 point2 或 之前, then point1 (沒) 發生?{s} 在 point2 之前 or point1 等於 point2.
(=>
(beforeOrEqual ?POINT1 ?POINT2)
(or
(before ?POINT1 ?POINT2)
(equal ?POINT1 ?POINT2)))
interval1 (沒) 相接s interval2 if and only if "interval1 的 結束" 等於 "interval2 的 �}始".
(<=>
(meetsTemporally ?INTERVAL1 ?INTERVAL2)
(equal
(EndFn ?INTERVAL1)
(BeginFn ?INTERVAL2)))
If "interval1 的 �}始" 等於 "interval2 的 �}始" and "interval1 的 結束" 等於 "interval2 的 結束", then interval1 等於 interval2.
(=>
(and
(equal
(BeginFn ?INTERVAL1)
(BeginFn ?INTERVAL2))
(equal
(EndFn ?INTERVAL1)
(EndFn ?INTERVAL2)))
(equal ?INTERVAL1 ?INTERVAL2))
phys1 (沒) 與 phys2 同時 發生not(s) if and only if "phys1 存在 的 時間" 等於 "phys2 存在 的 時間".
(<=>
(cooccur ?PHYS1 ?PHYS2)
(equal
(WhenFn ?PHYS1)
(WhenFn ?PHYS2)))
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 process 是 物質的 的 實例, then ""process 存在 的 時間" 之前" 等於 "時間起點/亙古 和 ""process 存在 的 時間" 的 �}始" 的 間距".
(=>
(instance ?PROCESS Physical)
(equal
(PastFn
(WhenFn ?PROCESS))
(TimeIntervalFn
NegativeInfinity
(BeginFn
(WhenFn ?PROCESS)))))
If process 是 物質的 的 實例, then ""process 存在 的 時間" 之後" 等於 """process 存在 的 時間" 的 結束" 和 時間終點/永遠 的 間距".
(=>
(instance ?PROCESS Physical)
(equal
(FutureFn
(WhenFn ?PROCESS))
(TimeIntervalFn
(EndFn
(WhenFn ?PROCESS))
PositiveInfinity)))
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 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 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 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 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
(=>
(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 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 month1 等於 "月份 三月" and month2 等於 "月份 四月", then month1 (沒) 相接s month2.
(=>
(and
(equal
?MONTH1
(MonthFn March ?YEAR))
(equal
?MONTH2
(MonthFn April ?YEAR)))
(meetsTemporally ?MONTH1 ?MONTH2))
If month1 等於 "月份 四月" and month2 等於 "月份 五月", then month1 (沒) 相接s month2.
(=>
(and
(equal
?MONTH1
(MonthFn April ?YEAR))
(equal
?MONTH2
(MonthFn May ?YEAR)))
(meetsTemporally ?MONTH1 ?MONTH2))
If month1 等於 "月份 五月" and month2 等於 "月份 六月", then month1 (沒) 相接s month2.
(=>
(and
(equal
?MONTH1
(MonthFn May ?YEAR))
(equal
?MONTH2
(MonthFn June ?YEAR)))
(meetsTemporally ?MONTH1 ?MONTH2))
If month1 等於 "月份 六月" and month2 等於 "月份 七月", then month1 (沒) 相接s month2.
(=>
(and
(equal
?MONTH1
(MonthFn June ?YEAR))
(equal
?MONTH2
(MonthFn July ?YEAR)))
(meetsTemporally ?MONTH1 ?MONTH2))
If month1 等於 "月份 七月" and month2 等於 "月份 八月", then month1 (沒) 相接s month2.
(=>
(and
(equal
?MONTH1
(MonthFn July ?YEAR))
(equal
?MONTH2
(MonthFn August ?YEAR)))
(meetsTemporally ?MONTH1 ?MONTH2))
If month1 等於 "月份 八月" and month2 等於 "月份 九月", then month1 (沒) 相接s month2.
(=>
(and
(equal
?MONTH1
(MonthFn August ?YEAR))
(equal
?MONTH2
(MonthFn September ?YEAR)))
(meetsTemporally ?MONTH1 ?MONTH2))
If month1 等於 "月份 九月" and month2 等於 "月份 十月", then month1 (沒) 相接s month2.
(=>
(and
(equal
?MONTH1
(MonthFn September ?YEAR))
(equal
?MONTH2
(MonthFn October ?YEAR)))
(meetsTemporally ?MONTH1 ?MONTH2))
If month1 等於 "月份 十月" and month2 等於 "月份 十一月", then month1 (沒) 相接s month2.
(=>
(and
(equal
?MONTH1
(MonthFn October ?YEAR))
(equal
?MONTH2
(MonthFn November ?YEAR)))
(meetsTemporally ?MONTH1 ?MONTH2))
If month1 等於 "月份 十一月" and month2 等於 "月份 十二月", then month1 (沒) 相接s month2.
(=>
(and
(equal
?MONTH1
(MonthFn November ?YEAR))
(equal
?MONTH2
(MonthFn December ?YEAR)))
(meetsTemporally ?MONTH1 ?MONTH2))
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 "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))
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 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 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 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 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 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 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 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 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 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 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 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))))
compound 是 化合物 的 實例 if and only if there exist 基本物質 element1,基本物質 element2,化學合成 process so that element1 等於 element2 and element1 對 process 是 資源 and element2 對 process 是 資源 and compound 是 process 的 結果.
(<=>
(instance ?COMPOUND CompoundSubstance)
(exists
(?ELEMENT1 ?ELEMENT2 ?PROCESS)
(and
(instance ?ELEMENT1 ElementalSubstance)
(instance ?ELEMENT2 ElementalSubstance)
(not
(equal ?ELEMENT1 ?ELEMENT2))
(instance ?PROCESS ChemicalSynthesis)
(resource ?PROCESS ?ELEMENT1)
(resource ?PROCESS ?ELEMENT2)
(result ?PROCESS ?COMPOUND))))
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 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 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 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 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))))
"大陸 中 實例 的 數目" 等於 .
(equal
(CardinalityFn Continent)
7)
- 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 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 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 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 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 "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 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 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 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 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 "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 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 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 "相對時間函數" 等於 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 多彩的 是 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 class1 是 集合或種類 的 實例 and class2 是 集合或種類 的 實例, then "class1 和 class2 的 差異" 等於 "class1 和 "class2 的 互補" 的 聯集".
(=>
(and
(instance ?CLASS1 SetOrClass)
(instance ?CLASS2 SetOrClass))
(equal
(RelativeComplementFn ?CLASS1 ?CLASS2)
(IntersectionFn
?CLASS1
(ComplementFn ?CLASS2))))
