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

logic/:

- test-logic.lisp Testing Logical Inference

logic/algorithms/:

- tell-ask.lisp Main Functions on KBs: Tell, Retract, Ask-Each, Ask, Ask-Pattern[s]
- unify.lisp Unification and Substitutions (aka Binding Lists)
- normal.lisp Convert Expressions to Normal Form (Conjunctive, Implicative or Horn)
- prop.lisp Propositional Logic
- horn.lisp Logical Reasoning in Horn Clause Knowledge Bases
- fol.lisp First Order Logic (FOL) Tell, Retract, and Ask-Each
- infix.lisp Prefix to Infix Conversion

logic/environments/:

- shopping.lisp The Shopping World:

## File logic/test-logic.lisp

## Testing Logical Inference

## File logic/algorithms/tell-ask.lisp

## Main Functions on KBs: Tell, Retract, Ask-Each, Ask, Ask-Pattern[s]

First we define a very simple kind of knowledge base, literal-kb, that just stores a list of literal sentences.

literal-kb

type (sentences)

> A knowledge base that just stores a set of literal sentences.

There are three generic functions that operate on knowledge bases, and that must be defined as methods for each type of knowledge base: TELL, RETRACT, and ASK-EACH. Here we show the implementation for literal-kb; elsewhere you'll see implementations for propositional, Horn, and FOL KBs.

tell

method ((kb literal-kb) sentence)

> Add the sentence to the knowledge base.

retract

method ((kb literal-kb) sentence)

> Remove the sentence from the knowledge base.

ask-each

method ((kb literal-kb) query fn)

> For each proof of query, call fn on the substitution that the proof ends up with.

There are three other ASK functions, defined below, that are defined in terms of ASK-EACH. These are defined once and for all here (not for each kind of KB)."

ask

function (kb query)

> Ask if query sentence is true; return t or nil.

ask-pattern

function (kb query &optional pattern)

> Ask if query sentence is true; if it is, substitute bindings into pattern.

ask-patterns

function (kb query &optional pattern)

> Find all proofs for query sentence, substitute bindings into pattern once for each proof. Return a list of all substituted patterns.

## File logic/algorithms/unify.lisp

## Unification and Substitutions (aka Binding Lists)

This code is borrowed from "Paradigms of AI Programming: Case Studies in Common Lisp", by Peter Norvig, published by Morgan Kaufmann, 1992. The complete code from that book is available for ftp at mkp.com in the directory "pub/Norvig". Note that it uses the term "bindings" rather than "substitution" or "theta". The meaning is the same.

## Constants

+fail+

constant

> Indicates unification failure

+no-bindings+

constant

> Indicates unification success, with no variables.

## Top Level Functions

unify

function (x y &optional bindings)

> See if x and y match with given bindings. If they do, return a binding list that would make them equal [p 303].

rename-variables

function (x)

> Replace all variables in x with new ones.

## Auxiliary Functions

unify-var

function (var x bindings)

> Unify var with x, using (and maybe extending) bindings [p 303].

variable?

function (x)

> Is x a variable (a symbol starting with $)?

get-binding

function (var bindings)

> Find a (variable . value) pair in a binding list.

binding-var

function (binding)

> Get the variable part of a single binding.

binding-val

function (binding)

> Get the value part of a single binding.

make-binding

function (var val)

lookup function (var bindings)

> Get the value part (for var) from a binding list.

extend-bindings

function (var val bindings)

> Add a (var . value) pair to a binding list.

occurs-in?

function (var x bindings)

> Does var occur anywhere inside x?

subst-bindings

function (bindings x)

> Substitute the value of variables in bindings into x, taking recursively bound variables into account.

unifier

function (x y)

> Return something that unifies with both x and y (or fail).

variables-in

function (exp)

> Return a list of all the variables in EXP.

unique-find-anywhere-if

function (predicate tree &optional found-so-far)

> Return a list of leaves of tree satisfying predicate, with duplicates removed.

find-anywhere-if

function (predicate tree)

> Does predicate apply to any atom in the tree?

*new-variable-counter*

variable

new-variable function (var)

> Create a new variable. Assumes user never types variables of form $X.9

## File logic/algorithms/normal.lisp

## Convert Expressions to Normal Form (Conjunctive, Implicative or Horn)

