"""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
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.
Then we implement various functions for doing logical inference:
pl_true Evaluate a propositional logical sentence in a model
tt_entails Say if a statement is entailed by a KB
pl_resolution Do resolution on propositional sentences
dpll_satisfiable See if a propositional sentence is satisfiable
WalkSAT (not yet implemented)
And a few other functions:
to_cnf Convert to conjunctive normal form
unify Do unification of two FOL sentences
diff, simp Symbolic differentiation and simplification
"""
import itertools, re
import agents
from utils import *
#______________________________________________________________________________
class KB:
"""A knowledge base to which you can tell and ask sentences.
To create a KB, first subclass this class and implement
tell, ask_generator, and retract. Why ask_generator instead of ask?
The book is a bit vague on what ask means --
For a Propositional Logic KB, ask(P & Q) returns True or False, but for an
FOL KB, something like ask(Brother(x, y)) might return many substitutions
such as {x: Cain, y: Abel}, {x: Abel, y: Cain}, {x: George, y: Jeb}, etc.
So ask_generator generates these one at a time, and ask either returns the
first one or returns False."""
def __init__(self, sentence=None):
abstract
def tell(self, sentence):
"Add the sentence to the KB."
abstract
def ask(self, query):
"""Return a substitution that makes the query true, or,
failing that, return False."""
for result in self.ask_generator(query):
return result
return False
def ask_generator(self, query):
"Yield all the substitutions that make query true."
abstract
def retract(self, sentence):
"Remove sentence from the KB."
abstract
class PropKB(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:
self.clauses.remove(c)
#______________________________________________________________________________
def KB_AgentProgram(KB):
"""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)
return program
#______________________________________________________________________________
class Expr:
"""A symbolic mathematical expression. We use this class for logical
expressions, and for terms within logical expressions. In general, an
Expr has an op (operator) and a list of args. The op can be:
Null-ary (no args) op:
A number, representing the number itself. (e.g. Expr(42) => 42)
A symbol, representing a variable or constant (e.g. Expr('F') => F)
Unary (1 arg) op:
'~', '-', representing NOT, negation (e.g. Expr('~', Expr('P')) => ~P)
Binary (2 arg) op:
'>>', ' y' parses as (x >> y) # Implication
'x R & S')
is ((P & (Q >> R)) & S); so you must use expr('(P & Q) ==> (R & S)').
>>> expr('P Q(1)')
(P Q(1))
>>> expr('P & Q | ~R(x, F(x))')
((P & Q) | ~R(x, F(x)))
"""
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(' Hates(f, r)'))
True
>>> is_definite_clause(expr('(Farmer(f) & ~Rabbit(r)) ==> Hates(f, r)'))
False
>>> is_definite_clause(expr('(Farmer(f) | Rabbit(r)) ==> Hates(f, r)'))
False
"""
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 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:
TRUE, FALSE, ZERO, ONE, TWO = map(Expr, ['TRUE', 'FALSE', 0, 1, 2])
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. [Fig. 7.10]
>>> tt_entails(expr('P & Q'), expr('Q'))
True
"""
assert not variables(alpha)
return tt_check_all(kb, alpha, prop_symbols(kb & alpha), {})
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 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
for symbol in prop_symbols(arg)))
def tt_true(alpha):
"""Is the propositional sentence alpha a tautology? (alpha will be
coerced to an expr.)
>>> tt_true(expr("(P >> Q) (~P | Q)"))
True
"""
return tt_entails(TRUE, expr(alpha))
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."""
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 (b | ~a)
elif s.op == '>> pl_fc_entails(Fig[7,15], expr('Q'))
True
"""
count = dict([(c, len(conjuncts(c.args[0]))) for c in KB.clauses
if c.op == '>>'])
inferred = DefaultDict(False)
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
## Wumpus World example [Fig. 7.13]
Fig[7,13] = expr("(B11 (P12 | P21)) & ~B11")
## Propositional Logic Forward Chaining example [Fig. 7.16]
Fig[7,15] = PropDefiniteKB()
for s in "P>>Q (L&M)>>P (B&L)>>M (A&P)>>L (A&B)>>L A B".split():
Fig[7,15].tell(expr(s))
#______________________________________________________________________________
# DPLL-Satisfiable [Fig. 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.
>>> ppsubst(dpll_satisfiable(A&~B))
{A: True, B: False}
>>> dpll_satisfiable(P&~P)
False
"""
clauses = conjuncts(to_cnf(s))
symbols = 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 == 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))
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 [Fig. 7.18]
def WalkSAT(clauses, p=0.5, max_flips=10000):
## 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:
if_(pl_true(clause, model), satisfied, 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
model[sym] = not model[sym]
#______________________________________________________________________________
class HybridWumpusAgent(agents.Agent):
"An agent for the wumpus world that does logical inference. [Fig. 7.19]"""
def __init__(self):
unimplemented()
def plan_route(current, goals, allowed):
unimplemented()
#______________________________________________________________________________
def SAT_plan(init, transition, goal, t_max, SAT_solver=dpll_satisfiable):
"[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)
return None
def translate_to_SAT(init, transition, goal, t):
unimplemented()
def extract_solution(model):
unimplemented()
#______________________________________________________________________________
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. [Fig. 9.1]
>>> ppsubst(unify(x + y, y + C, {}))
{x: y, y: C}
"""
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 is_var_symbol(x.op)
def unify_var(var, x, s):
if var in s:
return unify(s[var], 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 some(lambda element: occur_check(var, element, s), x)
else:
return False
def extend(s, var, val):
"""Copy the substitution s and extend it by setting var to val;
return copy.
>>> ppsubst(extend({x: 1}, y, 2))
{x: 1, y: 2}
"""
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 fol_fc_ask(KB, alpha):
"""Inefficient forward chaining for first-order logic. [Fig. 9.3]
KB is a FolKB and alpha must be an atomic sentence."""
while True:
new = {}
for r in KB.clauses:
ps, q = parse_definite_clause(standardize_variables(r))
raise NotImplementedError
def standardize_variables(sentence, dic=None):
"""Replace all the variables in sentence with new variables.
>>> e = expr('F(a, b, c) & G(c, A, 23)')
>>> len(variables(standardize_variables(e)))
3
>>> variables(e).intersection(variables(standardize_variables(e)))
set([])
>>> is_variable(standardize_variables(expr('x')))
True
"""
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,
*[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: %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):
return self.clauses
def test_ask(query, kb=None):
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],
key=repr)
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)'
])
)
def fol_bc_ask(KB, query):
"""A simple backward-chaining algorithm for first-order logic. [Fig. 9.6]
KB should be an instance of FolKB, and goals a list of literals.
>>> test_ask('Farmer(x)')
['{x: Mac}']
>>> test_ask('Human(x)')
['{x: Mac}', '{x: MrsMac}']
>>> test_ask('Hates(x, y)')
['{x: Mac, y: MrsRabbit}', '{x: Mac, y: Pete}']
>>> test_ask('Loves(x, y)')
['{x: MrsMac, y: Mac}', '{x: MrsRabbit, y: Pete}']
>>> test_ask('Rabbit(x)')
['{x: MrsRabbit}', '{x: Pete}']
>>> test_ask('Criminal(x)', crime_kb)
['{x: West}']
"""
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
#______________________________________________________________________________
# 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))
>>> simp(diff(x * x, x))
(2 * x)
"""
if y == x: return ONE
elif not y.args: return ZERO
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(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: %s in diff(%s, %s)" % (op, y, x))
def simp(x):
if not x.args: return x
args = map(simp, x.args)
u, op, v = args[0], x.op, args[-1]
if op == '+':
if v == ZERO: return u
if u == ZERO: return v
if u == v: return TWO * u
if u == -v or v == -u: return ZERO
elif op == '-' and len(args) == 1:
if u.op == '-' and len(u.args) == 1: return u.args[0] ## --y ==> y
elif op == '-':
if v == ZERO: return u
if u == ZERO: return -v
if u == v: return ZERO
if u == -v or v == -u: return ZERO
elif op == '*':
if u == ZERO or v == ZERO: return ZERO
if u == ONE: return v
if v == ONE: return u
if u == v: return u ** 2
elif op == '/':
if u == ZERO: return ZERO
if v == ZERO: return Expr('Undefined')
if u == v: return ONE
if u == -v or v == -u: return ZERO
elif op == '**':
if u == ZERO: return ZERO
if v == ZERO: return ONE
if u == ONE: return ONE
if v == ONE: return u
elif op == 'log':
if u == ONE: return ZERO
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))
#_______________________________________________________________________________
# Utilities for doctest cases
# These functions print their arguments in a standard order
# to compensate for the random order in the standard representation
def pretty(x):
t = type(x)
if t is dict: return pretty_dict(x)
elif t is set: return pretty_set(x)
else: return repr(x)
def pretty_dict(d):
"""Return dictionary d's repr but with the items sorted.
>>> pretty_dict({'m': 'M', 'a': 'A', 'r': 'R', 'k': 'K'})
"{'a': 'A', 'k': 'K', 'm': 'M', 'r': 'R'}"
>>> pretty_dict({z: C, y: B, x: A})
'{x: A, y: B, z: C}'
"""
return '{%s}' % ', '.join('%r: %r' % (k, v)
for k, v in sorted(d.items(), key=repr))
def pretty_set(s):
"""Return set s's repr but with the items sorted.
>>> pretty_set(set(['A', 'Q', 'F', 'K', 'Y', 'B']))
"set(['A', 'B', 'F', 'K', 'Q', 'Y'])"
>>> pretty_set(set([z, y, x]))
'set([x, y, z])'
"""
return 'set(%r)' % sorted(s, key=repr)
def pp(x):
print pretty(x)
def ppsubst(s):
"""Pretty-print substitution s"""
ppdict(s)
def ppdict(d):
print pretty_dict(d)
def ppset(s):
print pretty_set(s)
#________________________________________________________________________
class logicTest: """
### PropKB
>>> kb = PropKB()
>>> kb.tell(A & B)
>>> kb.tell(B >> C)
>>> kb.ask(C) ## The result {} means true, with no substitutions
{}
>>> kb.ask(P)
False
>>> kb.retract(B)
>>> kb.ask(C)
False
>>> pl_true(P, {})
>>> pl_true(P | Q, {P: True})
True
# Notice that the function pl_true cannot reason by cases:
>>> pl_true(P | ~P)
# However, tt_true can:
>>> tt_true(P | ~P)
True
# The following are tautologies from [Fig. 7.11]:
>>> tt_true("(A & B) (B & A)")
True
>>> tt_true("(A | B) (B | A)")
True
>>> tt_true("((A & B) & C) (A & (B & C))")
True
>>> tt_true("((A | B) | C) (A | (B | C))")
True
>>> tt_true("~~A A")
True
>>> tt_true("(A >> B) (~B >> ~A)")
True
>>> tt_true("(A >> B) (~A | B)")
True
>>> tt_true("(A B) ((A >> B) & (B >> A))")
True
>>> tt_true("~(A & B) (~A | ~B)")
True
>>> tt_true("~(A | B) (~A & ~B)")
True
>>> tt_true("(A & (B | C)) ((A & B) | (A & C))")
True
>>> tt_true("(A | (B & C)) ((A | B) & (A | C))")
True
# The following are not tautologies:
>>> tt_true(A & ~A)
False
>>> tt_true(A & B)
False
### An earlier version of the code failed on this:
>>> dpll_satisfiable(A & ~B & C & (A | ~D) & (~E | ~D) & (C | ~D) & (~A | ~F) & (E | ~F) & (~D | ~F) & (B | ~C | D) & (A | ~E | F) & (~A | E | D))
{B: False, C: True, A: True, F: False, D: True, E: False}
### [Fig. 7.13]
>>> alpha = expr("~P12")
>>> to_cnf(Fig[7,13] & ~alpha)
((~P12 | B11) & (~P21 | B11) & (P12 | P21 | ~B11) & ~B11 & P12)
>>> tt_entails(Fig[7,13], alpha)
True
>>> pl_resolution(PropKB(Fig[7,13]), alpha)
True
### [Fig. 7.15]
>>> pl_fc_entails(Fig[7,15], expr('SomethingSilly'))
False
### Unification:
>>> unify(x, x, {})
{}
>>> unify(x, 3, {})
{x: 3}
>>> to_cnf((P&Q) | (~P & ~Q))
((~P | P) & (~Q | P) & (~P | Q) & (~Q | Q))
"""