Function First

• 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:

Binary-Relation@Ol-User%Kif-Relations, Function@Ol-User%Kif-Relations, Relation@Ol-User%Kif-Relations, Set@Ol-User%Kif-Sets

Domain@Frame-Ontology: List

Arity@Frame-Ontology: 2

Frame References to First:

In class@frame-ontology Funterm@Ol-User%Kif-Meta:

Slots:

First:

Slot-Cardinality@Frame-Ontology: 1

Slot-Value-Type@Frame-Ontology: Funconst@Ol-User%Kif-Meta

Implication Axioms mentioning First:

(=> (Item ?X ?List) (Or (= ?X (First ?List)) (Item ?X (Rest ?List))))

(=> (Composition-Of@Frame-Ontology ?Binary-Relation
                    ?List-Of-Relations)
    (Or (And (Single ?List-Of-Relations)
             (= ?Binary-Relation (First ?List-Of-Relations)))
        (And (Double ?List-Of-Relations)
             (= ?Binary-Relation
                (Composition@Ol-User%Kif-Relations 
                    (First (Rest ?List-Of-Relations))
                    (First ?List-Of-Relations))))
        (Exists 
            (?Left-Sub-Relation)
            (And (= ?Binary-Relation
                    (Composition@Ol-User%Kif-Relations 
                        (Last ?List-Of-Relations)
                        ?Left-Sub-Relation))
                 (Composition-Of@Frame-Ontology 
                     ?Left-Sub-Relation
                     (Butlast ?List-Of-Relations))))))

(=> (Listterm@Ol-User%Kif-Meta ?Expr)
    (= (First ?Expr) 'Listof))

(=> (Setterm@Ol-User%Kif-Meta ?Expr) (= (First ?Expr) 'Setof))

(=> (Quoterm@Ol-User%Kif-Meta ?Expr)
    (Expression@Ol-User%Kif-Meta (First (First ?Expr))))

Equivalence Axioms mentioning First:

(<=> (Composition-Of@Frame-Ontology ?Binary-Relation
                     ?List-Of-Relations)
     (And (Binary-Relation@Ol-User%Kif-Relations ?Binary-Relation)
          (List ?List-Of-Relations)
          (Not (Null ?List-Of-Relations))
          (=> (Item ?R ?List-Of-Relations)
              (Binary-Relation@Ol-User%Kif-Relations ?R))
          (Or (And (Single ?List-Of-Relations)
                   (= ?Binary-Relation (First ?List-Of-Relations)))
              (And (Double ?List-Of-Relations)
                   (= ?Binary-Relation
                      (Composition@Ol-User%Kif-Relations 
                          (First (Rest ?List-Of-Relations))
                          (First ?List-Of-Relations))))
              (Exists 
                  (?Left-Sub-Relation)
                  (And (= ?Binary-Relation
                          (Composition@Ol-User%Kif-Relations 
                              (Last ?List-Of-Relations)
                              ?Left-Sub-Relation))
                       (Composition-Of@Frame-Ontology 
                           ?Left-Sub-Relation
                           (Butlast ?List-Of-Relations)))))))

(<=> (Funterm@Ol-User%Kif-Meta ?Expr)
     (And (Term@Ol-User%Kif-Meta ?Expr)
          (List ?Expr)
          (Value-Type@Frame-Ontology ?Expr
                      First
                      Funconst@Ol-User%Kif-Meta)
          (Value-Cardinality@Frame-Ontology ?Expr First 1)))

(<=> (Listterm@Ol-User%Kif-Meta ?Expr)
     (And (Term@Ol-User%Kif-Meta ?Expr)
          (List ?Expr)
          (= (First ?Expr) 'Listof)))

(<=> (Setterm@Ol-User%Kif-Meta ?Expr)
     (And (Term@Ol-User%Kif-Meta ?Expr)
          (List ?Expr)
          (= (First ?Expr) 'Setof)))

(<=> (Quoterm@Ol-User%Kif-Meta ?Expr)
     (And (Term@Ol-User%Kif-Meta ?Expr)
          (List ?Expr)
          (= (First ?Expr) 'Quote)
          (Expression@Ol-User%Kif-Meta (First (First ?Expr)))))