非 (not)
The truth-functional connective of negation.
Ontology
SUMO / STRUCTURAL-ONTOLOGYClass(es)
Coordinate term(s)
若且唯若
若
和
推知
存在
所有
或
Type restrictions
not(SUO-KIF表述式)
Related WordNet synsets
- negation
- the negative of the opposition
- not
- negation of a word or group of words; "he does not speak French"; "she is not going"; "they are not friends"; "not many"; "not much"; "not at all"
- no
- not in any degree or manner; not at all; "he is no better today"
See more related synsets on a separate page.
Axioms (121)
If entity 是 class 的 直接 實例, then there doesn't exist class subclass so that entity 是 subclass 的 實例.
(=>
(immediateInstance ?ENTITY ?CLASS)
(not
(exists
(?SUBCLASS)
(and
(subclass ?SUBCLASS ?CLASS)
(instance ?ENTITY ?SUBCLASS)))))
If 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))))))
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 無交集關係() 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))))))
obj1 是 obj2 的 正部分 if and only if obj1 是 obj2 的 部分) and obj2 是 obj1 的 部分).
(<=>
(properPart ?OBJ1 ?OBJ2)
(and
(part ?OBJ1 ?OBJ2)
(not
(part ?OBJ2 ?OBJ1))))
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 lang 是 動物語言 的 實例 and proc 是 agent 的 施事者 and lang 對 proc 是 工具, then agent 是 動物 的 實例 and agent 是 人類 的 實例.
(=>
(and
(instance ?LANG AnimalLanguage)
(agent ?PROC ?AGENT)
(instrument ?PROC ?LANG))
(and
(instance ?AGENT Animal)
(not
(instance ?AGENT Human))))
If 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)))))
abs 是 抽象的 的 實例 if and only if there doesn't exist point so that abs 位於 point or abs (不) 存在s point 期間.
(<=>
(instance ?ABS Abstract)
(not
(exists
(?POINT)
(or
(located ?ABS ?POINT)
(time ?ABS ?POINT)))))
If rel 是 二元關係 的 實例, then there don't exist item1,item2,item3, so that rel(item1,item2,item3,) (不) 成立s.
(=>
(instance ?REL BinaryRelation)
(not
(exists
(?ITEM1 ?ITEM2 ?ITEM3 @ROW)
(holds ?REL ?ITEM1 ?ITEM2 ?ITEM3 @ROW))))
If rel 是 非反身關係 的 實例, then 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,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 there don't exist item1,item2,item3,item4, so that rel(item1,item2,item3,item4,) (不) 成立s.
(=>
(instance ?REL TernaryRelation)
(not
(exists
(?ITEM1 ?ITEM2 ?ITEM3 ?ITEM4 @ROW)
(holds ?REL ?ITEM1 ?ITEM2 ?ITEM3 ?ITEM4 @ROW))))
If rel 是 四元關係 的 實例, then there don't exist item1,item2,item3,item4,item5, so that rel(item1,item2,item3,item4,item5,) (不) 成立s.
(=>
(instance ?REL QuaternaryRelation)
(not
(exists
(?ITEM1 ?ITEM2 ?ITEM3 ?ITEM4 ?ITEM5 @ROW)
(holds ?REL ?ITEM1 ?ITEM2 ?ITEM3 ?ITEM4 ?ITEM5 @ROW))))
If rel 是 五元關係 的 實例, then there don't exist item1,item2,item3,item4,item5,item6, so that rel(item1,item2,item3,item4,item5,item6,) (不) 成立s.
(=>
(instance ?REL QuintaryRelation)
(not
(exists
(?ITEM1 ?ITEM2 ?ITEM3 ?ITEM4 ?ITEM5 ?ITEM6 @ROW)
(holds ?REL ?ITEM1 ?ITEM2 ?ITEM3 ?ITEM4 ?ITEM5 ?ITEM6 @ROW))))
- if list 是 序列 的 實例,
- then there exists number1 so that there exists item1 so that "list 的 第二 元素" 等於 item1 and for all number2 holds: if number2 是 正整數 的 實例 and number2 小於 number1, then there exists item2 so that "list 的 第二 元素" 等於 item2
.
(=>
(instance ?LIST List)
(exists
(?NUMBER1)
(exists
(?ITEM1)
(and
(not
(equal
(ListOrderFn ?LIST ?NUMBER1)
?ITEM1))
(forall
(?NUMBER2)
(=>
(and
(instance ?NUMBER2 PositiveInteger)
(lessThan ?NUMBER2 ?NUMBER1))
(exists
(?ITEM2)
(equal
(ListOrderFn ?LIST ?NUMBER2)
?ITEM2))))))))
list 等於 空列 if and only if 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 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 rel 是 變異元數關係 的 實例, then there doesn't exist int so that rel %&有 論元(s) int.
(=>
(instance ?REL VariableArityRelation)
(not
(exists
(?INT)
(valence ?REL ?INT))))
- 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 situation timea(之中) time, then situation (沒) 為真 timea(之中) time.
(=>
(holdsDuring
?TIME
(not ?SITUATION))
(not
(holdsDuring ?TIME ?SITUATION)))
If obj 精確位於 region, then there doesn't exist otherobj so that otherobj 精確位於 region and otherobj 等於 obj.
(=>
(exactlyLocated ?OBJ ?REGION)
(not
(exists
(?OTHEROBJ)
(and
(exactlyLocated ?OTHEROBJ ?REGION)
(not
(equal ?OTHEROBJ ?OBJ))))))
- if proc1 避免 proc2 的 發生,
- then for all time,place holds: if there exists proc1 inst1 so that inst1 位於 place timea(之中) time, then there exists proc2 inst2 so that inst2 位於 place timea(之中) time
.
(=>
(prevents ?PROC1 ?PROC2)
(forall
(?TIME ?PLACE)
(=>
(holdsDuring
?TIME
(exists
(?INST1)
(and
(instance ?INST1 ?PROC1)
(located ?INST1 ?PLACE))))
(not
(holdsDuring
?TIME
(exists
(?INST2)
(and
(instance ?INST2 ?PROC2)
(located ?INST2 ?PLACE))))))))
If "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 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 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 int1 是 整數 的 實例 and int2 是 整數 的 實例, then int1 小於 int2 or int2 小於 "(int1+1)".
(=>
(and
(instance ?INT1 Integer)
(instance ?INT2 Integer))
(not
(and
(lessThan ?INT1 ?INT2)
(lessThan
?INT2
(SuccessorFn ?INT1)))))
If int1 是 整數 的 實例 and int2 是 整數 的 實例, then int2 小於 int1 or "(int1+2)" 小於 int2.
(=>
(and
(instance ?INT1 Integer)
(instance ?INT2 Integer))
(not
(and
(lessThan ?INT2 ?INT1)
(lessThan
(PredecessorFn ?INT1)
?INT2))))
There doesn't exist element so that element 是 空集合 的 元素.
(not
(exists
(?ELEMENT)
(element ?ELEMENT NullSet)))
- if class 是 互斥類 的 實例,
- then for all inst1,inst2 holds: if inst1 是 class 的 實例 and inst2 是 inst1 的 實例, then there exists class inst3 so that inst2 是 inst3 的 實例
.
(=>
(instance ?CLASS MutuallyDisjointClass)
(forall
(?INST1 ?INST2)
(=>
(and
(instance ?INST1 ?CLASS)
(instance ?INST2 ?INST1))
(exists
(?INST3)
(and
(instance ?INST3 ?CLASS)
(not
(instance ?INST2 ?INST3)))))))
If graph 是 圖 的 實例 and node1 是 圖節點 的 實例 and node2 是 圖節點 的 實例 and node1 是 graph 的 部分 and node2 是 graph 的 部分 and node1 等於 node2, then there exist arc,path so that - arc (沒) 連結not(s) node1 和 node2
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 是 樹狀圖 的 實例, then there doesn't exist 圖迴圈 loop so that loop 是 graph 的 部分.
(=>
(instance ?GRAPH Tree)
(not
(exists
(?LOOP)
(and
(instance ?LOOP GraphLoop)
(graphPart ?LOOP ?GRAPH)))))
- if graph 是 圖路徑 的 實例 and arc 是 圖弧線 的 實例 and arc 是 graph 的 部分,
- then if "arc 的 �_始節點" 等於 node, then there doesn't exist other so that "other 的 �_始節點" 等於 node and other 等於 arc
.
(=>
(and
(instance ?GRAPH GraphPath)
(instance ?ARC GraphArc)
(graphPart ?ARC ?GRAPH))
(=>
(equal
(InitialNodeFn ?ARC)
?NODE)
(not
(exists
(?OTHER)
(and
(equal
(InitialNodeFn ?OTHER)
?NODE)
(not
(equal ?OTHER ?ARC)))))))
- if graph 是 圖路徑 的 實例 and arc 是 圖弧線 的 實例 and arc 是 graph 的 部分,
- then if "arc 的 最終�`點" 等於 node, then there doesn't exist other so that "other 的 最終�`點" 等於 node and other 等於 arc
.
(=>
(and
(instance ?GRAPH GraphPath)
(instance ?ARC GraphArc)
(graphPart ?ARC ?GRAPH))
(=>
(equal
(TerminalNodeFn ?ARC)
?NODE)
(not
(exists
(?OTHER)
(and
(equal
(TerminalNodeFn ?OTHER)
?NODE)
(not
(equal ?OTHER ?ARC)))))))
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 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)))
There don't exist 劃分 graph 為 兩 獨立 圖表 的 相交路�| path1,劃分 graph 為 兩 獨立 圖表 的 最小相交路�| path2 so that path1 的 路�|長 是 number1 and path2 的 路�|長 是 number2 and number1 小於 number2.
(not
(exists
(?PATH1 ?PATH2)
(and
(instance
?PATH1
(CutSetFn ?GRAPH))
(instance
?PATH2
(MinimalCutSetFn ?GRAPH))
(pathLength ?PATH1 ?NUMBER1)
(pathLength ?PATH2 ?NUMBER2)
(lessThan ?NUMBER1 ?NUMBER2))))
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))))
- 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 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 "月份 二月" 等於 month and year 是 閏年 的 實例, then month 的 持續 是 " 日計(s)".
(=>
(and
(equal
(MonthFn February ?YEAR)
?MONTH)
(not
(instance ?YEAR LeapYear)))
(duration
?MONTH
(MeasureFn 28 DayDuration)))
- 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))))))
obj1 連結 obj2 和 obj3 if and only if obj1 與 obj2 相連 and obj1 與 obj3 相連 and obj2 與 obj3 相連.
(<=>
(connects ?OBJ1 ?OBJ2 ?OBJ3)
(and
(connected ?OBJ1 ?OBJ2)
(connected ?OBJ1 ?OBJ3)
(not
(connected ?OBJ2 ?OBJ3))))
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)))
obj1 (沒) 與 obj2 部分 重�|s if and only if - obj1 是 obj2 的 部分)
and - obj2 是 obj1 的 部分)
and - there exists obj3 so that obj3 是 obj1 的 部分) and obj3 是 obj2 的 部分)
.
(<=>
(overlapsPartially ?OBJ1 ?OBJ2)
(and
(not
(part ?OBJ1 ?OBJ2))
(not
(part ?OBJ2 ?OBJ1))
(exists
(?OBJ3)
(and
(part ?OBJ3 ?OBJ1)
(part ?OBJ3 ?OBJ2)))))
If obj1 是 obj2的 �~表部分, then obj1 是 obj2 的 一 內部 and there doesn't exist obj3 so that obj3 是 obj1 的 一 內部.
(=>
(superficialPart ?OBJ1 ?OBJ2)
(and
(not
(interiorPart ?OBJ1 ?OBJ2))
(not
(exists
(?OBJ3)
(interiorPart ?OBJ3 ?OBJ1)))))
- if obj1 是 obj2 的 一 內部,
- then for all part holds: if part 是 obj2的 �~表部分, then obj1 not(沒) 與 part 重�|
.
(=>
(interiorPart ?OBJ1 ?OBJ2)
(forall
(?PART)
(=>
(superficialPart ?PART ?OBJ2)
(not
(overlapsSpatially ?OBJ1 ?PART)))))
If object 的 底部 是 bottom and part 是 object 的 部分) and part 與 bottom 相連, then part 對 bottom 是 在...之上.
(=>
(and
(bottom ?BOTTOM ?OBJECT)
(part ?PART ?OBJECT)
(not
(connected ?PART ?BOTTOM)))
(orientation ?PART ?BOTTOM Above))
If object 的 頂端 是 top and part 是 object 的 部分) and part 與 top 相連, then part 對 top 是 在...之下.
(=>
(and
(top ?TOP ?OBJECT)
(part ?PART ?OBJECT)
(not
(connected ?PART ?TOP)))
(orientation ?PART ?TOP Below))
If object 的 側面 是 side and part 是 object 的 部分) and part 與 side 相連, then there exists direct so that side 對 part 是 direct.
(=>
(and
(side ?SIDE ?OBJECT)
(part ?PART ?OBJECT)
(not
(connected ?PART ?SIDE)))
(exists
(?DIRECT)
(orientation ?SIDE ?PART ?DIRECT)))
If obj3 等於 "obj1 和 obj2 的 差異", then for all part holds: part 是 obj3 的 部分) if and only if part 是 obj1 的 部分) and part 是 obj2 的 部分).
(=>
(equal
?OBJ3
(MereologicalDifferenceFn ?OBJ1 ?OBJ2))
(forall
(?PART)
(<=>
(part ?PART ?OBJ3)
(and
(part ?PART ?OBJ1)
(not
(part ?PART ?OBJ2))))))
If hole 在 obj 是 �}, then obj 是 洞 的 實例.
(=>
(hole ?HOLE ?OBJ)
(not
(instance ?OBJ Hole)))
If hole 在 obj 是 �}, then hole not(沒) 與 obj 重�|.
(=>
(hole ?HOLE ?OBJ)
(not
(overlapsSpatially ?HOLE ?OBJ)))
If hole1 是 洞 的 實例 and hole2 是 hole1 的 正部分, then there exists obj so that hole1 (沒) 接觸s obj and hole2 not(沒) 接觸 obj.
(=>
(and
(instance ?HOLE1 Hole)
(properPart ?HOLE2 ?HOLE1))
(exists
(?OBJ)
(and
(meetsSpatially ?HOLE1 ?OBJ)
(not
(meetsSpatially ?HOLE2 ?OBJ)))))
If obj1 (沒) 填充s hole and 可填充的 是 obj2 的 屬性, then obj1 not(沒) 與 obj2 重�|.
(=>
(and
(fills ?OBJ1 ?HOLE)
(attribute ?OBJ2 Fillable))
(not
(overlapsSpatially ?OBJ1 ?OBJ2)))
If rep 是 有性生殖 的 實例 and organism 是 rep 的 結果, then there don't exist mother,father so that mother 是 organism 的 母親 and father 是 organism 的 父親.
(=>
(and
(instance ?REP SexualReproduction)
(result ?REP ?ORGANISM))
(not
(exists
(?MOTHER ?FATHER)
(and
(mother ?ORGANISM ?MOTHER)
(father ?ORGANISM ?FATHER)))))
If rep 是 無性生殖 的 實例 and organism 是 rep 的 結果, then there don't exist parent1,parent2 so that parent1 是 organism 的 雙親 and parent2 是 organism 的 雙親 and parent1 等於 parent2.
(=>
(and
(instance ?REP AsexualReproduction)
(result ?REP ?ORGANISM))
(not
(exists
(?PARENT1 ?PARENT2)
(and
(parent ?ORGANISM ?PARENT1)
(parent ?ORGANISM ?PARENT2)
(not
(equal ?PARENT1 ?PARENT2))))))
If leave 是 脫離組織 的 實例 and org 是 組織 的 實例 and leave 是 org 的 施事者 and person 是 leave 的 受事者, then person 是 org的 成員 ""leave 存在 的 時間" 不久 之後"a(之中) "leave 存在 的 時間" 不久 之後.
(=>
(and
(instance ?LEAVE LeavingAnOrganization)
(instance ?ORG Organization)
(agent ?LEAVE ?ORG)
(patient ?LEAVE ?PERSON))
(holdsDuring
(ImmediateFutureFn
(WhenFn ?LEAVE))
(not
(member ?PERSON ?ORG))))
If fire 是 解僱 的 實例 and org 是 組織 的 實例 and fire 是 org 的 施事者 and person 是 fire 的 受事者, then org not(沒) 雇用(s) person ""fire 存在 的 時間" 不久 之後"a(之中) "fire 存在 的 時間" 不久 之後.
(=>
(and
(instance ?FIRE TerminatingEmployment)
(instance ?ORG Organization)
(agent ?FIRE ?ORG)
(patient ?FIRE ?PERSON))
(holdsDuring
(ImmediateFutureFn
(WhenFn ?FIRE))
(not
(employs ?ORG ?PERSON))))
- if
- 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 proc 是 方向的改變 的 實例, then there exists 方向屬性 attr so that - proc 以 方式 attr 執行 ""proc 存在 的 時間" 不久 之前"a(之中) "proc 存在 的 時間" 不久 之前 and proc 以 方式 attr 執行 ""proc 存在 的 時間" 不久 之後"a(之中) "proc 存在 的 時間" 不久 之後
or - proc 以 方式 attr 執行 ""proc 存在 的 時間" 不久 之後"a(之中) "proc 存在 的 時間" 不久 之後 and proc 以 方式 attr 執行 ""proc 存在 的 時間" 不久 之前"a(之中) "proc 存在 的 時間" 不久 之前
.
(=>
(instance ?PROC DirectionChange)
(exists
(?ATTR)
(and
(instance ?ATTR DirectionalAttribute)
(or
(and
(holdsDuring
(ImmediatePastFn
(WhenFn ?PROC))
(manner ?PROC ?ATTR))
(holdsDuring
(ImmediateFutureFn
(WhenFn ?PROC))
(not
(manner ?PROC ?ATTR))))
(and
(holdsDuring
(ImmediateFutureFn
(WhenFn ?PROC))
(manner ?PROC ?ATTR))
(holdsDuring
(ImmediatePastFn
(WhenFn ?PROC))
(not
(manner ?PROC ?ATTR))))))))
If transfer 是 轉移或轉換 的 實例 and transfer 是 agent 的 施事者 and patient 是 transfer 的 受事者, then agent 等於 patient.
(=>
(and
(instance ?TRANSFER Transfer)
(agent ?TRANSFER ?AGENT)
(patient ?TRANSFER ?PATIENT))
(not
(equal ?AGENT ?PATIENT)))
If remove 是 移除 的 實例 and remove (不) �_源s 於 place and obj 是 remove 的 受事者, then obj 位於 place ""remove 存在 的 時間" 不久 之前"a(之中) "remove 存在 的 時間" 不久 之前 and obj 位於 place ""remove 存在 的 時間" 不久 之後"a(之中) "remove 存在 的 時間" 不久 之後.
(=>
(and
(instance ?REMOVE Removing)
(origin ?REMOVE ?PLACE)
(patient ?REMOVE ?OBJ))
(and
(holdsDuring
(ImmediatePastFn
(WhenFn ?REMOVE))
(located ?OBJ ?PLACE))
(holdsDuring
(ImmediateFutureFn
(WhenFn ?REMOVE))
(not
(located ?OBJ ?PLACE)))))
If put 是 放置 的 實例 and put (不) 終結not(s) place and obj 是 put 的 受事者, then obj 位於 place ""put 存在 的 時間" 不久 之前"a(之中) "put 存在 的 時間" 不久 之前 and obj 位於 place ""put 存在 的 時間" 不久 之後"a(之中) "put 存在 的 時間" 不久 之後.
(=>
(and
(instance ?PUT Putting)
(destination ?PUT ?PLACE)
(patient ?PUT ?OBJ))
(and
(holdsDuring
(ImmediatePastFn
(WhenFn ?PUT))
(not
(located ?OBJ ?PLACE)))
(holdsDuring
(ImmediateFutureFn
(WhenFn ?PUT))
(located ?OBJ ?PLACE))))
If sub 是 替換 的 實例, then there exist 放置 put,移除 remove,obj1,obj2,place so that put 是 sub 的 次歷�{ and remove 是 sub 的 次歷�{ and obj1 是 remove 的 受事者 and remove (不) �_源s 於 place and obj2 是 put 的 受事者 and put (不) 終結not(s) place and obj1 等於 obj2.
(=>
(instance ?SUB Substituting)
(exists
(?PUT ?REMOVE ?OBJ1 ?OBJ2 ?PLACE)
(and
(instance ?PUT Putting)
(instance ?REMOVE Removing)
(subProcess ?PUT ?SUB)
(subProcess ?REMOVE ?SUB)
(patient ?REMOVE ?OBJ1)
(origin ?REMOVE ?PLACE)
(patient ?PUT ?OBJ2)
(destination ?PUT ?PLACE)
(not
(equal ?OBJ1 ?OBJ2)))))
If 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 give 是 單方面的給與 的 實例, then there doesn't exist 交易 trans so that give 是 trans 的 次歷�{.
(=>
(instance ?GIVE UnilateralGiving)
(not
(exists
(?TRANS)
(and
(instance ?TRANS Transaction)
(subProcess ?GIVE ?TRANS)))))
If get 是 單方面的獲取 的 實例, then there doesn't exist 交易 trans so that get 是 trans 的 次歷�{.
(=>
(instance ?GET UnilateralGetting)
(not
(exists
(?TRANS)
(and
(instance ?TRANS Transaction)
(subProcess ?GET ?TRANS)))))
If trans 是 交易 的 實例, then there exist agent1,agent2,給與 give1,給與 give2,obj1,obj2 so that give1 是 trans 的 次歷�{ and give2 是 trans 的 次歷�{ and give1 是 agent1 的 施事者 and give2 是 agent2 的 施事者 and obj1 是 give1 的 受事者 and obj2 是 give2 的 受事者 and give1 (不) 終結not(s) agent2 and give2 (不) 終結not(s) agent1 and agent1 等於 agent2 and obj1 等於 obj2.
(=>
(instance ?TRANS Transaction)
(exists
(?AGENT1 ?AGENT2 ?GIVE1 ?GIVE2 ?OBJ1 ?OBJ2)
(and
(instance ?GIVE1 Giving)
(instance ?GIVE2 Giving)
(subProcess ?GIVE1 ?TRANS)
(subProcess ?GIVE2 ?TRANS)
(agent ?GIVE1 ?AGENT1)
(agent ?GIVE2 ?AGENT2)
(patient ?GIVE1 ?OBJ1)
(patient ?GIVE2 ?OBJ2)
(destination ?GIVE1 ?AGENT2)
(destination ?GIVE2 ?AGENT1)
(not
(equal ?AGENT1 ?AGENT2))
(not
(equal ?OBJ1 ?OBJ2)))))
If confine 是 限定 的 實例 and person 是 confine 的 受事者, then person not(不) 冀求(s) "person 是 confine 的 受事者".
(=>
(and
(instance ?CONFINE Confining)
(patient ?CONFINE ?PERSON))
(not
(desires
?PERSON
(patient ?CONFINE ?PERSON))))
process 是 毀滅 的 實例 if and only if there exists patient so that patient 是 process 的 受事者 and patient (不) 存在s ""process 存在 的 時間" 不久 之前" 期間 and patient not(不) 存在 ""process 存在 的 時間" 不久 之後" 期間.
(<=>
(instance ?PROCESS Destruction)
(exists
(?PATIENT)
(and
(patient ?PROCESS ?PATIENT)
(time
?PATIENT
(ImmediatePastFn
(WhenFn ?PROCESS)))
(not
(time
?PATIENT
(ImmediateFutureFn
(WhenFn ?PROCESS)))))))
If attach 是 貼附 的 實例 and obj1 是 attach 的 受事者 and obj2 是 attach 的 受事者, then obj1 與 obj2 相連 ""attach 存在 的 時間" 不久 之前"a(之中) "attach 存在 的 時間" 不久 之前 and obj1 與 obj2 相連 ""attach 存在 的 時間" 不久 之後"a(之中) "attach 存在 的 時間" 不久 之後.
(=>
(and
(instance ?ATTACH Attaching)
(patient ?ATTACH ?OBJ1)
(patient ?ATTACH ?OBJ2))
(and
(holdsDuring
(ImmediatePastFn
(WhenFn ?ATTACH))
(not
(connected ?OBJ1 ?OBJ2)))
(holdsDuring
(ImmediateFutureFn
(WhenFn ?ATTACH))
(connected ?OBJ1 ?OBJ2))))
If detach 是 脫離 的 實例 and obj1 是 detach 的 受事者 and obj2 是 detach 的 受事者, then obj1 與 obj2 相連 ""detach 存在 的 時間" 不久 之前"a(之中) "detach 存在 的 時間" 不久 之前 and obj1 與 obj2 相連 ""detach 存在 的 時間" 不久 之後"a(之中) "detach 存在 的 時間" 不久 之後.
(=>
(and
(instance ?DETACH Detaching)
(patient ?DETACH ?OBJ1)
(patient ?DETACH ?OBJ2))
(and
(holdsDuring
(ImmediatePastFn
(WhenFn ?DETACH))
(connected ?OBJ1 ?OBJ2))
(holdsDuring
(ImmediateFutureFn
(WhenFn ?DETACH))
(not
(connected ?OBJ1 ?OBJ2)))))
combine 是 結合 的 實例 and obj1 對 combine 是 資源 and obj2 是 combine 的 結果 if and only if obj1 是 obj2 的 部分) ""combine 存在 的 時間" 不久 之前"a(之中) "combine 存在 的 時間" 不久 之前 and obj1 是 obj2 的 部分) ""combine 存在 的 時間" 不久 之後"a(之中) "combine 存在 的 時間" 不久 之後.
(<=>
(and
(instance ?COMBINE Combining)
(resource ?COMBINE ?OBJ1)
(result ?COMBINE ?OBJ2))
(and
(holdsDuring
(ImmediatePastFn
(WhenFn ?COMBINE))
(not
(part ?OBJ1 ?OBJ2)))
(holdsDuring
(ImmediateFutureFn
(WhenFn ?COMBINE))
(part ?OBJ1 ?OBJ2))))
compound 是 化合物 的 實例 if and only if there exist 基本物質 element1,基本物質 element2,化學合成 process so that element1 等於 element2 and element1 對 process 是 資源 and element2 對 process 是 資源 and compound 是 process 的 結果.
(<=>
(instance ?COMPOUND CompoundSubstance)
(exists
(?ELEMENT1 ?ELEMENT2 ?PROCESS)
(and
(instance ?ELEMENT1 ElementalSubstance)
(instance ?ELEMENT2 ElementalSubstance)
(not
(equal ?ELEMENT1 ?ELEMENT2))
(instance ?PROCESS ChemicalSynthesis)
(resource ?PROCESS ?ELEMENT1)
(resource ?PROCESS ?ELEMENT2)
(result ?PROCESS ?COMPOUND))))
If change 是 內在改變 的 實例 and obj 是 change 的 受事者, then there exists property so that - property 是 obj 的 屬性 ""change 存在 的 時間" 不久 之前"a(之中) "change 存在 的 時間" 不久 之前 and property 是 obj 的 屬性 ""change 存在 的 時間" 不久 之後"a(之中) "change 存在 的 時間" 不久 之後
or - property 是 obj 的 屬性 ""change 存在 的 時間" 不久 之前"a(之中) "change 存在 的 時間" 不久 之前 and property 是 obj 的 屬性 ""change 存在 的 時間" 不久 之後"a(之中) "change 存在 的 時間" 不久 之後
.
(=>
(and
(instance ?CHANGE InternalChange)
(patient ?CHANGE ?OBJ))
(exists
(?PROPERTY)
(or
(and
(holdsDuring
(ImmediatePastFn
(WhenFn ?CHANGE))
(attribute ?OBJ ?PROPERTY))
(holdsDuring
(ImmediateFutureFn
(WhenFn ?CHANGE))
(not
(attribute ?OBJ ?PROPERTY))))
(and
(holdsDuring
(ImmediatePastFn
(WhenFn ?CHANGE))
(not
(attribute ?OBJ ?PROPERTY)))
(holdsDuring
(ImmediateFutureFn
(WhenFn ?CHANGE))
(attribute ?OBJ ?PROPERTY))))))
If alt 是 表面改變 的 實例 and obj 是 alt 的 受事者, then there exist part,property so that part 是 obj的 �~表部分 and property 是 part 的 屬性 ""alt 存在 的 時間" 不久 之前"a(之中) "alt 存在 的 時間" 不久 之前 and property 是 part 的 屬性 ""alt 存在 的 時間" 不久 之後"a(之中) "alt 存在 的 時間" 不久 之後.
(=>
(and
(instance ?ALT SurfaceChange)
(patient ?ALT ?OBJ))
(exists
(?PART ?PROPERTY)
(and
(superficialPart ?PART ?OBJ)
(holdsDuring
(ImmediatePastFn
(WhenFn ?ALT))
(attribute ?PART ?PROPERTY))
(holdsDuring
(ImmediateFutureFn
(WhenFn ?ALT))
(not
(attribute ?PART ?PROPERTY))))))
If alt 是 形狀改變 的 實例 and obj 是 alt 的 受事者, then there exists 形狀屬性 property so that - property 是 obj 的 屬性 ""alt 存在 的 時間" 不久 之前"a(之中) "alt 存在 的 時間" 不久 之前 and property 是 obj 的 屬性 ""alt 存在 的 時間" 不久 之後"a(之中) "alt 存在 的 時間" 不久 之後
or - property 是 obj 的 屬性 ""alt 存在 的 時間" 不久 之前"a(之中) "alt 存在 的 時間" 不久 之前 and property 是 obj 的 屬性 ""alt 存在 的 時間" 不久 之後"a(之中) "alt 存在 的 時間" 不久 之後
.
(=>
(and
(instance ?ALT ShapeChange)
(patient ?ALT ?OBJ))
(exists
(?PROPERTY)
(and
(instance ?PROPERTY ShapeAttribute)
(or
(and
(holdsDuring
(ImmediatePastFn
(WhenFn ?ALT))
(attribute ?OBJ ?PROPERTY))
(holdsDuring
(ImmediateFutureFn
(WhenFn ?ALT))
(not
(attribute ?OBJ ?PROPERTY))))
(and
(holdsDuring
(ImmediatePastFn
(WhenFn ?ALT))
(not
(attribute ?OBJ ?PROPERTY)))
(holdsDuring
(ImmediateFutureFn
(WhenFn ?ALT))
(attribute ?OBJ ?PROPERTY)))))))
If coloring 是 著色 的 實例 and obj 是 coloring 的 受事者, then there exists 顏色屬性 property so that property 是 obj 的 屬性 ""coloring 存在 的 時間" 不久 之前"a(之中) "coloring 存在 的 時間" 不久 之前 and property 是 obj 的 屬性 ""coloring 存在 的 時間" 不久 之後"a(之中) "coloring 存在 的 時間" 不久 之後.
(=>
(and
(instance ?COLORING Coloring)
(patient ?COLORING ?OBJ))
(exists
(?PROPERTY)
(and
(instance ?PROPERTY ColorAttribute)
(holdsDuring
(ImmediatePastFn
(WhenFn ?COLORING))
(attribute ?OBJ ?PROPERTY))
(holdsDuring
(ImmediateFutureFn
(WhenFn ?COLORING))
(not
(attribute ?OBJ ?PROPERTY))))))
process 是 產生 的 實例 if and only if there exists patient so that patient 是 process 的 受事者 and patient (不) 存在s ""process 存在 的 時間" 不久 之後" 期間 and patient not(不) 存在 ""process 存在 的 時間" 不久 之前" 期間.
(<=>
(instance ?PROCESS Creation)
(exists
(?PATIENT)
(and
(patient ?PROCESS ?PATIENT)
(time
?PATIENT
(ImmediateFutureFn
(WhenFn ?PROCESS)))
(not
(time
?PATIENT
(ImmediatePastFn
(WhenFn ?PROCESS)))))))
If pursue 是 追 的 實例 and pursue 是 agent 的 施事者 and obj 是 pursue 的 受事者, then agent not(沒) 擁有(s) obj pursuea(之中) pursue.
(=>
(and
(instance ?PURSUE Pursuing)
(agent ?PURSUE ?AGENT)
(patient ?PURSUE ?OBJ))
(holdsDuring
?PURSUE
(not
(possesses ?AGENT ?OBJ))))
If investigate 是 調查 的 實例 and investigate 是 agent 的 施事者 and prop 是 investigate 的 受事者, then agent not(不）知道 "investigate 存在 的 時間"a(之中) investigate 存在 的 時間.
(=>
(and
(instance ?INVESTIGATE Investigating)
(agent ?INVESTIGATE ?AGENT)
(patient ?INVESTIGATE ?PROP))
(holdsDuring
(WhenFn ?INVESTIGATE)
(not
(knows ?AGENT ?PROP))))
If 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 question 是 詢問 的 實例 and question 是 agent 的 施事者 and formula 是 question 的 受事者 and formula 是 SUO-KIF表述式 的 實例, then agent not(不）知道 "question 存在 的 時間"a(之中) question 存在 的 時間.
(=>
(and
(instance ?QUESTION Questioning)
(agent ?QUESTION ?AGENT)
(patient ?QUESTION ?FORMULA)
(instance ?FORMULA Formula))
(holdsDuring
(WhenFn ?QUESTION)
(not
(knows ?AGENT ?FORMULA))))
If 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 island 是 島嶼 的 實例, then there don't exist 陸地 area,part1,part2 so that part1 是 island 的 部分) and part2 是 area 的 部分) and island 是 area 的 部分) and area 是 island 的 部分) and part1 與 part2 相連.
(=>
(instance ?ISLAND Island)
(not
(exists
(?AREA ?PART1 ?PART2)
(and
(instance ?AREA LandArea)
(part ?PART1 ?ISLAND)
(part ?PART2 ?AREA)
(not
(part ?ISLAND ?AREA))
(not
(part ?AREA ?ISLAND))
(connected ?PART1 ?PART2)))))
If part 是 軀體部件 的 實例, then there doesn't exist 病理歷程 proc so that part 是 proc 的 結果.
(=>
(instance ?PART BodyPart)
(not
(exists
(?PROC)
(and
(instance ?PROC PathologicProcess)
(result ?PROC ?PART)))))
If 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 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 comp1 與 comp2 連結, then comp1 是 comp2 的 元件 and comp2 是 comp1 的 元件.
(=>
(connectedEngineeringComponents ?COMP1 ?COMP2)
(and
(not
(engineeringSubcomponent ?COMP1 ?COMP2))
(not
(engineeringSubcomponent ?COMP2 ?COMP1))))
If comp1 與 comp2 連結, then comp1 是 工程連結元件 的 實例 and comp2 是 工程連結元件 的 實例.
(=>
(connectedEngineeringComponents ?COMP1 ?COMP2)
(not
(or
(instance ?COMP1 EngineeringConnection)
(instance ?COMP2 EngineeringConnection))))
If 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 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 obj1 對 obj2 是 在...之上, then obj1 與 obj2 相連.
(=>
(orientation ?OBJ1 ?OBJ2 Above)
(not
(connected ?OBJ1 ?OBJ2)))
If obj1 對 obj2 是 接近, then obj1 與 obj2 相連.
(=>
(orientation ?OBJ1 ?OBJ2 Near)
(not
(connected ?OBJ1 ?OBJ2)))
If obj1 對 obj2 是 在...上, then obj2 對 obj1 是 not 在...上.
(=>
(orientation ?OBJ1 ?OBJ2 On)
(not
(orientation ?OBJ2 ?OBJ1 On)))
For all org holds: org not(沒) 雇用(s) person and person 是 人類 的 實例 if and only if 失業的 是 person 的 屬性.
(<=>
(forall
(?ORG)
(and
(not
(employs ?ORG ?PERSON))
(instance ?PERSON Human)))
(attribute ?PERSON Unemployed))
陳述 formula 有 必要性 的 型態意義 if and only if 陳述 "formula" 有 可能性 的 型態意義.
(<=>
(modalAttribute ?FORMULA Necessity)
(not
(modalAttribute
(not ?FORMULA)
Possibility)))
陳述 formula 有 義務 的 型態意義 if and only if 陳述 "formula" 有 許可 的 型態意義.
(<=>
(modalAttribute ?FORMULA Obligation)
(not
(modalAttribute
(not ?FORMULA)
Permission)))
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 乾的 是 obj 的 屬性, then there doesn't exist subobj so that subobj 是 obj 的 部分) and 液體的 是 subobj 的 屬性.
(=>
(attribute ?OBJ Dry)
(not
(exists
(?SUBOBJ)
(and
(part ?SUBOBJ ?OBJ)
(attribute ?SUBOBJ Liquid)))))
If 不易碎的 是 obj 的 屬性, then there doesn't exist 損害 damage so that obj 是 damage 的 受事者.
(=>
(attribute ?OBJ Unbreakable)
(not
(exists
(?DAMAGE)
(and
(instance ?DAMAGE Damaging)
(patient ?DAMAGE ?OBJ)))))
If 胚胎的 是 org 的 屬性 timea(之中) time, then there doesn't exist 誕生 birth so that org (沒) 體驗not(s) birth timea(之中) time.
(=>
(holdsDuring
?TIME
(attribute ?ORG Embryonic))
(holdsDuring
?TIME
(not
(exists
(?BIRTH)
(and
(instance ?BIRTH Birth)
(experiencer ?BIRTH ?ORG))))))
entity 是 "class 的 互補" 的 實例 if and only if entity 是 class 的 實例.
(<=>
(instance
?ENTITY
(ComplementFn ?CLASS))
(not
(instance ?ENTITY ?CLASS)))
