序列函數 (ListFn)
A Function that takes any number of arguments and
returns the List containing those arguments in exactly the same order.
Ontology
SUMO / BASE-ONTOLOGYClass(es)
Coordinate term(s)
指定函數
最大公約數函數
最小公倍數函數
矛盾屬性
無交集分解
無交集關係
窮盡的屬性
窮盡的分解
成立
分割
Axioms (27)
- 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 無交集關係() 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 無交集關係() 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)))
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 是 意圖關係 的 實例 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 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 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))
""(,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))))
"()" (沒）初始化not(s) "(,item)".
(initialList
(ListFn @ROW)
(ListFn @ROW ?ITEM))
- 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 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 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)))
