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.
(<=> (Defined ?X) (Not (Undefined ?X)))
(=> (= (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))))
(<=> (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))))))