This could be done much more efficiently by using a special representation for CNF, which eliminates the explicit ANDs and ORs. This code is meant to be informative, not efficient.

## Top-Level Functions

->cnf

function (p &optional vars)

> Convert a sentence p to conjunctive normal form [p 279-280].

->inf

function (p)

> Convert a sentence p to implicative normal form [p 282].

->horn

function (p)

> Try to convert sentence to a Horn clause, or a conjunction of Horn clauses. Signal an error if this cannot be done.

logic

function (sentence)

> Canonicalize a sentence into proper logical form.

## Auxiliary Functions

cnf1->inf1

function (p)

eliminate-implications function (p)

move-not-inwards function (p)

> Given P, return ~P, but with the negation moved as far in as possible.

merge-disjuncts

function (disjuncts)

> Return a CNF expression for the disjunction.

skolemize

function (p vars outside-vars)

> Within the proposition P, replace each of VARS with a skolem constant, or if OUTSIDE-VARS is non-null, a skolem function of them.

skolem-constant

function (name)

> Return a unique skolem constant, a symbol starting with '$'.

renaming?

function (p q &optional bindings)

> Are p and q renamings of each other? (That is, expressions that differ only in variable names?)

## Utility Predicates and Accessors

+logical-connectives+

constant

+logical-quantifiers+ constant

atomic-clause? function (sentence)

> An atomic clause has no connectives or quantifiers.

literal-clause?

function (sentence)

> A literal is an atomic clause or a negated atomic clause.

negative-clause?

function (sentence)

> A negative clause has NOT as the operator.

horn-clause?

function (sentence)

> A Horn clause (in INF) is an implication with atoms on the left and one atom on the right.

conjuncts

function (sentence)

> Return a list of the conjuncts in this sentence.

disjuncts

function (sentence)

> Return a list of the disjuncts in this sentence.

conjunction

function (args)

> Form a conjunction with these args.

disjunction

function (args)

> Form a disjunction with these args.

## File logic/algorithms/prop.lisp

## Propositional Logic

prop-kb

type (sentence)

> A simple KB implementation that builds a big conjoined sentence.

truth-table

type (symbols sentences rows)

## Tell, Ask, and Retract

tell

method ((kb prop-kb) sentence)

> Add a sentence to a propositional knowledge base.

ask-each

method ((kb prop-kb) query fn)

> Ask a propositional knowledge base if the query is entailed by the kb.

retract

method ((kb prop-kb) sentence)

> Remove a sentence from a knowledge base.

## Other Useful Top-Level Functions

validity

function (sentence)

> Return either VALID, SATISFIABLE or UNSATISFIABLE.

truth-table

function (sentence)

> Build and print a truth table for this sentence, with columns for all the propositions and all the non-trivial component sentences. Iff the sentence is valid, the last column will have all T's. Example: (truth-table '(<=> P (not (not P)))).

## Auxiliary Functions

eval-truth

function (sentence &optional interpretation)

> Evaluate the truth of the sentence under an interpretation. The interpretation is a list of (proposition . truth-value) pairs, where a truth-value is t or nil, e.g., ((P . t) (Q . nil)). It is an error if there are any propositional symbols in the sentence that are not given a value in the interpretation.

## Truth Tables

build-truth-table

function (sentence &key short)

> Build a truth table whose last column is the sentence. If SHORT is true, then that is the only column. If SHORT is false, all the sub-sentences are also included as columns (except constants).

print-truth-table

function (table &optional stream)

> Print a truth table.

compute-truth-entries

function (symbols sentences)

> Compute the truth of each sentence under all interpretations of symbols.

all-truth-interpretations

function (symbols)

> Return all 2^n interpretations for a list of n symbols.

prop-symbols-in

function (sentence)

> Return a list of all the propositional symbols in sentence.

complex-sentences-in

function (sentence)

> Return a list of all non-atom sub-sentences of sentence.

sentence-output-form

function (sentence)

> Convert a prefix sentence back into an infix notation with brief operators.

## File logic/algorithms/horn.lisp

## Logical Reasoning in Horn Clause Knowledge Bases

horn-kb

type (table)

tell method ((kb horn-kb) sentence)

> Add a sentence to a Horn knowledge base. Warn if its not a Horn sentence.

retract

method ((kb horn-kb) sentence)

> Delete each conjunct of sentence from KB.

ask-each

