Skip to content

Navigation Menu

Sign in
Appearance settings

Search code, repositories, users, issues, pull requests...

Provide feedback

We read every piece of feedback, and take your input very seriously.

Saved searches

Use saved searches to filter your results more quickly
Appearance settings

Commit c3a6fbc

Browse filesBrowse files
dariusdarius
committed
Update logic.py to 3rd edition.
1 parent 1c9a371 commit c3a6fbc
Copy full SHA for c3a6fbc

File tree

Expand file treeCollapse file tree

1 file changed

+67
-113
lines changed
Open diff view settings
Filter options
Expand file treeCollapse file tree

1 file changed

+67
-113
lines changed
Open diff view settings
Collapse file

‎logic.py‎

Copy file name to clipboardExpand all lines: logic.py
+67-113Lines changed: 67 additions & 113 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
"""Representations and Inference for Logic (Chapters 7-10)
1+
"""Representations and Inference for Logic (Chapters 7-9, 12)
22
33
Covers both Propositional and First-Order Logic. First we have four
44
important data types:
@@ -23,12 +23,8 @@
2323
unify Do unification of two FOL sentences
2424
diff, simp Symbolic differentiation and simplification
2525
"""
26-
# (Written for the second edition of AIMA; expect some discrepanciecs
27-
# from the third edition until this gets reviewed.)
2826

29-
from __future__ import generators
30-
import re
31-
import itertools
27+
import itertools, re
3228
import agents
3329
from utils import *
3430

@@ -410,7 +406,7 @@ def pl_true(exp, model={}):
410406

411407
def to_cnf(s):
412408
"""Convert a propositional logical sentence s to conjunctive normal form.
413-
That is, to the form ((A | ~B | ...) & (B | C | ...) & ...) [p. 215]
409+
That is, to the form ((A | ~B | ...) & (B | C | ...) & ...) [p. 253]
414410
>>> to_cnf("~(B|C)")
415411
(~B & ~C)
416412
>>> to_cnf("B <=> (P1|P2)")
@@ -423,7 +419,7 @@ def to_cnf(s):
423419
((D | A | B | C) & (E | A | B | C))
424420
"""
425421
if isinstance(s, str): s = expr(s)
426-
s = eliminate_implications(s) # Steps 1, 2 from p. 215
422+
s = eliminate_implications(s) # Steps 1, 2 from p. 253
427423
s = move_not_inwards(s) # Step 3
428424
return distribute_and_over_or(s) # Step 4
429425

@@ -582,13 +578,11 @@ def pl_resolve(ci, cj):
582578

583579
#______________________________________________________________________________
584580

585-
class PropHornKB(PropKB):
586-
"A KB of propositional Horn clauses."
587-
# Actually definite clauses, but I won't resolve this discrepancy till
588-
# the code upgrade to the 3rd edition.
581+
class PropDefiniteKB(PropKB):
582+
"A KB of propositional definite clauses."
589583

590584
def tell(self, sentence):
591-
"Add a Horn clause to this KB."
585+
"Add a definite clause to this KB."
592586
assert is_definite_clause(sentence), "Must be definite clause"
593587
self.clauses.append(sentence)
594588

@@ -607,37 +601,36 @@ def clauses_with_premise(self, p):
607601
if c.op == '>>' and p in conjuncts(c.args[0])]
608602

609603
def pl_fc_entails(KB, q):
610-
"""Use forward chaining to see if a HornKB entails symbol q. [Fig. 7.14]
604+
"""Use forward chaining to see if a PropDefiniteKB entails symbol q.
605+
[Fig. 7.15]
611606
>>> pl_fc_entails(Fig[7,15], expr('Q'))
612607
True
613608
"""
614609
count = dict([(c, len(conjuncts(c.args[0]))) for c in KB.clauses
615610
if c.op == '>>'])
616611
inferred = DefaultDict(False)
617612
agenda = [s for s in KB.clauses if is_prop_symbol(s.op)]
618-
if q in agenda: return True
619613
while agenda:
620614
p = agenda.pop()
615+
if p == q: return True
621616
if not inferred[p]:
622617
inferred[p] = True
623618
for c in KB.clauses_with_premise(p):
624619
count[c] -= 1
625620
if count[c] == 0:
626-
if c.args[1] == q: return True
627621
agenda.append(c.args[1])
628622
return False
629623

630624
## Wumpus World example [Fig. 7.13]
631625
Fig[7,13] = expr("(B11 <=> (P12 | P21)) & ~B11")
632626

633-
## Propositional Logic Forward Chaining example [Fig. 7.15]
634-
Fig[7,15] = PropHornKB()
627+
## Propositional Logic Forward Chaining example [Fig. 7.16]
628+
Fig[7,15] = PropDefiniteKB()
635629
for s in "P>>Q (L&M)>>P (B&L)>>M (A&P)>>L (A&B)>>L A B".split():
636630
Fig[7,15].tell(expr(s))
637631

