"""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, failing that, return False."""

return first(self.ask_generator(query), default=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 entails query; else no results."""

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

yield {}

def ask_if_true(self, query):

"""Return True if the KB entails query, else return False."""

for _ in self.ask_generator(query):

return True

return False

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. [Figure 7.1]"""

steps = itertools.count()

def program(percept):

t = next(steps)

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(percept, t):

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

def make_action_query(t):

return expr("ShouldDo(action, {})".format(t))

def make_action_sentence(action, t):

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

"""Return a set of the variables in expression 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

all(is_symbol(arg.op) for arg in 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)

symbols = list(prop_symbols(kb & 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 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 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 a set of (symbol_name, arity) in x.

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

"""Is a propositional sentence a tautology?

s = expr(s)

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

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 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 == '^': # xor or 'not equivalent'

return pt != qt

else:

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

s = expr(s)

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 implications into equivalent form with only &, |, and ~ as logical operators."""

s = expr(s)

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

return s # Atoms are unchanged.

args = list(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.

s = expr(s)

if s.op == '~':

def NOT(b):

return 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('|', list(map(NOT, a.args)))

if a.op == '|':

return associate('&', list(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

s = expr(s)

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 = first(arg for arg in s.args if arg.op == '&')

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('&', list(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. [Figure 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:

if c not in clauses:

"""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 = {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 = list(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 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

"""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:

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

"""An agent for the wumpus world that does logical inference. [Figure 7.20]"""

def __init__(self):

"""Converts a planning problem to Satisfaction problem by translating it to a cnf sentence.

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

"""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 x in s:

return unify(var, s[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 first(e for e in x if occur_check(var, e, s))

else:

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

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:

"""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,

"""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: {}".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):

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

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

for theta2 in fol_bc_and(KB, rest, theta1):

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

'Rabbit(Pete)',

'Mother(MrsMac, Mac)',

'Mother(MrsRabbit, Pete)',