Class TERM

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

Slots on this class:

Documentation: KIF term expression

Instance-Of: Class

Alias: Expression

Exhaustive-Subclass-Partition: {

Constant, Listterm, Logterm, Quanterm, Quoterm, Setterm, Variable}

Superclass-Of:

Constant, Funterm, Listterm, Logterm, Operator, Quanterm, Quoterm, Setterm, Variable

Other Related Axioms:

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

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

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

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

(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 (?R ?Tlist)
        (And (Or (Relconst ?R) (Funconst ?R))
             (List ?Tlist)
             (>= (Length ?Tlist) 1)
             (=> (Item ?T ?Tlist) (Term ?T))
             (= ?X (Cons ?R ?Tlist))))

(<=> (Relsent ?X)
     (Exists (?R ?Tlist)
             (And (Or (Relconst ?R) (Funconst ?R))
                  (List ?Tlist)
                  (>= (Length ?Tlist) 1)
                  (=> (Item ?T ?Tlist) (Term ?T))
                  (= ?X (Cons ?R ?Tlist)))))

(Exists (?T1 ?T2)
        (And (Term ?T1) (Term ?T2) (= ?X (Listof (Quote =) ?T1 ?T2))))

(<=> (Equation ?X)
     (And (Relsent ?X)
          (Exists (?T1 ?T2)
                  (And (Term ?T1)
                       (Term ?T2)
                       (= ?X (Listof (Quote =) ?T1 ?T2))))))

(Exists (?T1 ?T2)
        (And (Term ?T1)
             (Term ?T2)
             (= ?X (Listof (Quote /=) ?T1 ?T2))))

(<=> (Inequality ?X)
     (And (Relsent ?X)
          (Exists (?T1 ?T2)
                  (And (Term ?T1)
                       (Term ?T2)
                       (= ?X (Listof (Quote /=) ?T1 ?T2))))))