February 17, 2025 CS 370 expr and logic¶

Expr¶

In [1]:
from utils4e import *
In [2]:
x = expr('A | B')
x
Out[2]:
(A | B)
In [3]:
type(x)
Out[3]:
utils4e.Expr
In [4]:
x.op
Out[4]:
'|'
In [5]:
x.args
Out[5]:
(A, B)
In [6]:
w = expr('A <== B')
y = expr('A ==> B')
z = expr('A <=> B')
w, y, z
Out[6]:
((A <== B), (A ==> B), (A <=> B))
In [7]:
x1 = expr('(A | B) ==> ~(C & D)')
x1
Out[7]:
((A | B) ==> ~(C & D))

Expr is a recursive data structure.

In [8]:
x1.op
Out[8]:
'==>'
In [9]:
x1.args
Out[9]:
((A | B), ~(C & D))
In [10]:
type(x1.args[0])
Out[10]:
utils4e.Expr
In [11]:
x1.args[0].op
Out[11]:
'|'

expr can also be used for arithmetic expressions¶

In [12]:
[expr('a + b ** c / d'), expr('x - sin(y) * e**x')]
Out[12]:
[(a + ((b ** c) / d)), (x - (sin(y) * (e ** x)))]

This is useful if you are implementing computer algebra systems that perform symbolic mathematics.

PropKB and logic.py¶

We are going to focus on expr objects that represent propositional

In [13]:
from logic import *

We will create an instance of knowledge base for propositional logic.

In [14]:
kb = PropKB()

We add the above propositions to the knowledge base, as clauses.

In [15]:
kb.tell(x)
kb.tell(y)
kb.tell(z)
kb.tell(w)
kb.tell(x1)
In [16]:
kb.clauses
Out[16]:
[x, y, z, (A | ~B), (~A | ~C | ~D), (~B | ~C | ~D)]

Note that the various ==>, <==, and <=> expressions were converted to disjunctive forms, using the or operator: |. That is to make it easier to perform inference.

Rules of inference: Modus Ponens¶

In [17]:
ikb = PropKB()
ikb.tell('A ==> B')
ikb.tell('A')
In [18]:
ikb.clauses
Out[18]:
[(B | ~A), A]
In [19]:
ikb.ask(expr('B'))
Out[19]:
{}

kb.tell() adds a clause to the KB. kb.ask() queries the KB to see if the given clause can be deduced. If the deduction is valid, ask() returns the binding list required to make it true. An empty dictionary, {}, indicates (somewhat obscurely) that no substitution is required. We can avoid this possible confusion by using ask_if_true()

In [20]:
ikb.ask_if_true(expr('B'))
Out[20]:
True
In [21]:
ikb.ask(expr('C'))
Out[21]:
False
In [22]:
ikb.ask_if_true(expr('C'))
Out[22]:
False
In [23]:
ikb.clauses
Out[23]:
[(B | ~A), A]

Note that even though ikb deduced that 'B' is valid, it did not add it to the knowledge base.

In [24]:
ikb.tell('B ==> C')
In [25]:
ikb.clauses
Out[25]:
[(B | ~A), A, (C | ~B)]
In [26]:
ikb.ask(expr('C'))
Out[26]:
{}
In [27]:
ikb.ask_if_true(expr('C'))
Out[27]:
True

And elimination¶

Fixed errors in expr: changed ^ to &

In [28]:
ikb.tell(expr('D & E'))
In [29]:
ikb.clauses
Out[29]:
[(B | ~A), A, (C | ~B), D, E]
In [30]:
ikb.ask(expr('E'))
Out[30]:
{}

It looks like and elimination works now. Let's try and introduction. We first retract the D & E clause.

In [31]:
ikb.retract(expr('D & E'))
ikb.clauses
Out[31]:
[(B | ~A), A, (C | ~B)]
In [32]:
ikb.tell(expr('C'))
ikb.tell(expr('D'))
In [33]:
ikb.clauses
Out[33]:
[(B | ~A), A, (C | ~B), C, D]
In [34]:
ikb.ask(expr('C & D'))
Out[34]:
{}

Good Now we try or introduction.

In [36]:
ikb.ask_if_true(expr('C | B'))
Out[36]:
True
In [37]:
ikb.ask(expr('D | E'))
Out[37]:
{}

Eureka! That works! Now we try doublenegation elimination.

In [38]:
ikb.clauses
Out[38]:
[(B | ~A), A, (C | ~B), C, D]
In [39]:
ikb.tell(expr('~~E'))
In [41]:
ikb.clauses
Out[41]:
[(B | ~A), A, (C | ~B), C, D, E]

