Converting strings into expressions. Used in logic.py, planning.py and elsewhere.
from utils import *
x = expr('A | B')
x
type(x)
x.op
x.args
w = expr('A <== B')
y = expr('A ==> B')
z = expr('A <=> B')
w, y, z
x1 = expr('(A | B) ==> ~(C ^ D)')
x1
Expr is a recursive data structure.
x1.op
x1.args
type(x1.args[0])
x1.args[0].op
[expr('a + b ** c / d'), expr('x - sin(y) * e**x')]
This is useful if you are implementing computer algebra systems that perform symbolic mathematics.
We are going to focus on expr objects that represent propositional and first order logic (FOL) expressions.
from logic import *
We will create an instance of knowledge base for propositional logic.
kb = PropKB()
We add the above propositions to the knowledge base, as clauses.
kb.tell(x)
kb.tell(y)
kb.tell(z)
kb.tell(w)
kb.tell(x1)
kb.clauses
Note that the various ==>, <==, and <=> expressions were converts to disjunctive forms, using the or operator: |. That is to make it easier to perform inference.
ikb = PropKB()
ikb.tell('A ==> B')
ikb.tell('A')
ikb.clauses
ikb.ask(expr('B'))
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()
ikb.ask_if_true(expr('B'))
ikb.ask(expr('C'))
ikb.ask_if_true(expr('C'))
ikb.clauses
Note that even though ikb deduced that 'B' is valid, it did not add it to the knowledge base.
Fixed errors in expr: changed ^ to &
ikb.tell(expr('D & E'))
ikb.clauses
ikb.ask(expr('E'))
It looks like and elimination works now. Let's try and introduction. We first retract the D & E clause.
ikb.retract(expr('D & E'))
ikb.clauses
ikb.tell(expr('C'))
ikb.tell(expr('D'))
ikb.clauses
ikb.ask(expr('C & D'))
Good Now we try or introduction.
ikb.ask(expr('C | B'))
ikb.ask(expr('D | E'))
Eureka! That works! Now we try doublenegation elimination.
ikb.clauses
ikb.tell(expr('~~E'))
ikb.clauses
It looks like that happened automagically!
ikb.clauses
ikb.tell(expr('F | G'))
ikb.clauses
ikb.tell(expr('~G'))
ikb.clauses
ikb.ask(expr('F'))
ikb.clauses
ikb.tell(expr('H | I'))
ikb.tell(expr('~I | J'))
ikb.clauses
ikb.ask(expr('H | J'))
Success! This is how resolution works!
ikb.tell('K ==> L')
ikb.tell('L ==> M')
ikb.clauses
ikb.ask(expr('K ==> M'))
This works!