領域 (domain)

Provides a computationally and heuristically convenient mechanism for declaring the argument types of a given relation. The formula (domain rel int class) means that the int'th element of each tuple in the relation rel must be an instance of class. Specifying argument types is very helpful in maintaining ontologies. Representation systems can use these specifications to classify terms and check integrity constraints. If the restriction on the argument type of a Relation is not captured by a SetOrClass already defined in the ontology, one can specify a SetOrClass compositionally with the functions UnionFn, IntersectionFn, etc.

Ontology

SUMO / STRUCTURAL-ONTOLOGY

Class(es)

種類

可繼承關係

三元述詞

領域

Coordinate term(s)

標高介於能力條件或然率賦予義務賦予權力相連深度距離領域次種類施事者有意圖連結有...職位相對方位偏愛 SUMO外部相關概念施事者呈現以...語言呈現時間介於時間介於或同時

Type restrictions

domain(關係, 正整數, 集合或種類)

Axioms (13)

If pred1 是 pred2 的次關係 and pred2 的論元 number 是 class1 的實例, then pred1 的論元 number 是 class1 的實例.

(=>
      (and
            (subrelation ?PRED1 ?PRED2)
            (domain ?PRED2 ?NUMBER ?CLASS1))
      (domain ?PRED1 ?NUMBER ?CLASS1))

If rel 的論元 number 是 class1 的實例 and rel 的論元 number 是 class2 的實例, then class1 是 class2 的次種類 or class2 是 class1 的次種類.

(=>
      (and
            (domain ?REL ?NUMBER ?CLASS1)
            (domain ?REL ?NUMBER ?CLASS2))
      (or
            (subclass ?CLASS1 ?CLASS2)
            (subclass ?CLASS2 ?CLASS1)))

If rel1 的論元 number 是 class1 的實例 and rel2 的論元 number 是 class2 的實例 and class1 無交集於 class2, then 無交集關係(rel1,rel2) holds.

(=>
      (and
            (domain ?REL1 ?NUMBER ?CLASS1)
            (domain ?REL2 ?NUMBER ?CLASS2)
            (disjoint ?CLASS1 ?CLASS2))
      (disjointRelation ?REL1 ?REL2))

If function 是一元恆定函數量的實例, then function 的論元是常量的實例 and function 的範圍是常量的實例.

(=>
      (instance ?FUNCTION UnaryConstantFunctionQuantity)
      (and
            (domain ?FUNCTION 1 ConstantQuantity)
            (range ?FUNCTION ConstantQuantity)))

If function 是時間依變量的實例, then function 的論元是時間單位的實例.

(=>
      (instance ?FUNCTION TimeDependentQuantity)
      (domain ?FUNCTION 1 TimeMeasure))

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

rel 是二元關係的實例
rel 的論元是 class1 的實例 or rel 的論元是 class1 的次種類
rel 的論元是 class2 的實例 or rel 的論元是 class2 的次種類 or rel 的範圍是 class2 的實例 or 被 rel 歸回的值是 class2的次種類
class1 無交集於 class2

, then rel 是不對稱關係的實例.

(=>
      (and
            (instance ?REL BinaryRelation)
            (or
                  (domain ?REL 1 ?CLASS1)
                  (domainSubclass ?REL 1 ?CLASS1))
            (or
                  (domain ?REL 2 ?CLASS2)
                  (domainSubclass ?REL 2 ?CLASS2)
                  (range ?REL ?CLASS2)
                  (rangeSubclass ?REL ?CLASS2))
            (disjoint ?CLASS1 ?CLASS2))
      (instance ?REL AsymmetricRelation))

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

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

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 分配(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 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))))