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))
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. method ((kb literal-kb) sentence)
Add the sentence to the knowledge base.method ((kb literal-kb) sentence)
Remove the sentence from the knowledge base.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)." function (kb query)
Ask if query sentence is true; return t or nil.function (kb query &optional pattern)
Ask if query sentence is true; if it is, substitute bindings into pattern.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.
Indicates unification failureconstant
Indicates unification success, with no variables.
See if x and y match with given bindings. If they do, return a binding list that would make them equal [p 303].function (x)
Replace all variables in x with new ones.
Unify var with x, using (and maybe extending) bindings [p 303].function (x)
Is x a variable (a symbol starting with $)?function (var bindings)
Find a (variable . value) pair in a binding list.function (binding)
Get the variable part of a single binding.function (binding)
Get the value part of a single binding.function (var val)
Get the value part (for var) from a binding list.function (var val bindings)
Add a (var . value) pair to a binding list.function (var x bindings)
Does var occur anywhere inside x?function (bindings x)
Substitute the value of variables in bindings into x, taking recursively bound variables into account.function (x y)
Return something that unifies with both x and y (or fail).function (exp)
Return a list of all the variables in EXP.function (predicate tree &optional found-so-far)
Return a list of leaves of tree satisfying predicate, with duplicates removed.function (predicate tree)
Does predicate apply to any atom in the tree?variable
Create a new variable. Assumes user never types variables of form $X.9
Convert a sentence p to conjunctive normal form [p 279-280].function (p)
Convert a sentence p to implicative normal form [p 282].function (p)
Try to convert sentence to a Horn clause, or a conjunction of Horn clauses. Signal an error if this cannot be done.function (sentence)
Canonicalize a sentence into proper logical form.
Given P, return ~P, but with the negation moved as far in as possible.function (disjuncts)
Return a CNF expression for the disjunction.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.function (name)
Return a unique skolem constant, a symbol starting with '$'.function (p q &optional bindings)
Are p and q renamings of each other? (That is, expressions that differ only in variable names?)
An atomic clause has no connectives or quantifiers.function (sentence)
A literal is an atomic clause or a negated atomic clause.function (sentence)
A negative clause has NOT as the operator.function (sentence)
A Horn clause (in INF) is an implication with atoms on the left and one atom on the right.function (sentence)
Return a list of the conjuncts in this sentence.function (sentence)
Return a list of the disjuncts in this sentence.function (args)
Form a conjunction with these args.function (args)
Form a disjunction with these args.
A simple KB implementation that builds a big conjoined sentence.type (symbols sentences rows)
Add a sentence to a propositional knowledge base.method ((kb prop-kb) query fn)
Ask a propositional knowledge base if the query is entailed by the kb.method ((kb prop-kb) sentence)
Remove a sentence from a knowledge base.
Return either VALID, SATISFIABLE or UNSATISFIABLE.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)))).
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.
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).function (table &optional stream)
Print a truth table.function (symbols sentences)
Compute the truth of each sentence under all interpretations of symbols.function (symbols)
Return all 2^n interpretations for a list of n symbols.function (sentence)
Return a list of all the propositional symbols in sentence.function (sentence)
Return a list of all non-atom sub-sentences of sentence.function (sentence)
Convert a prefix sentence back into an infix notation with brief operators.
method ((kb horn-kb) sentence)
Add a sentence to a Horn knowledge base. Warn if its not a Horn sentence.method ((kb horn-kb) sentence)
Delete each conjunct of sentence from KB.method ((kb horn-kb) query fn)
Use backward chaining to decide if sentence is true.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.
Add a sentence to a FOL knowledge base.method ((kb fol-kb) sentence)
Delete each conjunct of sentence from KB.method ((kb fol-kb) query fn)
Use resolution to decide if sentence is true.
Find clauses that might resolve with a clause containing literal.function (kb clause)
Remove the minimal-cnf clauses from the KB.function (sentence)
Convert a logical sentence to minimal CNF (no and/or connectives).function (kb)
Undo the changes that were temporarilly made to KB.function (clause)
Is clause a tautology (something that is always true)?
Try to prove that ~SOS is true (given KB) by resolution refutation.function (literal clause)
Resolve a single literal against a clausefunction (item list pred &key key)
File logic/algorithms/infix.lisp
A list of lists of operators, highest precedence first.function (infix)
Convert an infix expression to prefix.function (infix)
Find the highest-precedence operator in INFIX and reduce accordingly.function (op)
function (sequence start length new)
Find the matching op (paren or bracket) and reduce.function (exp)
Convert (|,| a b) to (a b).function (exp)
Change (FORALL x y P) to (FORALL (x y) P).
Convert a string to a list of tokens.function (string start)
Return the first token in string and the position after it, or nil.function (string pred i)
Convert string to symbol, preserving case, except for AND/OR/NOT/FORALL/EXISTS.function (x)
File logic/environments/shopping.lisp
type (zoomed-at can-zoom-at visible-offsets)
The percept is a sequence of sights, touch (i.e. bump), and sounds.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.function (agent env)
Return a list of visual attributes: (loc size color shape words)function (object)
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 |