成立 (holds)

(holds P N1 ... NK) is true just in case the tuple of objects denoted by N1,..., NK is an element of the Relation P.

Ontology

SUMO / STRUCTURAL-ONTOLOGY

Class(es)

種類

可繼承關係

述詞

變異元數關係

成立

Coordinate term(s)

指定函數最大公約數函數最小公倍數函數序列函數矛盾屬性無交集分解無交集關係窮盡的屬性窮盡的分解分割

Type restrictions

holds(關係)

Axioms (34)

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

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

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

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 無交集關係() 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 rel(,inst) (不) 成立s and rel 是函數的實例, then "rel()" 等於 inst.

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

If rel 是關係的實例, then rel() (不) 成立s if and only if rel() holds.

(=>
      (instance ?REL Relation)
      (<=>
            (holds ?REL @ROW)
            (?REL @ROW)))

rel 是單值關係的實例 if and only if for all ,item1,item2 holds: if rel(,item1) (不) 成立s and rel(,item2) (不) 成立s, then item1 等於 item2.

(<=>
      (instance ?REL SingleValuedRelation)
      (forall
            (@ROW ?ITEM1 ?ITEM2)
            (=>
                  (and
                        (holds ?REL @ROW ?ITEM1)
                        (holds ?REL @ROW ?ITEM2))
                  (equal ?ITEM1 ?ITEM2))))

rel 是全值關係的實例 if and only if there exists valence so that rel 是關係的實例 and rel %&有論元(s) valence and

if for all number,element,class holds: if number 小於 valence and rel 的論元 number 是 class 的實例 and element 等於 ""()" 的第二元素", then element 是 class 的實例,
then there exists item so that rel(,item) (不) 成立s

(<=>
      (instance ?REL TotalValuedRelation)
      (exists
            (?VALENCE)
            (and
                  (instance ?REL Relation)
                  (valence ?REL ?VALENCE)
                  (=>
                        (forall
                              (?NUMBER ?ELEMENT ?CLASS)
                              (=>
                                    (and
                                          (lessThan ?NUMBER ?VALENCE)
                                          (domain ?REL ?NUMBER ?CLASS)
                                          (equal
                                                ?ELEMENT
                                                (ListOrderFn
                                                      (ListFn @ROW)
                                                      ?NUMBER)))
                                    (instance ?ELEMENT ?CLASS)))
                        (exists
                              (?ITEM)
                              (holds ?REL @ROW ?ITEM))))))

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

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

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

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

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

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

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

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

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 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 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 rel 的論元 number 是 class 的實例 and rel() (不) 成立s, then ""()" 的第二元素" 是 class 的實例.

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

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

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

if 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 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 role 是格位角色的實例 and role(arg1,arg2) (不) 成立s and arg1 是 proc 的實例, then arg2 可以任角色 role 做 proc.

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

if 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 rel(inst1,inst2) (不) 成立s intervala(之中) interval and inst1 是物質的的實例 and inst2 是物質的的實例, then inst1 (不) 存在s interval 期間 and inst2 (不) 存在s interval 期間.

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

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

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

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

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