It looks like that happened automagically!

Unit Resolution¶

In [42]:
ikb.clauses
Out[42]:
[(B | ~A), A, (C | ~B), C, D, E]
In [43]:
ikb.tell(expr('F | G'))
In [44]:
ikb.clauses
Out[44]:
[(B | ~A), A, (C | ~B), C, D, E, (F | G)]
In [45]:
ikb.tell(expr('~G'))
In [46]:
ikb.ask(expr('F'))
Out[46]:
{}

Great! It works!

Resolution¶

In [47]:
ikb.clauses
Out[47]:
[(B | ~A), A, (C | ~B), C, D, E, (F | G), ~G]
In [48]:
ikb.tell(expr('H | I'))
ikb.tell(expr('~I | J'))
In [49]:
ikb.clauses
Out[49]:
[(B | ~A), A, (C | ~B), C, D, E, (F | G), ~G, (H | I), (~I | J)]
In [50]:
ikb.ask(expr('H | J'))
Out[50]:
{}

Success! This is how resolution works!

Implication is transitive¶

In [52]:
ikb.tell('K ==> L')
ikb.tell('L ==> M')
In [53]:
ikb.clauses
Out[53]:
[(B | ~A),
 A,
 (C | ~B),
 C,
 D,
 E,
 (F | G),
 ~G,
 (H | I),
 (~I | J),
 (L | ~K),
 (M | ~L)]
In [54]:
ikb.ask(expr('K ==> M'))
Out[54]:
{}

This works!

logic.py - details¶

See logic.py

In [55]:
from logic import *

class KB - Knowledge Base¶

class ProbKB(KB) - propositional logic¶

KB_AgentProgram(KB) - a general knowledge-based agent program¶

