Class Null

Subclass-Of@Frame-Ontology: List
Has-Instance@Frame-Ontology: Nil
Instance-Of@Frame-Ontology: Class@Frame-Ontology, Relation@Ol-User%Kif-Relations, Set@Ol-User%Kif-Sets
Arity@Frame-Ontology: 1
Documentation@Ol%Frame-Ontology: True of the list with no items.


Slots:


Equivalence Axioms for Null:

(<=> (Null ?List) (And (List ?List) (= (Length ?List) 0)))


Implication Axioms mentioning Null:

(=> (= (Rest ?List) ?Rest-List)
    (Or (And (Null ?List) (= ?Rest-List ?List))
        (Exists (?X @Items)
                (And (= ?List (Listof ?X @Items))
                     (= ?Rest-List (Listof @Items))))))


Equivalence Axioms mentioning Null:

(<=> (Rest ?List)
     (Or (And (Null ?List) (= ?Rest-List ?List))
         (Exists (?X @Items)
                 (And (= ?List (Listof ?X @Items))
                      (= ?Rest-List (Listof @Items))))))

(<=> (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)))))))


Axioms mentioning Null:

(Not (Null ?List))

(Not (Null ?List-Of-Relations))