Function PROJECTION

• Defined in theory: Frame-ontology
• Source code: frame-ontology.lisp

Slots on this function:

Documentation:

The projection of an N-ary relation on column i is the class whose instances are the ith items of each tuple in the relation.

Instance-Of: Function

Arity: 3

Equivalence Axioms:

(<=> (Projection ?Relation ?Column)
     (And (Defined (Arity ?Relation))
          (Positive-Integer ?Column)
          (=< ?Column (Arity ?Relation))
          (Class ?Projection-Relation)
          (Forall (?Projection-Instance)
                  (<=> (Instance-Of ?Instance ?Projection-Relation)
                       (Exists (?Tuple)
                               (And (Member ?Tuple ?Relation)
                                    (= (Nth ?Tuple ?Column)
                                       ?Instance)))))))

Axioms:

(Nth-Domain Projection 3 Class)

(Nth-Domain Projection 2 Positive-Integer)

Other Related Axioms:

(=> (= (Projection ?Relation ?Column) ?Projection-Relation)
    (Forall (?Projection-Instance)
            (<=> (Instance-Of ?Instance ?Projection-Relation)
                 (Exists (?Tuple)
                         (And (Member ?Tuple ?Relation)
                              (= (Nth ?Tuple ?Column) ?Instance))))))

(=> (= (Projection ?Relation ?Column) ?Projection-Relation)
    (Class ?Projection-Relation))

(=> (= (Projection ?Relation ?Column) ?Projection-Relation)
    (=< ?Column (Arity ?Relation)))

(=> (= (Projection ?Relation ?Column) ?Projection-Relation)
    (Positive-Integer ?Column))

(=> (= (Projection ?Relation ?Column) ?Projection-Relation)
    (Defined (Arity ?Relation)))