domain (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.

Ontologie

SUMO / STRUCTURAL-ONTOLOGY

Class(es)

třída

inheritable relation

predikát se třemi argumenty

domain

Související termín(y)

altitude between capability conditional probability confers obligation confers right connects depth distance domain subclass has purpose for agent links occupies position orientation prefers related external concept represents for agent represents in language temporally between temporally between or equal

Typy argumentů

domain(relace, kladné celé číslo, množina nebo třída)

Axiomy (13)

Jestliže pred1 je a subrelation of pred2 a numberth argument of pred2 je an instance of class1, potom numberth argument of pred1 je an instance of class1.

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

Jestliže numberth argument of rel je an instance of class1 a numberth argument of rel je an instance of class2, potom class1 je podtřídou class2 nebo class2 je podtřídou class1.

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

Jestliže numberth argument of rel1 je an instance of class1 a numberth argument of rel2 je an instance of class2 a class1 je disjoint from class2, potom rel1 and rel2 are disjoint.

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

Jestliže function je instancí třídy unary constant functionquantity, potom th argument of function je an instance of konstantní veličina a range of function je an instance of konstantní veličina.

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

Jestliže function je instancí třídy časově závislá veličina, potom th argument of function je an instance of časová míra.

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

rel je instancí třídy úplná relace tehdy a jen tehdy pokud existuje valence tak, že rel je instancí třídy relace a rel has valence argument(s) a

jestliže pro všechny number,element,class platí: jestliže number je menší než valence a numberth argument of rel je an instance of class a element se rovná "numberth element of "()"", potom element je instancí třídy class,
potom existuje item tak, že rel(,item) holds

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

Jestliže

rel je instancí třídy binární relace
th argument of rel je an instance of class1 nebo th argument of rel je a subclass of class1
th argument of rel je an instance of class2 nebo th argument of rel je a subclass of class2 nebo range of rel je an instance of class2 nebo range subclass(rel,class2) platí
class1 je disjoint from class2

, potom rel je instancí třídy nesymetrická relace.

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

Jestliže numberth argument of rel je an instance of class a rel() holds, potom "numberth element of "()"" je instancí třídy class.

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

jestliže fun je instancí třídy prostá funkce na,
potom pro všechny arg1,arg2 platí: jestliže th argument of fun je an instance of class a arg1 je instancí třídy class a arg2 je instancí třídy class a arg1 se nerovná arg2, potom "fun(arg1)" se nerovná "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))))))

jestliže function je instancí třídy asociativní funkce,
potom pro všechny inst1,inst2,inst3 platí: jestliže th argument of function je an instance of class a inst1 je instancí třídy class a inst2 je instancí třídy class a inst3 je instancí třídy class, potom "function(inst1,"function(inst2,inst3)")" se rovná "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)))))

jestliže function je instancí třídy komutativní funkce,
potom pro všechny inst1,inst2 platí: jestliže th argument of function je an instance of class a inst1 je instancí třídy class a inst2 je instancí třídy class, potom "function(inst1,inst2)" se rovná "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)))))

jestliže function1 je distributive over function2,
potom pro všechny inst1,inst2,inst3 platí: jestliže th argument of function1 je an instance of class1 a inst1 je instancí třídy class1 a inst2 je instancí třídy class1 a inst3 je instancí třídy class1 a th argument of function2 je an instance of class2 a inst1 je instancí třídy class2 a inst2 je instancí třídy class2 a inst3 je instancí třídy class2, potom "function1(inst1,"function2(inst2,inst3)")" se rovná "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))))))

jestliže id je an identity element of function,
potom pro všechny inst platí: jestliže th argument of function je an instance of class a inst je instancí třídy class, potom "function(id,inst)" se rovná inst

(=>
      (identityElement ?FUNCTION ?ID)
      (forall
            (?INST)
            (=>
                  (and
                        (domain ?FUNCTION 1 ?CLASS)
                        (instance ?INST ?CLASS))
                  (equal
                        (AssignmentFn ?FUNCTION ?ID ?INST)
                        ?INST))))