Class Term

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

Exhaustive-Subclass-Partition@Frame-Ontology: {

Funterm, Listterm, Logterm, Quanterm, Quoterm, Setterm, Word}

Superclass-Of@Frame-Ontology:

Listterm, Logterm, Quanterm, Quoterm, Setterm ...

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

Alias@Frame-Ontology: Expression

Arity@Frame-Ontology: 1

Documentation@Ol%Frame-Ontology: KIF term expression <H3>Notes:</H3> <UL> <LI>See notes on Word. <P></UL>

---

Slots:

Implication Axioms mentioning Term:

(=> (Funterm ?Expr) (Term ?Expr))

(=> (Listterm ?Expr) (Term ?Expr))

(=> (Setterm ?Expr) (Term ?Expr))

(=> (Quoterm ?Expr) (Term ?Expr))

(=> (Equation ?X)
    (Exists (?T1 ?T2)
            (And (Term ?T1)
                 (Term ?T2)
                 (= ?X (Listof '= ?T1 ?T2)))))

Equivalence Axioms mentioning Term:

(<=> (Funterm ?Expr)
     (And (Term ?Expr)
          (List ?Expr)
          (Value-Type@Frame-Ontology ?Expr First Funconst)
          (Value-Cardinality@Frame-Ontology ?Expr First 1)))

(<=> (Listterm ?Expr)
     (And (Term ?Expr) (List ?Expr) (= (First ?Expr) 'Listof)))

(<=> (Setterm ?Expr)
     (And (Term ?Expr) (List ?Expr) (= (First ?Expr) 'Setof)))

(<=> (Quoterm ?Expr)
     (And (Term ?Expr)
          (List ?Expr)
          (= (First ?Expr) 'Quote)
          (Expression (First (First ?Expr)))))

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