# 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/:
logic/algorithms/:
• 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/:

## Testing Logical Inference

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 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.

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

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

## Propositional Logic

prop-kb type (sentence)

A simple KB implementation that builds a big conjoined sentence.

truth-table type (symbols sentences rows)

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.

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

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

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

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