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))
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.
+fail+ constant
Indicates unification failure
+no-bindings+ constant
Indicates unification success, with no variables.
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.
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
->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.
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?)
+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.
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.
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)))).
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.
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.
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.
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.
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)?
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)
*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).
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)
*page250-supermarket* variable
shopping-world type nil
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
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 |