638632
#______________________________________________________________________________
639-
640-
# DPLL-Satisfiable [Fig. 7.16]
633+
# DPLL-Satisfiable [Fig. 7.17]
641634

642635
def dpll_satisfiable(s):
643636
"""Check satisfiability of a propositional sentence.
@@ -718,9 +711,8 @@ def literal_symbol(literal):
718711
else:
719712
return literal
720713

721-
722714
#______________________________________________________________________________
723-
# Walk-SAT [Fig. 7.17]
715+
# Walk-SAT [Fig. 7.18]
724716

725717
def WalkSAT(clauses, p=0.5, max_flips=10000):
726718
## model is a random assignment of true/false to the symbols in clauses
@@ -742,45 +734,31 @@ def WalkSAT(clauses, p=0.5, max_flips=10000):
742734
model[sym] = not model[sym]
743735

744736
#______________________________________________________________________________
745-
# PL-Wumpus-Agent [Fig. 7.19]
746737

747-
class PLWumpusAgent(agents.Agent):
738+
class HybridWumpusAgent(agents.Agent):
748739
"An agent for the wumpus world that does logical inference. [Fig. 7.19]"""
749740
def __init__(self):
750-
KB = FolKB() ## shouldn't this be a propositional KB? ***
751-
x, y, orientation = 1, 1, (1, 0)
752-
visited = set() ## squares already visited
753-
plan = []
754-
755-
def program(percept):
756-
stench, breeze, glitter = percept
757-
x, y, orientation = \
758-
update_position(x, y, orientation, program.action)
759-
KB.tell('%sS_%d,%d' % (if_(stench, '', '~'), x, y))
760-
KB.tell('%sB_%d,%d' % (if_(breeze, '', '~'), x, y))
761-
if glitter: program.action = 'Grab'
762-
elif plan: program.action = plan.pop()
763-
else:
764-
for [i, j] in fringe(visited):
765-
if KB.ask('~P_%d,%d & ~W_%d,%d' % (i, j, i, j)) != False:
766-
raise NotImplementedError
767-
KB.ask('~P_%d,%d | ~W_%d,%d' % (i, j, i, j)) != False
768-
if program.action is None:
769-
program.action = random.choice(['Forward', 'Right', 'Left'])
770-
return program.action
771-
772-
program.action = None
773-
774-
agents.Agent.__init__(self, program)
775-
776-
def update_position(x, y, orientation, action):
777-
if action == 'TurnRight':
778-
orientation = turn_right(orientation)
779-
elif action == 'TurnLeft':
780-
orientation = turn_left(orientation)
781-
elif action == 'Forward':
782-
x, y = x + vector_add((x, y), orientation)
783-
return x, y, orientation
741+
unimplemented()
742+
743+
def plan_route(current, goals, allowed):
744+
unimplemented()
745+
746+
#______________________________________________________________________________
747+
748+
def SAT_plan(init, transition, goal, t_max, SAT_solver=dpll_satisfiable):
749+
"[Fig. 7.22]"
750+
for t in range(t_max):
751+
cnf = translate_to_SAT(init, transition, goal, t)
752+
model = SAT_solver(cnf)
753+
if model is not False:
754+
return extract_solution(model)
755+
return None
756+
757+
def translate_to_SAT(init, transition, goal, t):
758+
unimplemented()
759+
760+
def extract_solution(model):
761+
unimplemented()
784762

785763
#______________________________________________________________________________
786764

@@ -868,17 +846,17 @@ def fol_fc_ask(KB, alpha):
868846
while True:
869847
new = {}
870848
for r in KB.clauses:
871-
ps, q = parse_definite_clause(standardize_apart(r))
849+
ps, q = parse_definite_clause(standardize_variables(r))
872850
raise NotImplementedError
873851

874-
def standardize_apart(sentence, dic=None):
852+
def standardize_variables(sentence, dic=None):
875853
"""Replace all the variables in sentence with new variables.
876854
>>> e = expr('F(a, b, c) & G(c, A, 23)')
877-
>>> len(variables(standardize_apart(e)))
855+
>>> len(variables(standardize_variables(e)))
878856
3
879-
>>> variables(e).intersection(variables(standardize_apart(e)))
857+
>>> variables(e).intersection(variables(standardize_variables(e)))
880858
set([])
881-
>>> is_variable(standardize_apart(expr('x')))
859+
>>> is_variable(standardize_variables(expr('x')))
882860
True
883861
"""
884862
if dic is None: dic = {}
@@ -888,14 +866,14 @@ def standardize_apart(sentence, dic=None):
888866
if sentence in dic:
889867
return dic[sentence]
890868
else:
891-
v = Expr('v_%d' % standardize_apart.counter.next())
869+
v = Expr('v_%d' % standardize_variables.counter.next())
892870
dic[sentence] = v
893871
return v
894872
else:
895873
return Expr(sentence.op,
896-
*[standardize_apart(a, dic) for a in sentence.args])
874+
*[standardize_variables(a, dic) for a in sentence.args])
897875

