Function Nth

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

Instance-Of@Frame-Ontology: Function@Ol-User%Kif-Relations, Relation@Ol-User%Kif-Relations, Set@Ol-User%Kif-Sets

Arity@Frame-Ontology: 3

Documentation@Ol%Frame-Ontology:

{tt nth} returns the item in the list specified as its first
argument in the position specified as its second argument.

Axioms for Nth:

(Nth-Domain@Frame-Ontology Nth 2 Natural)

(Nth-Domain@Frame-Ontology Nth 1 List)

Implication Axioms mentioning Nth:

(=> (= (Projection@Frame-Ontology ?Relation ?Column)
       ?Projection-Relation)
    (Forall (?Projection-Instance)
            (<=> (Instance-Of@Frame-Ontology ?Instance
                              ?Projection-Relation)
                 (Exists (?Tuple)
                         (And (Member@Ol-User%Kif-Sets ?Tuple
                                      ?Relation)
                              (= (Nth ?Tuple ?Column) ?Instance))))))

(=> (Nth-Domain@Frame-Ontology ?Relation ?N ?Type)
    (Forall (?Tuple)
            (=> (Member@Ol-User%Kif-Sets ?Tuple ?Relation)
                (And (>= (Length ?Tuple) ?N)
                     (Instance-Of@Frame-Ontology (Nth ?Tuple ?N)
                                  ?Type)))))

Equivalence Axioms mentioning Nth:

(<=> (Projection@Frame-Ontology ?Relation ?Column)
     (And (Defined@Ol-User%Kif-Extensions 
              (Arity@Frame-Ontology ?Relation))
          (Positive-Integer@Ol-User%Kif-Extensions ?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@Ol-User%Kif-Sets ?Tuple
                                            ?Relation)
                                    (= (Nth ?Tuple ?Column)
                                       ?Instance)))))))

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