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.

Ontology

SUMO / STRUCTURAL-ONTOLOGY

Class(es)

class

inheritable relation

ternary predicate

domain

Coordinate term(s)

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

Type restrictions

domain(relation, positive integer, set or class)

Axioms (13)

If pred1 is a subrelation of pred2 and the number number argument of pred2 is an instance of class1, then the number number argument of pred1 is an instance of class1.

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

If the number number argument of rel is an instance of class1 and the number number argument of rel is an instance of class2, then class1 is a subclass of class2 or class2 is a subclass of class1.

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

If the number number argument of rel1 is an instance of class1 and the number number argument of rel2 is an instance of class2 and class1 is disjoint from class2, then rel1 and rel2 are disjoint.

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

If function is an instance of unary constant functionquantity, then the number argument of function is an instance of constant quantity and range of function is an instance of constant quantity.

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

If function is an instance of time dependent quantity, then the number argument of function is an instance of time measure.

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

rel is an instance of total valued relation if and only if there exists valence so that rel is an instance of relation and rel %&has valence argument(s) and

if for all number,element,class holds: if number is less than valence and the number number argument of rel is an instance of class and element is equal to "numberth element of "()"", then element is an instance of class,
then there exists item so that 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))))))

rel is an instance of binary relation
the number argument of rel is an instance of class1 or the number argument of rel is a subclass of class1
the number argument of rel is an instance of class2 or the number argument of rel is a subclass of class2 or range of rel is an instance of class2 or the values returned by rel are subclasses of class2
class1 is disjoint from class2

, then rel is an instance of asymmetric relation.

(=>
      (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 the number number argument of rel is an instance of class and rel() holds, then "numberth element of "()"" is an instance of class.

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

if fun is an instance of one to one function,
then for all arg1,arg2 holds: if the number argument of fun is an instance of class and arg1 is an instance of class and arg2 is an instance of class and arg1 is not equal to arg2, then "fun(arg1)" is not equal to "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 is an instance of associative function,
then for all inst1,inst2,inst3 holds: if the number argument of function is an instance of class and inst1 is an instance of class and inst2 is an instance of class and inst3 is an instance of class, then "function(inst1,"function(inst2,inst3)")" is equal to "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 is an instance of commutative function,
then for all inst1,inst2 holds: if the number argument of function is an instance of class and inst1 is an instance of class and inst2 is an instance of class, then "function(inst1,inst2)" is equal to "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 is distributive over function2,
then for all inst1,inst2,inst3 holds: if the number argument of function1 is an instance of class1 and inst1 is an instance of class1 and inst2 is an instance of class1 and inst3 is an instance of class1 and the number argument of function2 is an instance of class2 and inst1 is an instance of class2 and inst2 is an instance of class2 and inst3 is an instance of class2, then "function1(inst1,"function2(inst2,inst3)")" is equal to "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 is an identity element of function,
then for all inst holds: if the number argument of function is an instance of class and inst is an instance of class, then "function(id,inst)" is equal to inst

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