Class LOGTERM

Subclass-Of: Term

Axioms:

(<=> (Logterm ?X)
     (Or (Exists (?P1 ?T1)
                 (And (Sentence ?P1)
                      (Term ?T1)
                      (= ?X (Listof 'If ?P1 ?T1))))
         (Exists (?P1 ?T1 ?T2)
                 (And (Sentence ?P1)
                      (Term ?T1)
                      (Term ?T2)
                      (= ?X (Listof 'If ?P1 ?T1 ?T2))))
         (Exists (?Clist)
                 (And (List ?Clist)
                      (=> (Item ?C ?Clist)
                          (Exists (?P ?T)
                                  (And (Sentence ?P)
                                       (Term ?T)
                                       (= ?C (Listof ?P ?T)))))
                      (= ?X (Cons 'Cond ?Clist))))))

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