We need a new language for logical expressions, since we don't have all the nice characters (like upside-down A) that we would like to use. We will allow an infix format for input, and manipulate a Lisp-like prefix format internally. Here is a description of the formats (compare to [p 167, 187]). The prefix notation is a subset of the KIF 3.0 Knowledge Interchange Format.
Infix Prefix Meaning Alternate Infix Notation ========== ====== =========== ======================== ~P (not P) negation not P P ^ Q (and P Q) conjunction P and Q P | Q (or P Q) disjunction P or Q P => Q (=> P Q) implication P <=> Q (<=> P Q) logical equivalence P(x) (P x) predicate Q(x,y) (Q x y) predicate with multiple arguments f(x) (f x) function f(x)=3 (= (f x) 3) equality forall(x,P(x) (forall (x) (P x)) universal quantification exists(x,P(x) (exists (x) (P x)) existential quantification [a,b] (listof a b) list of elements {a,b} (setof a b) mathematical set of elements true true the true logical constant false false the false logical constantYou can also use the usual operators for mathematical notation: +, -, *, / for arithmetic, and &;lt;, >, <=, >= for comparison. Many of the functions we define also accept strings as input, interpreting them as infix expressions, so the following are equivalent:
(tell kb "P=>Q") (tell kb '(=> P Q))