Class QUANTERM

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

Slots on this class:

Instance-Of: Class

Subclass-Of: Term

Equivalence Axioms:

(<=> (Quanterm ?X)
     (Or (Exists (?T ?P)
                 (And (Term ?T)
                      (Sentence ?P)
                      (= ?X (Listof (Quote The) ?T ?P))))
         (Exists (?T ?P)
                 (And (Term ?T)
                      (Sentence ?P)
                      (= ?X (Listof (Quote Setofall) ?T ?P))))
         (Exists (?Vlist ?P)
                 (And (List ?Vlist)
                      (Sentence ?P)
                      (>= (Length ?Vlist) 1)
                      (=> (Item ?V ?Vlistp) (Indvar ?V))
                      (= ?X (Listof (Quote Kappa) ?Vlistp ?P))))
         (Exists (?Vlist ?Sv ?P)
                 (And (List ?Vlist)
                      (Seqvar ?Sv)
                      (Sentence ?P)
                      (=> (Item ?V ?Vlist) (Indvar ?V))
                      (= ?X
                         (Listof 'Kappa
                                 (Append ?Vlist (Listof ?Sv))
                                 ?P))))
         (Exists (?Vlist ?T)
                 (And (List ?Vlist)
                      (Term ?T)
                      (>= (Length ?Vlist) 1)
                      (=> (Item ?V ?Vlistp) (Indvar ?V))
                      (= ?X (Listof (Quote Lambda) ?Vlistp ?T))))
         (Exists (?Vlist ?Sv ?T)
                 (And (List ?Vlist)
                      (Seqvar ?Sv)
                      (Sentence ?T)
                      (=> (Item ?V ?Vlist) (Indvar ?V))
                      (= ?X
                         (Listof 'Lambda
                                 (Append ?Vlist (Listof ?Sv))
                                 ?T))))))

Axioms:

(Or (Exists (?T ?P)
            (And (Term ?T)
                 (Sentence ?P)
                 (= ?X (Listof (Quote The) ?T ?P))))
    (Exists (?T ?P)
            (And (Term ?T)
                 (Sentence ?P)
                 (= ?X (Listof (Quote Setofall) ?T ?P))))
    (Exists (?Vlist ?P)
            (And (List ?Vlist)
                 (Sentence ?P)
                 (>= (Length ?Vlist) 1)
                 (=> (Item ?V ?Vlistp) (Indvar ?V))
                 (= ?X (Listof (Quote Kappa) ?Vlistp ?P))))
    (Exists (?Vlist ?Sv ?P)
            (And (List ?Vlist)
                 (Seqvar ?Sv)
                 (Sentence ?P)
                 (=> (Item ?V ?Vlist) (Indvar ?V))
                 (= ?X
                    (Listof 'Kappa
                            (Append ?Vlist (Listof ?Sv))
                            ?P))))
    (Exists (?Vlist ?T)
            (And (List ?Vlist)
                 (Term ?T)
                 (>= (Length ?Vlist) 1)
                 (=> (Item ?V ?Vlistp) (Indvar ?V))
                 (= ?X (Listof (Quote Lambda) ?Vlistp ?T))))
    (Exists (?Vlist ?Sv ?T)
            (And (List ?Vlist)
                 (Seqvar ?Sv)
                 (Sentence ?T)
                 (=> (Item ?V ?Vlist) (Indvar ?V))
                 (= ?X
                    (Listof 'Lambda
                            (Append ?Vlist (Listof ?Sv))
                            ?T)))))

Other Related Axioms:

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

(<=> (Quanterm ?X)
     (Or (Exists (?T ?P)
                 (And (Term ?T)
                      (Sentence ?P)
                      (= ?X (Listof (Quote The) ?T ?P))))
         (Exists (?T ?P)
                 (And (Term ?T)
                      (Sentence ?P)
                      (= ?X (Listof (Quote Setofall) ?T ?P))))
         (Exists (?Vlist ?P)
                 (And (List ?Vlist)
                      (Sentence ?P)
                      (>= (Length ?Vlist) 1)
                      (=> (Item ?V ?Vlistp) (Indvar ?V))
                      (= ?X (Listof (Quote Kappa) ?Vlistp ?P))))
         (Exists (?Vlist ?Sv ?P)
                 (And (List ?Vlist)
                      (Seqvar ?Sv)
                      (Sentence ?P)
                      (=> (Item ?V ?Vlist) (Indvar ?V))
                      (= ?X
                         (Listof 'Kappa
                                 (Append ?Vlist (Listof ?Sv))
                                 ?P))))
         (Exists (?Vlist ?T)
                 (And (List ?Vlist)
                      (Term ?T)
                      (>= (Length ?Vlist) 1)
                      (=> (Item ?V ?Vlistp) (Indvar ?V))
                      (= ?X (Listof (Quote Lambda) ?Vlistp ?T))))
         (Exists (?Vlist ?Sv ?T)
                 (And (List ?Vlist)
                      (Seqvar ?Sv)
                      (Sentence ?T)
                      (=> (Item ?V ?Vlist) (Indvar ?V))
                      (= ?X
                         (Listof 'Lambda
                                 (Append ?Vlist (Listof ?Sv))
                                 ?T))))))