Class RELSENT

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

Slots on this class:

Instance-Of: Class

Subclass-Of: Sentence

Superclass-Of: Equation, Inequality

Equivalence Axioms:

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

Axioms:

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

Other Related Axioms:

(Exhaustive-Subclass-Partition Sentence
                               (Setof Logconst
                                      Relsent
                                      Logsent
                                      Quantsent))

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

(<=> (Equation ?X)
     (And (Relsent ?X)
          (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))))))