"""Representations and Inference for Logic (Chapters 7-9, 12)
Covers both Propositional and First-Order Logic. First we have four
important data types:
KB Abstract class holds a knowledge base of logical expressions
KB_Agent Abstract class subclasses agents.Agent
Expr A logical expression, imported from utils.py
substitution Implemented as a dictionary of var:value pairs, {x:1, y:x}
Be careful: some functions take an Expr as argument, and some take a KB.
Logical expressions can be created with Expr or expr, imported from utils, TODO
or with expr, which adds the capability to write a string that uses
the connectives ==>, >> variables(expr('F(x, x) & G(x, y) & H(y, z) & R(A, z, 2)')) == {x, y, z}
True
"""
return {x for x in subexpressions(s) if is_variable(x)}
def is_definite_clause(s):
"""Returns True for exprs s of the form A & B & ... & C ==> D,
where all literals are positive. In clause form, this is
~A | ~B | ... | ~C | D, where exactly one clause is positive.
>>> is_definite_clause(expr('Farmer(Mac)'))
True
"""
if is_symbol(s.op):
return True
elif s.op == '==>':
antecedent, consequent = s.args
return (is_symbol(consequent.op) and
all(is_symbol(arg.op) for arg in conjuncts(antecedent)))
else:
return False
def parse_definite_clause(s):
"""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
return conjuncts(antecedent), consequent
# Useful constant Exprs used in examples and code:
A, B, C, D, E, F, G, P, Q, x, y, z = map(Expr, 'ABCDEFGPQxyz')
# ______________________________________________________________________________
def tt_entails(kb, alpha):
"""Does kb entail the sentence alpha? Use truth tables. For propositional
kb's and sentences. [Figure 7.10]. Note that the 'kb' should be an
Expr which is a conjunction of clauses.
>>> tt_entails(expr('P & Q'), expr('Q'))
True
"""
assert not variables(alpha)
symbols = list(prop_symbols(kb & alpha))
return tt_check_all(kb, alpha, symbols, {})
def tt_check_all(kb, alpha, symbols, model):
"""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
tt_check_all(kb, alpha, rest, extend(model, P, False)))
def prop_symbols(x):
"""Return the set of all propositional symbols in x."""
if not isinstance(x, Expr):
return set()
elif is_prop_symbol(x.op):
return {x}
else:
return {symbol for arg in x.args for symbol in prop_symbols(arg)}
def constant_symbols(x):
"""Return the set of all constant symbols in x."""
if not isinstance(x, Expr):
return set()
elif is_prop_symbol(x.op) and not x.args:
return {x}
else:
return {symbol for arg in x.args for symbol in constant_symbols(arg)}
def predicate_symbols(x):
"""Return a set of (symbol_name, arity) in x.
All symbols (even functional) with arity > 0 are considered."""
if not isinstance(x, Expr) or not x.args:
return set()
pred_set = {(x.op, len(x.args))} if is_prop_symbol(x.op) else set()
pred_set.update({symbol for arg in x.args for symbol in predicate_symbols(arg)})
return pred_set
def tt_true(s):
"""Is a propositional sentence a tautology?
>>> tt_true('P | ~P')
True
"""
s = expr(s)
return tt_entails(True, s)
def pl_true(exp, model={}):
"""Return True if the propositional logic expression is true in the model,
and False if it is false. If the model does not specify the value for
every proposition, this may return None to indicate 'not obvious';
this may happen even when the expression is tautological."""
if exp in (True, False):
return exp
op, args = exp.op, exp.args
if 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 b | ~a
elif s.op == '>> pl_fc_entails(horn_clauses_KB, expr('Q'))
True
"""
count = {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])
return False
""" [Figure 7.13]
Simple inference in a wumpus world example
"""
wumpus_world_inference = expr("(B11 (P12 | P21)) & ~B11")
""" [Figure 7.16]
Propositional Logic Forward Chaining example
"""
horn_clauses_KB = PropDefiniteKB()
for s in "P==>Q; (L&M)==>P; (B&L)==>M; (A&P)==>L; (A&B)==>L; A;B".split(';'):
horn_clauses_KB.tell(expr(s))
# ______________________________________________________________________________
# DPLL-Satisfiable [Figure 7.17]
def dpll_satisfiable(s):
"""Check satisfiability of a propositional sentence.
This differs from the book code in two ways: (1) it returns a model
rather than True when it succeeds; this is more useful. (2) The
function find_pure_symbol is passed a list of unknown clauses, rather
than a list of all clauses and the model; this is more efficient."""
clauses = conjuncts(to_cnf(s))
symbols = list(prop_symbols(s))
return dpll(clauses, symbols, {})
def dpll(clauses, symbols, model):
"""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 is False:
return False
if val is not 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
dpll(clauses, symbols, extend(model, P, False)))
def find_pure_symbol(symbols, clauses):
"""Find a symbol and its value if it appears only as a positive literal
(or only as a negative) in clauses.
>>> find_pure_symbol([A, B, C], [A|~B,~B|~C,C|A])
(A, True)
"""
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
return None, None
def find_unit_clause(clauses, model):
"""Find a forced assignment if possible from a clause with only 1
variable not bound in the model.
>>> find_unit_clause([A|B|C, B|~C, ~A|~B], {A:True})
(B, False)
"""
for clause in clauses:
P, value = unit_clause_assign(clause, model)
if P:
return P, value
return None, None
def unit_clause_assign(clause, model):
"""Return a single variable/value pair that makes clause true in
the model, if possible.
>>> unit_clause_assign(A|B|C, {A:True})
(None, None)
>>> unit_clause_assign(B|~C, {A:True})
(None, None)
>>> unit_clause_assign(~A|~B, {A:True})
(B, False)
"""
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
return P, value
def inspect_literal(literal):
"""The symbol in this literal, and the value it should take to
make the literal true.
>>> inspect_literal(P)
(P, True)
>>> inspect_literal(~P)
(P, False)
"""
if literal.op == '~':
return literal.args[0], False
else:
return literal, True
# ______________________________________________________________________________
# Walk-SAT [Figure 7.18]
def WalkSAT(clauses, p=0.5, max_flips=10000):
"""Checks for satisfiability of all clauses by randomly flipping values of variables
"""
# Set of all symbols in all clauses
symbols = {sym for clause in clauses for sym in prop_symbols(clause)}
# model is a random assignment of true/false to the symbols in clauses
model = {s: random.choice([True, False]) for s in symbols}
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(list(prop_symbols(clause)))
else:
# Flip the symbol in clause that maximizes number of sat. clauses
def sat_count(sym):
# Return the the number of clauses satisfied after flipping the symbol.
model[sym] = not model[sym]
count = len([clause for clause in clauses if pl_true(clause, model)])
model[sym] = not model[sym]
return count
sym = argmax(prop_symbols(clause), key=sat_count)
model[sym] = not model[sym]
# If no solution is found within the flip limit, we return failure
return None
# ______________________________________________________________________________
class HybridWumpusAgent(agents.Agent):
"""An agent for the wumpus world that does logical inference. [Figure 7.20]"""
def __init__(self):
raise NotImplementedError
def plan_route(current, goals, allowed):
raise NotImplementedError
# ______________________________________________________________________________
def SAT_plan(init, transition, goal, t_max, SAT_solver=dpll_satisfiable):
"""Converts a planning problem to Satisfaction problem by translating it to a cnf sentence.
[Figure 7.22]"""
# Functions used by SAT_plan
def translate_to_SAT(init, transition, goal, time):
clauses = []
states = [state for state in transition]
# Symbol claiming state s at time t
state_counter = itertools.count()
for s in states:
for t in range(time+1):
state_sym[s, t] = Expr("State_{}".format(next(state_counter)))
# Add initial state axiom
clauses.append(state_sym[init, 0])
# Add goal state axiom
clauses.append(state_sym[goal, time])
# All possible transitions
transition_counter = itertools.count()
for s in states:
for action in transition[s]:
s_ = transition[s][action]
for t in range(time):
# Action 'action' taken from state 's' at time 't' to reach 's_'
action_sym[s, action, t] = Expr(
"Transition_{}".format(next(transition_counter)))
# Change the state from s to s_
clauses.append(action_sym[s, action, t] |'==>'| state_sym[s, t])
clauses.append(action_sym[s, action, t] |'==>'| state_sym[s_, t + 1])
# Allow only one state at any time
for t in range(time+1):
# must be a state at any time
clauses.append(associate('|', [state_sym[s, t] for s in states]))
for s in states:
for s_ in states[states.index(s) + 1:]:
# for each pair of states s, s_ only one is possible at time t
clauses.append((~state_sym[s, t]) | (~state_sym[s_, t]))
# Restrict to one transition per timestep
for t in range(time):
# list of possible transitions at time t
transitions_t = [tr for tr in action_sym if tr[2] == t]
# make sure at least one of the transitions happens
clauses.append(associate('|', [action_sym[tr] for tr in transitions_t]))
for tr in transitions_t:
for tr_ in transitions_t[transitions_t.index(tr) + 1:]:
# there cannot be two transitions tr and tr_ at time t
clauses.append(~action_sym[tr] | ~action_sym[tr_])
# Combine the clauses to form the cnf
return associate('&', clauses)
def extract_solution(model):
true_transitions = [t for t in action_sym if model[action_sym[t]]]
# Sort transitions based on time, which is the 3rd element of the tuple
true_transitions.sort(key=lambda x: x[2])
return [action for s, action, time in true_transitions]
# Body of SAT_plan algorithm
for t in range(t_max):
# dictionaries to help extract the solution from model
state_sym = {}
action_sym = {}
cnf = translate_to_SAT(init, transition, goal, t)
model = SAT_solver(cnf)
if model is not False:
return extract_solution(model)
return None
# ______________________________________________________________________________
def unify(x, y, s={}):
"""Unify expressions x,y with substitution s; return a substitution that
would make x,y equal, or None if x,y can not unify. x and y can be
variables (e.g. Expr('x')), constants, lists, or Exprs. [Figure 9.1]"""
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:
return None
def is_variable(x):
"""A variable is an Expr with no args and a lowercase symbol as the op."""
return isinstance(x, Expr) and not x.args and x.op[0].islower()
def unify_var(var, x, s):
if var in s:
return unify(s[var], x, s)
elif x in s:
return unify(var, s[x], s)
elif occur_check(var, x, s):
return None
else:
return extend(s, var, x)
def occur_check(var, x, s):
"""Return true if variable var occurs anywhere in x
(or in subst(s, x), if s has a binding for 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 first(e for e in x if occur_check(var, e, s))
else:
return False
def extend(s, var, val):
"""Copy the substitution s and extend it by setting var to val; return copy."""
s2 = s.copy()
s2[var] = val
return s2
def subst(s, x):
"""Substitute the substitution s into the expression x.
>>> subst({x: 42, y:0}, F(x) + y)
(F(42) + 0)
"""
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:
return Expr(x.op, *[subst(s, arg) for arg in x.args])
def standardize_variables(sentence, dic=None):
"""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_{}'.format(next(standardize_variables.counter)))
dic[sentence] = v
return v
else:
return Expr(sentence.op,
*[standardize_variables(a, dic) for a in sentence.args])
standardize_variables.counter = itertools.count()
# ______________________________________________________________________________
class FolKB(KB):
"""A knowledge base consisting of first-order definite clauses.
>>> kb0 = FolKB([expr('Farmer(Mac)'), expr('Rabbit(Pete)'),
... expr('(Rabbit(r) & Farmer(f)) ==> Hates(f, r)')])
>>> kb0.tell(expr('Rabbit(Flopsie)'))
>>> kb0.retract(expr('Rabbit(Pete)'))
>>> kb0.ask(expr('Hates(Mac, x)'))[x]
Flopsie
>>> kb0.ask(expr('Wife(Pete, x)'))
False
"""
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: {}".format(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):
return self.clauses
def fol_fc_ask(KB, alpha):
"""A simple forward-chaining algorithm. [Figure 9.3]"""
# TODO: Improve efficiency
kb_consts = list({c for clause in KB.clauses for c in constant_symbols(clause)})
def enum_subst(p):
query_vars = list({v for clause in p for v in variables(clause)})
for assignment_list in itertools.product(kb_consts, repeat=len(query_vars)):
theta = {x: y for x, y in zip(query_vars, assignment_list)}
yield theta
# check if we can answer without new inferences
for q in KB.clauses:
phi = unify(q, alpha, {})
if phi is not None:
yield phi
while True:
new = []
for rule in KB.clauses:
p, q = parse_definite_clause(rule)
for theta in enum_subst(p):
if set(subst(theta, p)).issubset(set(KB.clauses)):
q_ = subst(theta, q)
if all([unify(x, q_, {}) is None for x in KB.clauses + new]):
new.append(q_)
phi = unify(q_, alpha, {})
if phi is not None:
yield phi
if not new:
break
for clause in new:
KB.tell(clause)
return None
def fol_bc_ask(KB, query):
"""A simple backward-chaining algorithm for first-order logic. [Figure 9.6]
KB should be an instance of FolKB, and query an atomic sentence."""
return fol_bc_or(KB, query, {})
def fol_bc_or(KB, goal, theta):
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)):
yield theta1
def fol_bc_and(KB, goals, 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):
for theta2 in fol_bc_and(KB, rest, theta1):
yield theta2
# A simple KB that defines the relevant conditions of the Wumpus World as in Fig 7.4.
# See Sec. 7.4.3
wumpus_kb = PropKB()
P11, P12, P21, P22, P31, B11, B21 = expr('P11, P12, P21, P22, P31, B11, B21')
wumpus_kb.tell(~P11)
wumpus_kb.tell(B11 | '' | ((P12 | P21)))
wumpus_kb.tell(B21 | '' | ((P11 | P22 | P31)))
wumpus_kb.tell(~B11)
wumpus_kb.tell(B21)
test_kb = FolKB(
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)'
]))
crime_kb = FolKB(
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)'
]))
# ______________________________________________________________________________
# Example application (not in the book).
# You can use the Expr class to do symbolic differentiation. This used to be
# a part of AI; now it is considered a separate field, Symbolic Algebra.
def diff(y, x):
"""Return the symbolic derivative, dy/dx, as an Expr.
However, you probably want to simplify the results with simp.
>>> diff(x * x, x)
((x * 1) + (x * 1))
"""
if y == x:
return 1
elif not y.args:
return 0
else:
u, op, v = y.args[0], y.op, y.args[-1]
if op == '+':
return diff(u, x) + diff(v, x)
elif op == '-' and len(y.args) == 1:
return -diff(u, x)
elif op == '-':
return diff(u, x) - diff(v, x)
elif op == '*':
return u * diff(v, x) + v * diff(u, x)
elif op == '/':
return (v * diff(u, x) - u * diff(v, x)) / (v * v)
elif op == '**' and isnumber(x.op):
return (v * u ** (v - 1) * diff(u, x))
elif op == '**':
return (v * u ** (v - 1) * diff(u, x) +
u ** v * Expr('log')(u) * diff(v, x))
elif op == 'log':
return diff(u, x) / u
else:
raise ValueError("Unknown op: {} in diff({}, {})".format(op, y, x))
def simp(x):
"""Simplify the expression x."""
if isnumber(x) or not x.args:
return x
args = list(map(simp, x.args))
u, op, v = args[0], x.op, args[-1]
if op == '+':
if v == 0:
return u
if u == 0:
return v
if u == v:
return 2 * u
if u == -v or v == -u:
return 0
elif op == '-' and len(args) == 1:
if u.op == '-' and len(u.args) == 1:
return u.args[0] # --y ==> y
elif op == '-':
if v == 0:
return u
if u == 0:
return -v
if u == v:
return 0
if u == -v or v == -u:
return 0
elif op == '*':
if u == 0 or v == 0:
return 0
if u == 1:
return v
if v == 1:
return u
if u == v:
return u ** 2
elif op == '/':
if u == 0:
return 0
if v == 0:
return Expr('Undefined')
if u == v:
return 1
if u == -v or v == -u:
return 0
elif op == '**':
if u == 0:
return 0
if v == 0:
return 1
if u == 1:
return 1
if v == 1:
return u
elif op == 'log':
if u == 1:
return 0
else:
raise ValueError("Unknown op: " + op)
# If we fall through to here, we can not simplify further
return Expr(op, *args)
def d(y, x):
"""Differentiate and then simplify."""
return simp(diff(y, x))