Class SENTENCE

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

Slots on this class:

Documentation:

KIF sentence expression. Has a truth value.

Instance-Of: Class

Subclass-Of: Expression

Exhaustive-Subclass-Partition: {

Logconst, Logsent, Quantsent, Relsent}

Range-Of: Defining-axiom

Superclass-Of:

Analytic-truth, Logconst, Logsent, Quantsent, Relsent, Truth

Other Related 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)))))

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

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

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

(Exists (?P) (And (Sentence ?P) (= ?X (Listof (Quote Not) ?P))))

(<=> (Negation ?X)
     (Exists (?P) (And (Sentence ?P) (= ?X (Listof (Quote Not) ?P)))))

(Exists (?Plist)
        (And (List ?Plist)
             (>= (Length ?Plist) 1)
             (=> (Item ?P ?Plist) (Sentence ?P))
             (= ?X (Cons (Quote And) ?Plist))))

(<=> (Conjunction ?X)
     (Exists (?Plist)
             (And (List ?Plist)
                  (>= (Length ?Plist) 1)
                  (=> (Item ?P ?Plist) (Sentence ?P))
                  (= ?X (Cons (Quote And) ?Plist)))))

(Exists (?Plist)
        (And (List ?Plist)
             (>= (Length ?Plist) 1)
             (=> (Item ?P ?Plist) (Sentence ?P))
             (= ?X (Cons (Quote Or) ?Plist))))

(<=> (Disjunction ?X)
     (Exists (?Plist)
             (And (List ?Plist)
                  (>= (Length ?Plist) 1)
                  (=> (Item ?P ?Plist) (Sentence ?P))
                  (= ?X (Cons (Quote Or) ?Plist)))))

(Exists (?Plist)
        (And (List ?Plist)
             (>= (Length ?Plist) 2)
             (=> (Item ?P ?Plist) (Sentence ?P))
             (= ?X (Cons (Quote =>) ?Plist))))

(<=> (Implication ?X)
     (Exists (?Plist)
             (And (List ?Plist)
                  (>= (Length ?Plist) 2)
                  (=> (Item ?P ?Plist) (Sentence ?P))
                  (= ?X (Cons (Quote =>) ?Plist)))))

(Exists (?Plist)
        (And (List ?Plist)
             (>= (Length ?Plist) 2)
             (=> (Item ?P ?Plist) (Sentence ?P))
             (= ?X (Cons (Quote <=) ?Plist))))

(<=> (Reverse-Implication ?X)
     (Exists (?Plist)
             (And (List ?Plist)
                  (>= (Length ?Plist) 2)
                  (=> (Item ?P ?Plist) (Sentence ?P))
                  (= ?X (Cons (Quote <=) ?Plist)))))

(Exists (?P1 ?P2)
        (And (Sentence ?P1)
             (Sentence ?P2)
             (= ?X (Listof (Quote <=>) ?P1 ?P2))))

(<=> (Equivalence ?X)
     (Exists (?P1 ?P2)
             (And (Sentence ?P1)
                  (Sentence ?P2)
                  (= ?X (Listof (Quote <=>) ?P1 ?P2)))))

(Or (Exists (?V ?P)
            (And (Indvar ?V)
                 (Sentence ?P)
                 (Or (= ?X (Listof (Quote Forall) ?V ?P))
                     (= ?X (Listof (Quote Exists) ?V ?P)))))
    (Exists (?Vlist ?P)
            (And (List ?Vlist)
                 (Sentence ?P)
                 (>= (Length ?Vlist) 1)
                 (=> (Item ?V ?Vlist) (Indvar ?V))
                 (Or (= ?X (Listof (Quote Forall) ?Vlist ?P))
                     (= ?X (Listof (Quote Exists) ?Vlist ?P))))))

(<=> (Quantsent ?X)
     (Or (Exists (?V ?P)
                 (And (Indvar ?V)
                      (Sentence ?P)
                      (Or (= ?X (Listof (Quote Forall) ?V ?P))
                          (= ?X (Listof (Quote Exists) ?V ?P)))))
         (Exists (?Vlist ?P)
                 (And (List ?Vlist)
                      (Sentence ?P)
                      (>= (Length ?Vlist) 1)
                      (=> (Item ?V ?Vlist) (Indvar ?V))
                      (Or (= ?X (Listof (Quote Forall) ?Vlist ?P))
                          (= ?X (Listof (Quote Exists) ?Vlist ?P)))))))

(=> (Defining-Axiom $X $Y) (Sentence $Y))