Expr

Converting strings into expressions. Used in logic.py, planning.py and elsewhere.

In [1]:
from utils import *
In [2]:
x = expr('A | B')
x
Out[2]:
(A | B)
In [3]:
type(x)
Out[3]:
utils.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]:
utils.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 and first order logic (FOL) expressions.

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), (~A | C | ~D), (~B | C | ~D)]

Note that the various ==>, <==, and <=> expressions were converts 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.

And elimination

Fixed errors in expr: changed ^ to &

In [24]:
ikb.tell(expr('D & E'))
In [25]:
ikb.clauses
Out[25]:
[(B | ~A), A, D, E]
In [26]:
ikb.ask(expr('E'))
Out[26]:
{}

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

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

Good Now we try or introduction.

In [31]:
ikb.ask(expr('C | B'))
Out[31]:
{}
In [32]:
ikb.ask(expr('D | E'))
Out[32]:
{}

Eureka! That works! Now we try doublenegation elimination.

In [33]:
ikb.clauses
Out[33]:
[(B | ~A), A, C, D]
In [34]:
ikb.tell(expr('~~E'))
In [69]:
ikb.clauses
Out[69]:
[(B | ~A), A, C, D, E]

It looks like that happened automagically!

Unit Resolution

In [35]:
ikb.clauses
Out[35]:
[(B | ~A), A, C, D, E]
In [36]:
ikb.tell(expr('F | G'))
In [37]:
ikb.clauses
Out[37]:
[(B | ~A), A, C, D, E, (F | G)]
In [38]:
ikb.tell(expr('~G'))
In [39]:
ikb.clauses
Out[39]:
[(B | ~A), A, C, D, E, (F | G), ~G]
In [40]:
ikb.ask(expr('F'))
Out[40]:
{}
Great! It works!

Resolution

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

Success! This is how resolution works!

Implication is transitive

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

This works!