Class Sentence

• Defined in ontology: Kif-meta
• Source pathname: /tmp_mnt/vol/q/htw/cms/ontolingua/examples/kif/../../all-ontologies/kif/kif-meta.lisp

Subclass-Of@Frame-Ontology: Expression

Exhaustive-Subclass-Partition@Frame-Ontology: {

Logconst, Logsent, Quantsent, Relsent}

Superclass-Of@Frame-Ontology:

Analytic-Truth, Logsent, Quantsent, Relsent, Truth ...

Instance-Of@Frame-Ontology: Class@Frame-Ontology, Relation@Ol-User%Kif-Relations, Set

Range-Of@Frame-Ontology: Defining-Axiom, Related-Axioms@Frame-Ontology

Arity@Frame-Ontology: 1

Documentation@Ol%Frame-Ontology: KIF sentence expression. Has a truth value.

---

Slots:

Equivalence Axioms mentioning Sentence:

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

(<=> (Quanterm ?X)
     (Or (Exists (?T ?P)
                 (And (Term ?T)
                      (Sentence ?P)
                      (= ?X (Listof 'The ?T ?P))))
         (Exists (?T ?P)
                 (And (Term ?T)
                      (Sentence ?P)
                      (= ?X (Listof 'Setofall ?T ?P))))
         (Exists (?Vlist ?P)
                 (And (List ?Vlist)
                      (Sentence ?P)
                      (>= (Length ?Vlist) 1)
                      (=> (Item ?V ?Vlistp) (Indvar ?V))
                      (= ?X (Listof '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 '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))))))

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

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

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