Class NULL

• Defined in theory: Kif-lists
• Source code: kif-lists.lisp

Slots on this class:

Documentation:

True of the list with no items.

Instance-Of: Class

Subclass-Of: List

Has-Instance:

Equivalence Axioms:

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

Axioms:

(= (Length ?List) 0)

(List ?List)

Other Related Axioms:

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

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

(<- (Last ?List)
    (Cond ((Null ?List) Bottom)
          ((Null (Rest ?List)) (First ?List))
          (True (Last (Rest ?List)))))

(<- (Butlast ?List)
    (Cond ((Null ?List) Bottom)
          ((Null (Rest ?List)) Nil)
          (True (Cons (First ?List) (Butlast (Rest ?List))))))

(=> (Item ?X ?List)
    (And (Not (Null ?List))
         (Or (= ?X (First ?List)) (Item ?X (Rest ?List)))))

(<- (Append ?L1 ?L2)
    (If (Null ?L1)
        (If (List ?L2) ?L2)
        (Cons (First ?L1) (Append (Rest ?L1) ?L2))))

(<- (Revappend ?L1 ?L2)
    (If (Null ?L1)
        (If (List ?L2) ?L2)
        (Revappend (Rest ?L1) (Cons (First ?L1) ?L2))))

(<- (Remove ?X ?List)
    (Cond ((Null ?List) Nil)
          ((And (= ?X (First ?List)) (List ?List))
           (Remove ?X (Rest ?List)))
          ((List ?List) (Cons ?X (Remove ?X (Rest ?List))))))

(<- (Subst ?X ?Y ?Z)
    (Cond ((= ?Y ?Z) ?X)
          ((Null ?Z) Nil)
          ((List ?Z)
           (Cons (Subst ?X ?Y (First ?Z)) (Subst ?X ?Y (Rest ?Z))))
          (True ?Z)))

(<- (Length ?List)
    (Cond ((Null ?List) 0) ((List ?List) (1+ (Length (Rest ?List))))))