所有 (forall)
The universal quantifier of predicate logic.
Ontology
SUMO / STRUCTURAL-ONTOLOGYClass(es)
Coordinate term(s)
若且唯若
若
和
推知
存在
非
或
Type restrictions
forall(序列, SUO-KIF表述式)
Related WordNet synsets
See more related synsets on a separate page.
Axioms (114)
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 是 集合或種類 的 實例
and - class 是 集合或種類 的 實例
and - for all inst holds: if inst 是 subclass 的 實例, then inst 是 class 的 實例
.
(<=>
(subclass ?SUBCLASS ?CLASS)
(and
(instance ?SUBCLASS SetOrClass)
(instance ?CLASS SetOrClass)
(forall
(?INST)
(=>
(instance ?INST ?SUBCLASS)
(instance ?INST ?CLASS)))))
If thing1 等於 thing2, then for all attr holds: thing1 有 屬性 attr if and only if thing2 有 屬性 attr.
(=>
(equal ?THING1 ?THING2)
(forall
(?ATTR)
(<=>
(property ?THING1 ?ATTR)
(property ?THING2 ?ATTR))))
If attr1 等於 attr2, then for all thing holds: thing 有 屬性 attr1 if and only if thing 有 屬性 attr2.
(=>
(equal ?ATTR1 ?ATTR2)
(forall
(?THING)
(<=>
(property ?THING ?ATTR1)
(property ?THING ?ATTR2))))
If thing1 等於 thing2, then for all class holds: thing1 是 class 的 實例 if and only if thing2 是 class 的 實例.
(=>
(equal ?THING1 ?THING2)
(forall
(?CLASS)
(<=>
(instance ?THING1 ?CLASS)
(instance ?THING2 ?CLASS))))
If class1 等於 class2, then for all thing holds: thing 是 class1 的 實例 if and only if thing 是 class2 的 實例.
(=>
(equal ?CLASS1 ?CLASS2)
(forall
(?THING)
(<=>
(instance ?THING ?CLASS1)
(instance ?THING ?CLASS2))))
If rel1 等於 rel2, then for all holds: rel1() (不) 成立s if and only if rel2() (不) 成立s.
(=>
(equal ?REL1 ?REL2)
(forall
(@ROW)
(<=>
(holds ?REL1 @ROW)
(holds ?REL2 @ROW))))
- if 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)))))
class1 無交集 於 class2 if and only if - class1 是 集合或種類 的 實例
and - class2 是 集合或種類 的 實例
and - for all inst holds: inst 是 class1 的 實例 or inst 是 class2 的 實例
.
(<=>
(disjoint ?CLASS1 ?CLASS2)
(and
(instance ?CLASS1 SetOrClass)
(instance ?CLASS2 SetOrClass)
(forall
(?INST)
(not
(and
(instance ?INST ?CLASS1)
(instance ?INST ?CLASS2))))))
- if 對立於 ?,
- 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 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 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 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))))
coll1 是 coll2 的 正 次聚集 if and only if - coll1 是 群集 的 實例
and - coll2 是 群集 的 實例
and - 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)))))
"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))))
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 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))))
- 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 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 "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))))
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 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 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 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 次類肇因,
- 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 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 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 抑制(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))))))))
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 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 " 的 最大公約數" 等於 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 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 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 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 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
- "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 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 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 "劃分 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 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 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 每 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 "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))))
- 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 和 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 分解成 ? 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 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))))))
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 是 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 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 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 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 (沒) 填充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 等於 "洞 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 for all region holds: if proc 位於 region, then subproc 位於 region
.
(=>
(subProcess ?SUBPROC ?PROC)
(forall
(?REGION)
(=>
(located ?PROC ?REGION)
(located ?SUBPROC ?REGION))))
- if
- path1 伴隨 process 發生 的 process路徑
and - process (不) �_源s 於 source
and - process (不) 終結not(s) dest
and - path1 的 長度 是 measure1
and - 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 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 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 war 是 戰爭 的 實例 and war 是 agent 的 施事者,
- then
- agent 是 國家 的 實例
or - agent 是 組織 的 實例
and - 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 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 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 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 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 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 實體 在 歷程 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))))
For all org holds: org not(沒) 雇用(s) person and person 是 人類 的 實例 if and only if 失業的 是 person 的 屬性.
(<=>
(forall
(?ORG)
(and
(not
(employs ?ORG ?PERSON))
(instance ?PERSON Human)))
(attribute ?PERSON Unemployed))
- 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 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))))))
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))))