In [56]:
## must start with letter
is_symbol('R2D2')
Out[56]:
True
In [57]:
is_symbol('123go')
Out[57]:
False
In [58]:
is_symbol('x25')
Out[58]:
True
In [59]:
## must be lower case
is_var_symbol('R2D2')
Out[59]:
False
In [60]:
is_var_symbol('x25')
Out[60]:
True
In [61]:
## must be upper case
is_prop_symbol('R2D2')
Out[61]:
True
In [62]:
is_prop_symbol('x25')
Out[62]:
False
In [63]:
variables(expr('F(x, x) & G(x, y) & H(y, z) & R(A, z, 2)'))
Out[63]:
{x, y, z}
In [64]:
is_definite_clause(expr('Farmer(Mac)'))
Out[64]:
True
In [65]:
parse_definite_clause(expr('Farmer(Mac)'))
Out[65]:
([], Farmer(Mac))
In [66]:
tt_entails(expr('P & Q'), expr('Q'))
Out[66]:
True
In [67]:
tt_entails(expr('P & Q'), expr('R'))
Out[67]:
False
In [68]:
## calls tt_check_all
tt_entails(expr('P | Q'), expr('Q'))
Out[68]:
False
In [69]:
prop_symbols(expr('Farmer(Mac)'))
Out[69]:
{Farmer(Mac)}
In [70]:
prop_symbols(expr('P | Q'))
Out[70]:
{P, Q}
In [71]:
prop_symbols(expr('x | y'))
Out[71]:
set()
In [72]:
constant_symbols(expr('A | B'))
Out[72]:
{A, B}
In [73]:
constant_symbols(expr('x & y'))
Out[73]:
set()
In [74]:
constant_symbols(expr('Farmer(Mac)'))
Out[74]:
{Mac}
In [75]:
## check for tautology
tt_true('P | ~P')
Out[75]:
True
In [76]:
# is propositional logic statement in given model (environment)
pl_true(P, {})
In [77]:
pl_true(P, {}) is None
Out[77]:
True
In [78]:
pl_true(P, {P: True})
Out[78]:
True
In [79]:
pl_true(P, {P: False})
Out[79]:
False
In [80]:
from notebook4e import psource
In [81]:
## check out definition of pl_true
psource(pl_true)


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.
    >>> pl_true(P, {}) is None
    True
    """
    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:
        raise ValueError("illegal operator in logic expression" + str(exp))

to_cnf()¶

Convert an expression to conjunctive normal form (CNF)

In [82]:
to_cnf(expr('A ==> B'))
Out[82]:
(B | ~A)
In [83]:
to_cnf(expr('A <== B'))
Out[83]:
(A | ~B)
In [84]:
to_cnf(expr('A <=> B'))
Out[84]:
((A | ~B) & (B | ~A))
In [85]:
to_cnf(expr('A ^ B'))
Out[85]:
((~A | A) & (B | A) & (~A | ~B) & (B | ~B))
In [86]:
## called by to_cnf()
eliminate_implications(expr('A ==> B'))
Out[86]:
(B | ~A)
In [87]:
## called by to_cnf()
move_not_inwards(~(A | B))
Out[87]:
(~A & ~B)
In [88]:
## called by to_cnf()
distribute_and_over_or((A & B) | C)
Out[88]:
((A | C) & (B | C))

join or flatten with given op

In [89]:
associate('&', [(A&B),(B|C),(B&C)])
Out[89]:
(A & B & (B | C) & B & C)
In [90]:
associate('|', [A|(B|(C|(A&B)))])
Out[90]:
(A | B | C | (A & B))

Given an associative op, return a flattened list result

In [91]:
dissociate('&', [A & B])
Out[91]:
[A, B]

Return a list of the conjuncts in the sentence s.

In [92]:
conjuncts(A & B)
Out[92]:
[A, B]
In [93]:
conjuncts(A | B)
Out[93]:
[(A | B)]

Return a list of the disjuncts in the sentence

In [94]:
disjuncts(A | B)
Out[94]:
[A, B]
In [95]:
disjuncts(A & B)
Out[95]:
[(A & B)]

Propositional-logic resolution: say if alpha follows from KB.

In [97]:
horn_clauses_KB.clauses
Out[97]:
[(P ==> Q),
 ((L & M) ==> P),
 ((B & L) ==> M),
 ((A & P) ==> L),
 ((A & B) ==> L),
 A,
 B]
In [98]:
pl_resolution(horn_clauses_KB, A)
Out[98]:
True

class PropDefiniteKB(PropKB):¶

In [99]:
## Use forward chaining to see if a PropDefiniteKB entails symbol q.
pl_fc_entails(horn_clauses_KB, expr('Q'))
Out[99]:
True

DPLL-Satisfiable¶

In [100]:
dpll_satisfiable(A |'<=>'| B)
Out[100]:
{B: True, A: True}

Walk-SAT [Figure 7.18]¶

In [101]:
WalkSAT([A & ~A], 0.5, 100)
In [102]:
WalkSAT([A & ~A], 0.5, 100) is None
Out[102]:
True
In [103]:
WalkSAT([A | ~A], 0.5, 100)
Out[103]:
{A: True}

skip map coloring and wumpus code¶

unify -- unification algorithm¶

For those of you who took CS 201, this is the boolean function homework problem: match

In [104]:
unify(x, 3, {})
Out[104]:
{x: 3}
In [105]:
unify(x, y, {})
Out[105]:
{x: y}
In [106]:
unify(expr('x & y'), z, {})
Out[106]:
{z: (x & y)}
In [107]:
unify(z, expr('x & y'), {})
Out[107]:
{z: (x & y)}

FolKB(KB) first-order logic knowledge base¶

In [108]:
kb0 = FolKB([expr('Farmer(Mac)'), expr('Rabbit(Pete)'),
              expr('(Rabbit(r) & Farmer(f)) ==> Hates(f, r)')])
In [109]:
kb0.tell(expr('Rabbit(Flopsie)'))
kb0.clauses
Out[109]:
[Farmer(Mac),
 Rabbit(Pete),
 ((Rabbit(r) & Farmer(f)) ==> Hates(f, r)),
 Rabbit(Flopsie)]
In [110]:
kb0.retract(expr('Rabbit(Pete)'))
In [111]:
kb0.clauses
Out[111]:
[Farmer(Mac), ((Rabbit(r) & Farmer(f)) ==> Hates(f, r)), Rabbit(Flopsie)]
In [112]:
kb0.ask(expr('Hates(Mac, x)'))[x]
Out[112]:
Flopsie
In [113]:
kb0.ask(expr('Wife(Pete, x)'))
Out[113]:
False

skip more wumpus¶

differential calculus!¶

In [114]:
## differentiate
diff(x * x, x)
Out[114]:
((x * 1) + (x * 1))
In [115]:
## simplify
simp(diff(x * x, x))
Out[115]:
(2 * x)
In [116]:
## differentiate and then simplify
d(x * x, x)
Out[116]:
(2 * x)
In [117]:
d(x * x - x, x)
Out[117]:
((2 * x) - 1)
In [120]:
d(x * x * x - x, x)
Out[120]:
(((x ** 2) + (x * (2 * x))) - 1)
In [121]:
simp(d(x * x * x - x, x))
Out[121]:
(((x ** 2) + (x * (2 * x))) - 1)

should be 3 * x * x - 1

In [ ]: