# Logic (Subsystem of AIMA Code)

The logic system covers part III of the book. We define knowledge bases, and `tell` and `ask` operations on those knowledge bases. The interface is defined in the file tell-ask.lisp.

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 constant

You 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))