"""A knowledge base to which you can tell and ask sentences.

def __init__(self, sentence=None):

raise NotImplementedError

def tell(self, sentence):

"Add the sentence to the KB."

raise NotImplementedError

def ask(self, query):

"""Return a substitution that makes the query true, or,

for result in self.ask_generator(query):

return result

return False

def ask_generator(self, query):

"Yield all the substitutions that make query true."

raise NotImplementedError

def retract(self, sentence):

"Remove sentence from the KB."

"A KB for propositional logic. Inefficient, with no indexing."

def __init__(self, sentence=None):

self.clauses = []

if sentence:

self.tell(sentence)

def tell(self, sentence):

"Add the sentence's clauses to the KB."

self.clauses.extend(conjuncts(to_cnf(sentence)))

def ask_generator(self, query):

"Yield the empty substitution if KB implies query; else nothing."

if tt_entails(Expr('&', *self.clauses), query):

yield {}

def retract(self, sentence):

"Remove the sentence's clauses from the KB."

for c in conjuncts(to_cnf(sentence)):

if c in self.clauses:

"""A generic logical knowledge-based agent program. [Fig. 7.1]"""

steps = itertools.count()

def program(percept):

t = steps.next()

KB.tell(make_percept_sentence(percept, t))

action = KB.ask(make_action_query(t))

KB.tell(make_action_sentence(action, t))

return action

def make_percept_sentence(self, percept, t):

return Expr("Percept")(percept, t)

def make_action_query(self, t):

return expr("ShouldDo(action, %d)" % t)

def make_action_sentence(self, action, t):

return Expr("Did")(action[expr('action')], t)

"""A symbolic mathematical expression. We use this class for logical

def __init__(self, op, *args):

"Op is a string or number; args are Exprs (or are coerced to Exprs)."

assert isinstance(op, str) or (isnumber(op) and not args)

self.op = num_or_str(op)

self.args = map(expr, args) ## Coerce args to Exprs

def __call__(self, *args):

"""Self must be a symbol with no args, such as Expr('F'). Create a new

assert is_symbol(self.op) and not self.args

return Expr(self.op, *args)

def __repr__(self):

"Show something like 'P' or 'P(x, y)', or '~P' or '(P | Q | R)'"

if not self.args: # Constant or proposition with arity 0

return str(self.op)

elif is_symbol(self.op): # Functional or propositional operator

return '%s(%s)' % (self.op, ', '.join(map(repr, self.args)))

elif len(self.args) == 1: # Prefix operator

return self.op + repr(self.args[0])

else: # Infix operator

return '(%s)' % (' '+self.op+' ').join(map(repr, self.args))

def __eq__(self, other):

"""x and y are equal iff their ops and args are equal."""

return (other is self) or (isinstance(other, Expr)

and self.op == other.op and self.args == other.args)

def __ne__(self, other):

return not self.__eq__(other)

def __hash__(self):

"Need a hash method so Exprs can live in dicts."

return hash(self.op) ^ hash(tuple(self.args))

# See http://www.python.org/doc/current/lib/module-operator.html

# Not implemented: not, abs, pos, concat, contains, *item, *slice

def __lt__(self, other): return Expr('<', self, other)

def __le__(self, other): return Expr('<=', self, other)

def __ge__(self, other): return Expr('>=', self, other)

def __gt__(self, other): return Expr('>', self, other)

def __add__(self, other): return Expr('+', self, other)

def __sub__(self, other): return Expr('-', self, other)

def __and__(self, other): return Expr('&', self, other)

def __div__(self, other): return Expr('/', self, other)

def __truediv__(self, other):return Expr('/', self, other)

def __invert__(self): return Expr('~', self)

def __lshift__(self, other): return Expr('<<', self, other)

def __rshift__(self, other): return Expr('>>', self, other)

def __mul__(self, other): return Expr('*', self, other)

def __neg__(self): return Expr('-', self)

def __or__(self, other): return Expr('|', self, other)

def __pow__(self, other): return Expr('**', self, other)

def __xor__(self, other): return Expr('^', self, other)

"""Create an Expr representing a logic expression by parsing the input

if isinstance(s, Expr): return s

if isnumber(s): return Expr(s)

## Replace the alternative spellings of operators with canonical spellings

s = s.replace('==>', '>>').replace('<==', '<<')

s = s.replace('<=>', '%').replace('=/=', '^')

## Replace a symbol or number, such as 'P' with 'Expr("P")'

s = re.sub(r'([a-zA-Z0-9_.]+)', r'Expr("\1")', s)

## Now eval the string. (A security hole; do not use with an adversary.)

"""Return a set of the variables in expression s.

