Function EXACT-DOMAIN

Slots on this function:

Documentation:
The EXACT-DOMAIN of a relation is a relation whose tuples (all of them) are mapped by the relation to instances of the range. A binary relation R is defined as a set of tuples of form . If we say (= (exact-domain R) D) then all of the x's must be in the class D, and for each instance x of class D, the relation maps x to some y. The exact-domain of a relation of arity other than 2 is the relation that represents a cross product. For example, the notation F:A x B -> C, means that function F maps pairs onto c's where a is an instance of A, b is an instance of B, and c is an instance of C. The exact-domain of F is the set of pairs that occur in some triple in F. Some treatments of functions define a function as a mapping from a domain to a range. This ontology treats functions as relations, and relations as sets of tuples. Thus, functions and relations are not defined relative to domains and ranges; the exact-domain is a function of the set of tuples. It follows that all functions are `total' with respect to their exact-domains and `onto' with respect to their exact-ranges. The exact-domain of a variable-arity relation is another variable-arity relation; the lengths of the tuples in the exact-domain of R is one less than the corresponding tuples in the relation R. The exact-domain of a unary relation, or a relation that contains a tuple of length one, is undefined.
Instance-Of: Function
Arity: 2
Domain: Relation
Range: Relation

Equivalence Axioms:

(<=> (Exact-Domain ?Relation)
     (And (Relation ?Relation)
          (Relation ?Domain-Relation)
          (Forall (?Tuple)
                  (=> (Member ?Tuple ?Relation)
                      (Not (Empty (Butlast ?Tuple)))))
          (Forall (?Tuple @Args)
                  (<=> (Holds ?Domain-Relation @Args)
                       (And (Member ?Tuple ?Relation)
                            (= (Listof @Args) (Butlast ?Tuple)))))))

Other Related Axioms:

(=> (Exact-Domain $X $Y) (Relation $Y))

(=> (Exact-Domain $X $Y) (Relation $X))

(=> (= (Exact-Domain ?Relation) ?Domain-Relation)
    (Forall (?Tuple @Args)
            (<=> (Holds ?Domain-Relation @Args)
                 (And (Member ?Tuple ?Relation)
                      (= (Listof @Args) (Butlast ?Tuple))))))

(=> (= (Exact-Domain ?Relation) ?Domain-Relation)
    (Forall (?Tuple)
            (=> (Member ?Tuple ?Relation)
                (Not (Empty (Butlast ?Tuple))))))

(=> (= (Exact-Domain ?Relation) ?Domain-Relation)
    (Relation ?Domain-Relation))

(=> (= (Exact-Domain ?Relation) ?Domain-Relation)
    (Relation ?Relation))

(<=> (Total-On ?Relation ?Domain-Relation)
     (Subrelation-Of (Exact-Domain ?Relation) ?Domain-Relation))

(<=> (Domain ?Relation ?Restriction)
     (And (Binary-Relation ?Relation)
          (Class ?Restriction)
          (Subclass-Of (Exact-Domain ?Relation) ?Restriction)))

(=> (Instance-Of ?X (Exact-Domain ?R)) (Holds ?R ?X ?X))

(<=> (Reflexive-Relation ?R)
     (And (Binary-Relation ?R)
          (=> (Instance-Of ?X (Exact-Domain ?R)) (Holds ?R ?X ?X))))

(=> (And (Instance-Of ?X (Exact-Domain ?R))
         (Instance-Of ?Y (Exact-Domain ?R)))
    (Or (Holds ?R ?X ?Y) (Holds ?R ?Y ?X)))

(<=> (Total-Order-Relation ?R)
     (And (Partial-Order-Relation ?R)
          (=> (And (Instance-Of ?X (Exact-Domain ?R))
                   (Instance-Of ?Y (Exact-Domain ?R)))
              (Or (Holds ?R ?X ?Y) (Holds ?R ?Y ?X)))))

Notes: