Class Defined

Instance-Of@Frame-Ontology: Class@Frame-Ontology, Relation, Set
Arity@Frame-Ontology: 1
Documentation@Ol%Frame-Ontology:
A term is defined if it does not denote the undefined object, called bottom. (defined (F x)) means that the function F is defined for the object x. (F x) denotes its value. In relational terminology, (defined (F x)) means (exists ?y (F x ?y)).

Notes:

  • DEFINED is not in the KIF 3.0 spec.


Slots:


Equivalence Axioms for Defined:

(<=> (Defined ?X) (Not (Undefined ?X)))


Implication Axioms mentioning Defined:

(=> (= (Projection@Frame-Ontology ?Relation ?Column)
       ?Projection-Relation)
    (Defined (Arity@Frame-Ontology ?Relation)))

(=> (Subrelation-Of@Frame-Ontology ?Child-Relation ?Parent-Relation)
    (=> (Defined (Arity@Frame-Ontology ?Parent-Relation))
        (= (Arity@Frame-Ontology ?Child-Relation)
           (Arity@Frame-Ontology ?Parent-Relation))))


Equivalence Axioms mentioning Defined:

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

(<=> (Nth-Domain@Frame-Ontology ?Relation ?N ?Type)
     (And (Defined (Arity@Frame-Ontology ?Relation))
          (Positive-Integer ?N)
          (Class@Frame-Ontology ?Type)
          (Forall (?Tuple)
                  (=> (Member ?Tuple ?Relation)
                      (And (>= (Length ?Tuple) ?N)
                           (Instance-Of@Frame-Ontology (Nth ?Tuple ?N)
                                        ?Type))))))