898-
standardize_apart.counter = itertools.count()
876+
standardize_variables.counter = itertools.count()
899877

900878
#______________________________________________________________________________
901879

@@ -922,15 +900,18 @@ def tell(self, sentence):
922900
raise Exception("Not a definite clause: %s" % sentence)
923901

924902
def ask_generator(self, query):
925-
return fol_bc_ask(self, [query])
903+
return fol_bc_ask(self, query)
926904

927905
def retract(self, sentence):
928906
self.clauses.remove(sentence)
929907

908+
def fetch_rules_for_goal(self, goal):
909+
return self.clauses
910+
930911
def test_ask(query, kb=None):
931912
q = expr(query)
932913
vars = variables(q)
933-
answers = fol_bc_ask(kb or test_kb, [q])
914+
answers = fol_bc_ask(kb or test_kb, q)
934915
return sorted([pretty(dict((x, v) for x, v in a.items() if x in vars))
935916
for a in answers],
936917
key=repr)
@@ -964,7 +945,7 @@ def test_ask(query, kb=None):
964945
])
965946
)
966947

967-
def fol_bc_ask(KB, goals, theta={}):
948+
def fol_bc_ask(KB, query):
968949
"""A simple backward-chaining algorithm for first-order logic. [Fig. 9.6]
969950
KB should be an instance of FolKB, and goals a list of literals.
970951
>>> test_ask('Farmer(x)')
@@ -980,51 +961,24 @@ def fol_bc_ask(KB, goals, theta={}):
980961
>>> test_ask('Criminal(x)', crime_kb)
981962
['{x: West}']
982963
"""
983-
if not goals:
964+
return fol_bc_or(KB, query, {})
965+
966+
def fol_bc_or(KB, goal, theta):
967+
for rule in KB.fetch_rules_for_goal(goal):
968+
lhs, rhs = parse_definite_clause(standardize_variables(rule))
969+
for theta1 in fol_bc_and(KB, lhs, unify(rhs, goal, theta)):
970+
yield theta1
971+
972+
def fol_bc_and(KB, goals, theta):
973+
if theta is None:
974+
pass
975+
elif not goals:
984976
yield theta
985-
return
986-
q1 = subst(theta, goals[0])
987-
for r in KB.clauses:
988-
ps, q = parse_definite_clause(standardize_apart(r))
989-
theta1 = unify(q, q1, {})
990-
if theta1 is not None:
991-
new_goals = ps + goals[1:]
992-
for ans in fol_bc_ask(KB, new_goals, subst_compose(theta1, theta)):
993-
yield ans
994-
995-
def subst_compose(s1, s2):
996-
"""Return the substitution which is equivalent to applying s2 to
997-
the result of applying s1 to an expression.
998-
999-
>>> s1 = {x: A, y: B}
1000-
>>> s2 = {z: x, x: C}
1001-
>>> p = F(x) & G(y) & expr('H(z)')
1002-
>>> subst(s1, p)
1003-
((F(A) & G(B)) & H(z))
1004-
>>> subst(s2, p)
1005-
((F(C) & G(y)) & H(x))
1006-
1007-
>>> subst(s2, subst(s1, p))
1008-
((F(A) & G(B)) & H(x))
1009-
>>> subst(subst_compose(s1, s2), p)
1010-
((F(A) & G(B)) & H(x))
1011-
1012-
>>> subst(s1, subst(s2, p))
1013-
((F(C) & G(B)) & H(A))
1014-
>>> subst(subst_compose(s2, s1), p)
1015-
((F(C) & G(B)) & H(A))
1016-
>>> ppsubst(subst_compose(s1, s2))
1017-
{x: A, y: B, z: x}
1018-
>>> ppsubst(subst_compose(s2, s1))
1019-
{x: C, y: B, z: A}
1020-
>>> subst(subst_compose(s1, s2), p) == subst(s2, subst(s1, p))
1021-
True
1022-
>>> subst(subst_compose(s2, s1), p) == subst(s1, subst(s2, p))
1023-
True
1024-
"""
1025-
result = dict((x, s2.get(v, v)) for x, v in s1.items())
1026-
result.update((x, v) for x, v in s2.items() if x not in s1)
1027-
return result
977+
else:
978+
first, rest = goals[0], goals[1:]
979+
for theta1 in fol_bc_or(KB, subst(theta, first), theta):
980+
for theta2 in fol_bc_and(KB, rest, theta1):
981+
yield theta2
1028982

1029983
#______________________________________________________________________________
1030984

0 commit comments

Comments
0 (0)
Morty Proxy This is a proxified and sanitized view of the page, visit original site.