method ((kb horn-kb) query fn)

> Use backward chaining to decide if sentence is true.

back-chain-each

function (kb goals bindings fn)

> Solve the conjunction of goals by backward chaining. See [p 275], but notice that this implementation is different. It applies fn to each answer found, and handles composition differently.

## File logic/algorithms/fol.lisp

## First Order Logic (FOL) Tell, Retract, and Ask-Each

fol-kb

type ( a fol (first-order logic) kb stores clauses. access to the kb is via possible-resolvers, which takes a literal (e.g. (not d), or b), and returns all the clauses that contain the literal. we also keep a list of temporary clauses, added to the kb during a proof and removed at the end. internally, clauses are in minimal-cnf format, which is cnf without the and/or. so (and (or p q) (or r (not s))) becomes ((p q) (r (not s))) positive-clauses negative-clauses temp-added)

tell method ((kb fol-kb) sentence)

> Add a sentence to a FOL knowledge base.

retract

method ((kb fol-kb) sentence)

> Delete each conjunct of sentence from KB.

ask-each

method ((kb fol-kb) query fn)

> Use resolution to decide if sentence is true.

## FOL Knowledge Base Utility Functions

possible-resolvers

function (kb literal)

> Find clauses that might resolve with a clause containing literal.

tell-minimal-cnf-clause

function (kb clause)

retract-minimal-cnf-clauses function (kb clauses)

> Remove the minimal-cnf clauses from the KB.

->minimal-cnf

function (sentence)

> Convert a logical sentence to minimal CNF (no and/or connectives).

undo-temp-changes

function (kb)

> Undo the changes that were temporarilly made to KB.

tautology?

function (clause)

> Is clause a tautology (something that is always true)?

## Functions for Resolution Refutation Theorem Proving

prove-by-refutation

function (kb sos fn)

> Try to prove that ~SOS is true (given KB) by resolution refutation.

resolve

function (literal clause)

> Resolve a single literal against a clause

insert

function (item list pred &key key)

## File logic/algorithms/infix.lisp

## Prefix to Infix Conversion

*infix-ops*

variable

> A list of lists of operators, highest precedence first.

->prefix

function (infix)

> Convert an infix expression to prefix.

reduce-infix

function (infix)

> Find the highest-precedence operator in INFIX and reduce accordingly.

op-token

function (op)

op-name function (op)

op-type function (op)

op-match function (op)

replace-subseq function (sequence start length new)

reduce-matching-op function (op pos infix)

> Find the matching op (paren or bracket) and reduce.

remove-commas

function (exp)

> Convert (|,| a b) to (a b).

handle-quantifiers

function (exp)

> Change (FORALL x y P) to (FORALL (x y) P).

## Tokenization: convert a string to a sequence of tokens

string->infix

function (string &optional start)

> Convert a string to a list of tokens.

parse-infix-token

function (string start)

> Return the first token in string and the position after it, or nil.

parse-span

function (string pred i)

make-logic-symbol function (string)

> Convert string to symbol, preserving case, except for AND/OR/NOT/FORALL/EXISTS.

operator-char?

function (x)

symbol-char? function (x)

function-symbol? function (x)

whitespace? function (ch)

## File logic/environments/shopping.lisp

## The Shopping World:

Warning! This code has not yet been tested or debugged!

*page250-supermarket*

variable

shopping-world type nil

## New Structures

credit-card

type nil

food type nil

tomato type nil

lettuce type nil

onion type nil

orange type nil

apple type nil

grapefruit type nil

sign type (words)

cashier-stand type nil

cashier type nil

seeing-agent-body type (zoomed-at can-zoom-at visible-offsets)

shopper type nil

## Percepts

get-percept

method ((env shopping-world) agent)

> The percept is a sequence of sights, touch (i.e. bump), and sounds.

see

function (agent env)

> Return a list of visual percepts for an agent. Note the agent's camera may either be zoomed out, so that it sees several squares, or zoomed in on one.

feel

function (agent env)

hear function (agent env)

see-loc function (loc env zoomed-at)

appearance function (object)

> Return a list of visual attributes: (loc size color shape words)

object-words

function (object)

zoom function (agent-body env offset)

> Zoom the camera at an offset if it is feasible; otherwise zoom out.

AIMA Home | Authors | Lisp Code | AI Programming | Instructors Pages