Class LOGTERM

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

Slots on this class:

Instance-Of: Class

Subclass-Of: Term

Equivalence Axioms:

(<=> (Logterm ?X)
     (Or (Exists (?P1 ?T1)
                 (And (Sentence ?P1)
                      (Term ?T1)
                      (= ?X (Listof (Quote If) ?P1 ?T1))))
         (Exists (?P1 ?T1 ?T2)
                 (And (Sentence ?P1)
                      (Term ?T1)
                      (Term ?T2)
                      (= ?X (Listof (Quote 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 (Quote Cond) ?Clist))))))

Axioms:

(Or (Exists (?P1 ?T1)
            (And (Sentence ?P1)
                 (Term ?T1)
                 (= ?X (Listof (Quote If) ?P1 ?T1))))
    (Exists (?P1 ?T1 ?T2)
            (And (Sentence ?P1)
                 (Term ?T1)
                 (Term ?T2)
                 (= ?X (Listof (Quote 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 (Quote Cond) ?Clist)))))

Other Related Axioms:

(Exhaustive-Subclass-Partition Term
                               (Setof Variable
                                      Constant
                                      Listterm
                                      Setterm
                                      Quoterm
                                      Logterm
                                      Quanterm))

(<=> (Logterm ?X)
     (Or (Exists (?P1 ?T1)
                 (And (Sentence ?P1)
                      (Term ?T1)
                      (= ?X (Listof (Quote If) ?P1 ?T1))))
         (Exists (?P1 ?T1 ?T2)
                 (And (Sentence ?P1)
                      (Term ?T1)
                      (Term ?T2)
                      (= ?X (Listof (Quote 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 (Quote Cond) ?Clist))))))