Function Relation-Universe

• Defined in ontology: Frame-ontology
• Source pathname: /tmp_mnt/vol/q/htw/cms/ontolingua/examples/ontolingua/../../all-ontologies/ontolingua/frame-ontology.lisp

Arity: 2

Documentation:

A relation-universe of a relation of any arity is a class from which is drawn every item in every tuple of the relation. Like EXACT-DOMAIN, it is exactly those items and no other. Thus, to state that the universe of a relation is covered by some class, one can state that the relation-universe is a subclass of the covering class.

Notes:

• See-Also: universe
• version 4: Added.

Domain: Relation

Instance-Of:

Binary-Relation, Function, Relation, Set

Range: Class

Equivalence Axioms for Relation-Universe:

(<=> (Relation-Universe ?Relation)
     (And (Relation ?Relation)
          (Class ?Type-Class)
          (Forall (?X)
                  (<=> (Exists (?Tuple)
                               (And (Member ?Tuple ?Relation)
                                    (Item ?X ?Tuple)))
                       (Instance-Of ?X ?Type-Class)))))

Implication Axioms mentioning Relation-Universe:

(=> (= (Relation-Universe ?Relation) ?Type-Class)
    (Forall (?X)
            (<=> (Exists (?Tuple)
                         (And (Member ?Tuple ?Relation)
                              (Item ?X ?Tuple)))
                 (Instance-Of ?X ?Type-Class))))

(=> (= (Relation-Universe ?Relation) ?Type-Class)
    (Class ?Type-Class))

(=> (= (Relation-Universe ?Relation) ?Type-Class)
    (Relation ?Relation))