result = set([])

def walk(s):

if is_variable(s):

result.add(s)

else:

for arg in s.args:

walk(arg)

walk(s)

"""returns True for exprs s of the form A & B & ... & C ==> D,

if is_symbol(s.op):

return True

elif s.op == '>>':

antecedent, consequent = s.args

return (is_symbol(consequent.op)

and every(lambda arg: is_symbol(arg.op), conjuncts(antecedent)))

else:

"Return the antecedents and the consequent of a definite clause."

assert is_definite_clause(s)

if is_symbol(s.op):

return [], s

else:

antecedent, consequent = s.args

"""Does kb entail the sentence alpha? Use truth tables. For propositional

assert not variables(alpha)

"Auxiliary routine to implement tt_entails."

if not symbols:

if pl_true(kb, model):

result = pl_true(alpha, model)

assert result in (True, False)

return result

else:

return True

else:

P, rest = symbols[0], symbols[1:]

return (tt_check_all(kb, alpha, rest, extend(model, P, True)) and

"Return a list of all propositional symbols in x."

if not isinstance(x, Expr):

return []

elif is_prop_symbol(x.op):

return [x]

else:

return list(set(symbol for arg in x.args

"""Is the propositional sentence alpha a tautology? (alpha will be

"""Return True if the propositional logic expression is true in the model,

op, args = exp.op, exp.args

if exp == TRUE:

return True

elif exp == FALSE:

return False

elif is_prop_symbol(op):

return model.get(exp)

elif op == '~':

p = pl_true(args[0], model)

if p is None: return None

else: return not p

elif op == '|':

result = False

for arg in args:

p = pl_true(arg, model)

if p is True: return True

if p is None: result = None

return result

elif op == '&':

result = True

for arg in args:

p = pl_true(arg, model)

if p is False: return False

if p is None: result = None

return result

p, q = args

if op == '>>':

return pl_true(~p | q, model)

elif op == '<<':

return pl_true(p | ~q, model)

pt = pl_true(p, model)

if pt is None: return None

qt = pl_true(q, model)

if qt is None: return None

if op == '<=>':

return pt == qt

elif op == '^':

return pt != qt

else:

"""Convert a propositional logical sentence s to conjunctive normal form.

if isinstance(s, str): s = expr(s)

s = eliminate_implications(s) # Steps 1, 2 from p. 253

s = move_not_inwards(s) # Step 3

"""Change >>, <<, and <=> into &, |, and ~. That is, return an Expr

if not s.args or is_symbol(s.op): return s ## (Atoms are unchanged.)

args = map(eliminate_implications, s.args)

a, b = args[0], args[-1]

if s.op == '>>':

return (b | ~a)

elif s.op == '<<':

return (a | ~b)

elif s.op == '<=>':

return (a | ~b) & (b | ~a)

elif s.op == '^':

assert len(args) == 2 ## TODO: relax this restriction

return (a & ~b) | (~a & b)

else:

assert s.op in ('&', '|', '~')

"""Rewrite sentence s by moving negation sign inward.

if s.op == '~':

NOT = lambda b: move_not_inwards(~b)

a = s.args[0]

if a.op == '~': return move_not_inwards(a.args[0]) # ~~A ==> A

if a.op =='&': return associate('|', map(NOT, a.args))

if a.op =='|': return associate('&', map(NOT, a.args))

return s

elif is_symbol(s.op) or not s.args:

return s

else:

"""Given a sentence s consisting of conjunctions and disjunctions

if s.op == '|':

s = associate('|', s.args)

if s.op != '|':

return distribute_and_over_or(s)

if len(s.args) == 0:

return FALSE

if len(s.args) == 1:

return distribute_and_over_or(s.args[0])

conj = find_if((lambda d: d.op == '&'), s.args)

if not conj:

return s

others = [a for a in s.args if a is not conj]

rest = associate('|', others)

return associate('&', [distribute_and_over_or(c|rest)

for c in conj.args])

elif s.op == '&':

return associate('&', map(distribute_and_over_or, s.args))

else:

"""Given an associative op, return an expression with the same

args = dissociate(op, args)

if len(args) == 0:

return _op_identity[op]

elif len(args) == 1:

return args[0]

else:

"""Given an associative op, return a flattened list result such

result = []

def collect(subargs):

for arg in subargs:

if arg.op == op: collect(arg.args)

else: result.append(arg)

collect(args)

"""Return a list of the conjuncts in the sentence s.

"""Return a list of the disjuncts in the sentence s.

"Propositional-logic resolution: say if alpha follows from KB. [Fig. 7.12]"

clauses = KB.clauses + conjuncts(to_cnf(~alpha))

new = set()

while True:

n = len(clauses)

pairs = [(clauses[i], clauses[j])

for i in range(n) for j in range(i+1, n)]

for (ci, cj) in pairs:

resolvents = pl_resolve(ci, cj)

if FALSE in resolvents: return True

new = new.union(set(resolvents))

if new.issubset(set(clauses)): return False

for c in new:

"""Return all clauses that can be obtained by resolving clauses ci and cj.

clauses = []

for di in disjuncts(ci):

for dj in disjuncts(cj):

if di == ~dj or ~di == dj:

dnew = unique(removeall(di, disjuncts(ci)) +

removeall(dj, disjuncts(cj)))

clauses.append(associate('|', dnew))

"A KB of propositional definite clauses."

def tell(self, sentence):

"Add a definite clause to this KB."

assert is_definite_clause(sentence), "Must be definite clause"

self.clauses.append(sentence)

def ask_generator(self, query):

"Yield the empty substitution if KB implies query; else nothing."

if pl_fc_entails(self.clauses, query):

yield {}

def retract(self, sentence):

self.clauses.remove(sentence)

def clauses_with_premise(self, p):

"""Return a list of the clauses in KB that have p in their premise.

return [c for c in self.clauses

"""Use forward chaining to see if a PropDefiniteKB entails symbol q.

count = dict([(c, len(conjuncts(c.args[0]))) for c in KB.clauses

if c.op == '>>'])

inferred = defaultdict(bool)

agenda = [s for s in KB.clauses if is_prop_symbol(s.op)]

while agenda:

p = agenda.pop()

if p == q: return True

if not inferred[p]:

inferred[p] = True

for c in KB.clauses_with_premise(p):

count[c] -= 1

if count[c] == 0:

agenda.append(c.args[1])

"""Check satisfiability of a propositional sentence.

clauses = conjuncts(to_cnf(s))

symbols = prop_symbols(s)

"See if the clauses are true in a partial model."

unknown_clauses = [] ## clauses with an unknown truth value

for c in clauses:

val = pl_true(c, model)

if val == False:

return False

if val != True:

unknown_clauses.append(c)

if not unknown_clauses:

return model

P, value = find_pure_symbol(symbols, unknown_clauses)

if P:

return dpll(clauses, removeall(P, symbols), extend(model, P, value))

P, value = find_unit_clause(clauses, model)

if P:

return dpll(clauses, removeall(P, symbols), extend(model, P, value))

if not symbols:

raise TypeError("Argument should be of the type Expr.")

P, symbols = symbols[0], symbols[1:]

return (dpll(clauses, symbols, extend(model, P, True)) or

"""Find a symbol and its value if it appears only as a positive literal

for s in symbols:

found_pos, found_neg = False, False

for c in clauses:

if not found_pos and s in disjuncts(c): found_pos = True

if not found_neg and ~s in disjuncts(c): found_neg = True

if found_pos != found_neg: return s, found_pos

"""Find a forced assignment if possible from a clause with only 1

for clause in clauses:

P, value = unit_clause_assign(clause, model)

if P: return P, value

"""Return a single variable/value pair that makes clause true in

P, value = None, None

for literal in disjuncts(clause):

sym, positive = inspect_literal(literal)

if sym in model:

if model[sym] == positive:

return None, None # clause already True

elif P:

return None, None # more than 1 unbound variable

else:

P, value = sym, positive

"""The symbol in this literal, and the value it should take to

if literal.op == '~':

return literal.args[0], False

else:

## model is a random assignment of true/false to the symbols in clauses

## See ~/aima1e/print1/manual/knowledge+logic-answers.tex ???

model = dict([(s, random.choice([True, False]))

for s in prop_symbols(clauses)])

for i in range(max_flips):

satisfied, unsatisfied = [], []

for clause in clauses:

(satisfied if pl_true(clause, model) else unsatisfied).append(clause)

if not unsatisfied: ## if model satisfies all the clauses

return model

clause = random.choice(unsatisfied)

if probability(p):

sym = random.choice(prop_symbols(clause))

else:

## Flip the symbol in clause that maximizes number of sat. clauses

raise NotImplementedError

"[Fig. 7.22]"

for t in range(t_max):

cnf = translate_to_SAT(init, transition, goal, t)

model = SAT_solver(cnf)

if model is not False:

return extract_solution(model)

"""Unify expressions x,y with substitution s; return a substitution that

if s is None:

return None

elif x == y:

return s

elif is_variable(x):

return unify_var(x, y, s)

elif is_variable(y):

return unify_var(y, x, s)

elif isinstance(x, Expr) and isinstance(y, Expr):

return unify(x.args, y.args, unify(x.op, y.op, s))

elif isinstance(x, str) or isinstance(y, str):

return None

elif issequence(x) and issequence(y) and len(x) == len(y):

if not x: return s

return unify(x[1:], y[1:], unify(x[0], y[0], s))

else:

if var in s:

return unify(s[var], x, s)

elif occur_check(var, x, s):

return None

else:

"""Return true if variable var occurs anywhere in x

if var == x:

return True

elif is_variable(x) and x in s:

return occur_check(var, s[x], s)

elif isinstance(x, Expr):

return (occur_check(var, x.op, s) or

occur_check(var, x.args, s))

elif isinstance(x, (list, tuple)):

return some(lambda element: occur_check(var, element, s), x)

else:

"""Copy the substitution s and extend it by setting var to val;

s2 = s.copy()

s2[var] = val

"""Substitute the substitution s into the expression x.

if isinstance(x, list):

return [subst(s, xi) for xi in x]

elif isinstance(x, tuple):

return tuple([subst(s, xi) for xi in x])

elif not isinstance(x, Expr):

return x

elif is_var_symbol(x.op):

return s.get(x, x)

else:

"""Inefficient forward chaining for first-order logic. [Fig. 9.3]

while True:

new = {}

for r in KB.clauses:

ps, q = parse_definite_clause(standardize_variables(r))

"""Replace all the variables in sentence with new variables.

if dic is None: dic = {}

if not isinstance(sentence, Expr):

return sentence

elif is_var_symbol(sentence.op):

if sentence in dic:

return dic[sentence]

else:

v = Expr('v_%d' % standardize_variables.counter.next())

dic[sentence] = v

return v

else:

return Expr(sentence.op,

"""A knowledge base consisting of first-order definite clauses.

def __init__(self, initial_clauses=[]):

self.clauses = [] # inefficient: no indexing

for clause in initial_clauses:

self.tell(clause)

def tell(self, sentence):

if is_definite_clause(sentence):

self.clauses.append(sentence)

else:

raise Exception("Not a definite clause: %s" % sentence)

def ask_generator(self, query):

return fol_bc_ask(self, query)

def retract(self, sentence):

self.clauses.remove(sentence)

def fetch_rules_for_goal(self, goal):

q = expr(query)

vars = variables(q)

answers = fol_bc_ask(kb or test_kb, q)

return sorted([pretty(dict((x, v) for x, v in a.items() if x in vars))

for a in answers],

map(expr, ['Farmer(Mac)',

'Rabbit(Pete)',

'Mother(MrsMac, Mac)',

'Mother(MrsRabbit, Pete)',

'(Rabbit(r) & Farmer(f)) ==> Hates(f, r)',

'(Mother(m, c)) ==> Loves(m, c)',

'(Mother(m, r) & Rabbit(r)) ==> Rabbit(m)',

'(Farmer(f)) ==> Human(f)',

# Note that this order of conjuncts

# would result in infinite recursion:

#'(Human(h) & Mother(m, h)) ==> Human(m)'

'(Mother(m, h) & Human(h)) ==> Human(m)'

])

map(expr,

['(American(x) & Weapon(y) & Sells(x, y, z) & Hostile(z)) ==> Criminal(x)',

'Owns(Nono, M1)',

'Missile(M1)',

'(Missile(x) & Owns(Nono, x)) ==> Sells(West, x, Nono)',

'Missile(x) ==> Weapon(x)',

'Enemy(x, America) ==> Hostile(x)',

'American(West)',

'Enemy(Nono, America)'

])

"""A simple backward-chaining algorithm for first-order logic. [Fig. 9.6]

for rule in KB.fetch_rules_for_goal(goal):

lhs, rhs = parse_definite_clause(standardize_variables(rule))

for theta1 in fol_bc_and(KB, lhs, unify(rhs, goal, theta)):

if theta is None:

pass

elif not goals:

yield theta

else:

first, rest = goals[0], goals[1:]

for theta1 in fol_bc_or(KB, subst(theta, first), theta):