This notebook describes the logic.py module, which covers Chapters 6 (Logical Agents), 7 (First-Order Logic) and 8 (Inference in First-Order Logic) of Artificial Intelligence: A Modern Approach. See the intro notebook for instructions.
We'll start by looking at Expr
, the data type for logical sentences, and the convenience function expr
. We'll be covering two types of knowledge bases, PropKB
- Propositional logic knowledge base and FolKB
- First order logic knowledge base. We will construct a propositional knowledge base of a specific situation in the Wumpus World. We will next go through the tt_entails
function and experiment with it a bit. The pl_resolution
and pl_fc_entails
functions will come next. We'll study forward chaining and backward chaining algorithms for FolKB
and use them on crime_kb
knowledge base.
But the first step is to load the code:
In [1]:
from utils import *
from logic import *
The Expr
class is designed to represent any kind of mathematical expression. The simplest type of Expr
is a symbol, which can be defined with the function Symbol
:
In [2]:
Symbol('x')
Out[2]:
Or we can define multiple symbols at the same time with the function symbols
:
In [3]:
(x, y, P, Q, f) = symbols('x, y, P, Q, f')
We can combine Expr
s with the regular Python infix and prefix operators. Here's how we would form the logical sentence "P and not Q":
In [4]:
P & ~Q
Out[4]:
This works because the Expr
class overloads the &
operator with this definition:
def __and__(self, other): return Expr('&', self, other)
and does similar overloads for the other operators. An Expr
has two fields: op
for the operator, which is always a string, and args
for the arguments, which is a tuple of 0 or more expressions. By "expression," I mean either an instance of Expr
, or a number. Let's take a look at the fields for some Expr
examples:
In [5]:
sentence = P & ~Q
sentence.op
Out[5]:
In [6]:
sentence.args
Out[6]:
In [7]:
P.op
Out[7]:
In [8]:
P.args
Out[8]:
In [9]:
Pxy = P(x, y)
Pxy.op
Out[9]:
In [10]:
Pxy.args
Out[10]:
It is important to note that the Expr
class does not define the logic of Propositional Logic sentences; it just gives you a way to represent expressions. Think of an Expr
as an abstract syntax tree. Each of the args
in an Expr
can be either a symbol, a number, or a nested Expr
. We can nest these trees to any depth. Here is a deply nested Expr
:
In [11]:
3 * f(x, y) + P(y) / 2 + 1
Out[11]:
Here is a table of the operators that can be used to form sentences. Note that we have a problem: we want to use Python operators to make sentences, so that our programs (and our interactive sessions like the one here) will show simple code. But Python does not allow implication arrows as operators, so for now we have to use a more verbose notation that Python does allow: |'==>'|
instead of just ==>
. Alternately, you can always use the more verbose Expr
constructor forms:
Operation | Book | Python Infix Input | Python Output | Python Expr Input |
---|---|---|---|---|
Negation | ¬ P | ~P |
~P |
Expr('~', P) |
And | P ∧ Q | P & Q |
P & Q |
Expr('&', P, Q) |
Or | P ∨ Q | P | Q |
P | Q |
Expr(' |', P, Q) |
Inequality (Xor) | P ≠ Q | P ^ Q |
P ^ Q |
Expr('^', P, Q) |
Implication | P → Q | P |'==>' | Q |
P ==> Q |
Expr('==>', P, Q) |
Reverse Implication | Q ← P | Q |'<==' | P |
Q <== P |
Expr('<==', Q, P) |
Equivalence | P ↔ Q | P |'<=>' | Q |
P <=> Q |
Expr('<=>', P, Q) |
Here's an example of defining a sentence with an implication arrow:
In [12]:
~(P & Q) |'==>'| (~P | ~Q)
Out[12]:
In [13]:
expr('~(P & Q) ==> (~P | ~Q)')
Out[13]:
expr
takes a string as input, and parses it into an Expr
. The string can contain arrow operators: ==>
, <==
, or <=>
, which are handled as if they were regular Python infix operators. And expr
automatically defines any symbols, so you don't need to pre-define them:
In [14]:
expr('sqrt(b ** 2 - 4 * a * c)')
Out[14]:
For now that's all you need to know about expr
. If you are interested, we explain the messy details of how expr
is implemented and how |'==>'|
is handled in the appendix.
PropKB
The class PropKB
can be used to represent a knowledge base of propositional logic sentences.
We see that the class KB
has four methods, apart from __init__
. A point to note here: the ask
method simply calls the ask_generator
method. Thus, this one has already been implemented and what you'll have to actually implement when you create your own knowledge base class (if you want to, though I doubt you'll ever need to; just use the ones we've created for you), will be the ask_generator
function and not the ask
function itself.
The class PropKB
now.
__init__(self, sentence=None)
: The constructor __init__
creates a single field clauses
which will be a list of all the sentences of the knowledge base. Note that each one of these sentences will be a 'clause' i.e. a sentence which is made up of only literals and or
s.tell(self, sentence)
: When you want to add a sentence to the KB, you use the tell
method. This method takes a sentence, converts it to its CNF, extracts all the clauses, and adds all these clauses to the clauses
field. So, you need not worry about tell
ing only clauses to the knowledge base. You can tell
the knowledge base a sentence in any form that you wish; converting it to CNF and adding the resulting clauses will be handled by the tell
method.ask_generator(self, query)
: The ask_generator
function is used by the ask
function. It calls the tt_entails
function, which in turn returns True
if the knowledge base entails query and False
otherwise. The ask_generator
itself returns an empty dict {}
if the knowledge base entails query and None
otherwise. This might seem a little bit weird to you. After all, it makes more sense just to return a True
or a False
instead of the {}
or None
But this is done to maintain consistency with the way things are in First-Order Logic, where, an ask_generator
function, is supposed to return all the substitutions that make the query true. Hence the dict, to return all these substitutions. I will be mostly be using the ask
function which returns a {}
or a False
, but if you don't like this, you can always use the ask_if_true
function which returns a True
or a False
.retract(self, sentence)
: This function removes all the clauses of the sentence given, from the knowledge base. Like the tell
function, you don't have to pass clauses to remove them from the knowledge base; any sentence will do fine. The function will take care of converting that sentence to clauses and then remove those.
In [15]:
wumpus_kb = PropKB()
We define the symbols we use in our clauses.
$P_{x, y}$ is true if there is a pit in [x, y]
.
$B_{x, y}$ is true if the agent senses breeze in [x, y]
.
In [16]:
P11, P12, P21, P22, P31, B11, B21 = expr('P11, P12, P21, P22, P31, B11, B21')
Now we tell sentences based on section 7.4.3
.
There is no pit in [1,1]
.
In [17]:
wumpus_kb.tell(~P11)
A square is breezy if and only if there is a pit in a neighboring square. This has to be stated for each square but for now, we include just the relevant squares.
In [18]:
wumpus_kb.tell(B11 | '<=>' | ((P12 | P21)))
wumpus_kb.tell(B21 | '<=>' | ((P11 | P22 | P31)))
Now we include the breeze percepts for the first two squares leading up to the situation in Figure 7.3(b)
In [19]:
wumpus_kb.tell(~B11)
wumpus_kb.tell(B21)
We can check the clauses stored in a KB
by accessing its clauses
variable
In [20]:
wumpus_kb.clauses
Out[20]:
We see that the equivalence $B_{1, 1} \iff (P_{1, 2} \lor P_{2, 1})$ was automatically converted to two implications which were inturn converted to CNF which is stored in the KB
.
$B_{1, 1} \iff (P_{1, 2} \lor P_{2, 1})$ was split into $B_{1, 1} \implies (P_{1, 2} \lor P_{2, 1})$ and $B_{1, 1} \Longleftarrow (P_{1, 2} \lor P_{2, 1})$.
$B_{1, 1} \implies (P_{1, 2} \lor P_{2, 1})$ was converted to $P_{1, 2} \lor P_{2, 1} \lor \neg B_{1, 1}$.
$B_{1, 1} \Longleftarrow (P_{1, 2} \lor P_{2, 1})$ was converted to $\neg (P_{1, 2} \lor P_{2, 1}) \lor B_{1, 1}$ which becomes $(\neg P_{1, 2} \lor B_{1, 1}) \land (\neg P_{2, 1} \lor B_{1, 1})$ after applying De Morgan's laws and distributing the disjunction.
$B_{2, 1} \iff (P_{1, 1} \lor P_{2, 2} \lor P_{3, 2})$ is converted in similar manner.
In this section we will look at two algorithms to check if a sentence is entailed by the KB
. Our goal is to decide whether $\text{KB} \vDash \alpha$ for some sentence $\alpha$.
It is a model-checking approach which, as the name suggests, enumerates all possible models in which the KB
is true and checks if $\alpha$ is also true in these models. We list the $n$ symbols in the KB
and enumerate the $2^{n}$ models in a depth-first manner and check the truth of KB
and $\alpha$.
In [21]:
%psource tt_check_all
Note that tt_entails()
takes an Expr
which is a conjunction of clauses as the input instead of the KB
itself. You can use the ask_if_true()
method of PropKB
which does all the required conversions. Let's check what wumpus_kb
tells us about $P_{1, 1}$.
In [22]:
wumpus_kb.ask_if_true(~P11), wumpus_kb.ask_if_true(P11)
Out[22]:
Looking at Figure 7.9 we see that in all models in which the knowledge base is True
, $P_{1, 1}$ is False
. It makes sense that ask_if_true()
returns True
for $\alpha = \neg P_{1, 1}$ and False
for $\alpha = P_{1, 1}$. This begs the question, what if $\alpha$ is True
in only a portion of all models. Do we return True
or False
? This doesn't rule out the possibility of $\alpha$ being True
but it is not entailed by the KB
so we return False
in such cases. We can see this is the case for $P_{2, 2}$ and $P_{3, 1}$.
In [23]:
wumpus_kb.ask_if_true(~P22), wumpus_kb.ask_if_true(P22)
Out[23]:
Recall that our goal is to check whether $\text{KB} \vDash \alpha$ i.e. is $\text{KB} \implies \alpha$ true in every model. Suppose we wanted to check if $P \implies Q$ is valid. We check the satisfiability of $\neg (P \implies Q)$, which can be rewritten as $P \land \neg Q$. If $P \land \neg Q$ is unsatisfiable, then $P \implies Q$ must be true in all models. This gives us the result "$\text{KB} \vDash \alpha$ if and only if $\text{KB} \land \neg \alpha$ is unsatisfiable".
This technique corresponds to proof by contradiction, a standard mathematical proof technique. We assume $\alpha$ to be false and show that this leads to a contradiction with known axioms in $\text{KB}$. We obtain a contradiction by making valid inferences using inference rules. In this proof we use a single inference rule, resolution which states $(l_1 \lor \dots \lor l_k) \land (m_1 \lor \dots \lor m_n) \land (l_i \iff \neg m_j) \implies l_1 \lor \dots \lor l_{i - 1} \lor l_{i + 1} \lor \dots \lor l_k \lor m_1 \lor \dots \lor m_{j - 1} \lor m_{j + 1} \lor \dots \lor m_n$. Applying the resolution yeilds us a clause which we add to the KB. We keep doing this until:
In [24]:
%psource pl_resolution
In [25]:
pl_resolution(wumpus_kb, ~P11), pl_resolution(wumpus_kb, P11)
Out[25]:
In [26]:
pl_resolution(wumpus_kb, ~P22), pl_resolution(wumpus_kb, P22)
Out[26]:
FolKB
The class FolKB
can be used to represent a knowledge base of First-order logic sentences. You would initialize and use it the same way as you would for PropKB
except that the clauses are first-order definite clauses. We will see how to write such clauses to create a database and query them in the following sections.
In this section we create a FolKB
based on the following paragraph.
The law says that it is a crime for an American to sell weapons to hostile nations. The country Nono, an enemy of America, has some missiles, and all of its missiles were sold to it by Colonel West, who is American.
The first step is to extract the facts and convert them into first-order definite clauses. Extracting the facts from data alone is a challenging task. Fortnately we have a small paragraph and can do extraction and conversion manually. We'll store the clauses in list aptly named clauses
.
In [27]:
clauses = []
“... it is a crime for an American to sell weapons to hostile nations”
The keywords to look for here are 'crime', 'American', 'sell', 'weapon' and 'hostile'. We use predicate symbols to make meaning of them.
x
is also the American x
who sells weapon y
to z
, which is a hostile nation.
$\text{American}(x) \land \text{Weapon}(y) \land \text{Sells}(x, y, z) \land \text{Hostile}(z) \implies \text{Criminal} (x)$
In [28]:
clauses.append(expr("(American(x) & Weapon(y) & Sells(x, y, z) & Hostile(z)) ==> Criminal(x)"))
"The country Nono, an enemy of America"
We now know that Nono is an enemy of America. We represent these nations using the constant symbols Nono
and America
. the enemy relation is show using the predicate symbol Enemy
.
$\text{Enemy}(\text{Nono}, \text{America})$
In [29]:
clauses.append(expr("Enemy(Nono, America)"))
"Nono ... has some missiles"
This states the existance of some missile which is owned by Nono. $\exists x \text{Owns}(\text{Nono}, x) \land \text{Missile}(x)$. We invoke existential instantiation to introduce a new constant M1
which is the missile owned by Nono.
$\text{Owns}(\text{Nono}, \text{M1}), \text{Missile}(\text{M1})$
In [30]:
clauses.append(expr("Owns(Nono, M1)"))
clauses.append(expr("Missile(M1)"))
"All of its missiles were sold to it by Colonel West"
If Nono owns something and it classifies as a missile, then it was sold to Nono by West.
$\text{Missile}(x) \land \text{Owns}(\text{Nono}, x) \implies \text{Sells}(\text{West}, x, \text{Nono})$
In [31]:
clauses.append(expr("(Missile(x) & Owns(Nono, x)) ==> Sells(West, x, Nono)"))
"West, who is American"
West is an American.
$\text{American}(\text{West})$
In [32]:
clauses.append(expr("American(West)"))
We also know, from our understanding of language, that missiles are weapons and that an enemy of America counts as “hostile”.
$\text{Missile}(x) \implies \text{Weapon}(x), \text{Enemy}(x, \text{America}) \implies \text{Hostile}(x)$
In [33]:
clauses.append(expr("Missile(x) ==> Weapon(x)"))
clauses.append(expr("Enemy(x, America) ==> Hostile(x)"))
Now that we have converted the information into first-order definite clauses we can create our first-order logic knowledge base.
In [34]:
crime_kb = FolKB(clauses)
We sometimes require finding substitutions that make different logical expressions look identical. This process, called unification, is done by the unify
algorithm. It takes as input two sentences and returns a unifier for them if one exists. A unifier is a dictionary which stores the substitutions required to make the two sentences identical. It does so by recursively unifying the components of a sentence, where the unification of a variable symbol var
with a constant symbol Const
is the mapping {var: Const}
. Let's look at a few examples.
In [35]:
unify(expr('x'), 3)
Out[35]:
In [36]:
unify(expr('A(x)'), expr('A(B)'))
Out[36]:
In [37]:
unify(expr('Cat(x) & Dog(Dobby)'), expr('Cat(Bella) & Dog(y)'))
Out[37]:
In cases where there is no possible substitution that unifies the two sentences the function return None
.
In [38]:
print(unify(expr('Cat(x)'), expr('Dog(Dobby)')))
We also need to take care we do not unintentionally use same variable name. Unify treats them as a single variable which prevents it from taking multiple value.
In [39]:
print(unify(expr('Cat(x) & Dog(Dobby)'), expr('Cat(Bella) & Dog(x)')))
We consider the simple forward-chaining algorithm presented in Figure 9.3. We look at each rule in the knoweldge base and see if the premises can be satisfied. This is done by finding a substitution which unifies the each of the premise with a clause in the KB
. If we are able to unify the premises the conclusion (with the corresponding substitution) is added to the KB
. This inferencing process is repeated until either the query can be answered or till no new sentences can be aded. We test if the newly added clause unifies with the query in which case the substitution yielded by unify
is an answer to the query. If we run out of sentences to infer, this means the query was a failure.
The function fol_fc_ask
is a generator which yields all substitutions which validate the query.
In [40]:
%psource fol_fc_ask
Let's find out all the hostile nations. Note that we only told the KB
that Nono was an enemy of America, not that it was hostile.
In [41]:
answer = fol_fc_ask(crime_kb, expr('Hostile(x)'))
print(list(answer))
The generator returned a single substitution which says that Nono is a hostile nation. See how after adding another enemy nation the generator returns two substitutions.
In [42]:
crime_kb.tell(expr('Enemy(JaJa, America)'))
answer = fol_fc_ask(crime_kb, expr('Hostile(x)'))
print(list(answer))
Note: fol_fc_ask
makes changes to the KB
by adding sentences to it.
This algorithm works backward from the goal, chaining through rules to find known facts that support the proof. Suppose goal
is the query we want to find the substitution for. We find rules of the form $\text{lhs} \implies \text{goal}$ in the KB
and try to prove lhs
. There may be multiple clauses in the KB
which give multiple lhs
. It is sufficient to prove only one of these. But to prove a lhs
all the conjuncts in the lhs
of the clause must be proved. This makes it similar to And/Or search.
The OR part of the algorithm comes from our choice to select any clause of the form $\text{lhs} \implies \text{goal}$. Looking at all rules's lhs
whose rhs
unify with the goal
, we yield a substitution which proves all the conjuncts in the lhs
. We use parse_definite_clause
to attain lhs
and rhs
from a clause of the form $\text{lhs} \implies \text{rhs}$. For atomic facts the lhs
is an empty list.
In [43]:
%psource fol_bc_or
In [44]:
%psource fol_bc_and
Now the main function fl_bc_ask
calls fol_bc_or
with substitution initialized as empty. The ask
method of FolKB
uses fol_bc_ask
and fetches the first substitution returned by the generator to answer query. Let's query the knowledge base we created from clauses
to find hostile nations.
In [45]:
# Rebuild KB because running fol_fc_ask would add new facts to the KB
crime_kb = FolKB(clauses)
In [46]:
crime_kb.ask(expr('Hostile(x)'))
Out[46]:
You may notice some new variables in the substitution. They are introduced to standardize the variable names to prevent naming problems as discussed in the Unification section
In [47]:
P |'==>'| ~Q
Out[47]:
What is the funny |'==>'|
syntax? The trick is that "|
" is just the regular Python or-operator, and so is exactly equivalent to this:
In [48]:
(P | '==>') | ~Q
Out[48]:
In other words, there are two applications of or-operators. Here's the first one:
In [49]:
P | '==>'
Out[49]:
What is going on here is that the __or__
method of Expr
serves a dual purpose. If the right-hand-side is another Expr
(or a number), then the result is an Expr
, as in (P | Q)
. But if the right-hand-side is a string, then the string is taken to be an operator, and we create a node in the abstract syntax tree corresponding to a partially-filled Expr
, one where we know the left-hand-side is P
and the operator is ==>
, but we don't yet know the right-hand-side.
The PartialExpr
class has an __or__
method that says to create an Expr
node with the right-hand-side filled in. Here we can see the combination of the PartialExpr
with Q
to create a complete Expr
:
In [50]:
partial = PartialExpr('==>', P)
partial | ~Q
Out[50]:
This trick is due to Ferdinand Jamitzky, with a modification by C. G. Vedant, who suggested using a string inside the or-bars.
expr
How does expr
parse a string into an Expr
? It turns out there are two tricks (besides the Jamitzky/Vedant trick):
==>
" with "|'==>'|
" (and likewise for other operators).eval
the resulting string in an environment in which every identifier
is bound to a symbol with that identifier as the op
.In other words,
In [51]:
expr('~(P & Q) ==> (~P | ~Q)')
Out[51]:
is equivalent to doing:
In [52]:
P, Q = symbols('P, Q')
~(P & Q) |'==>'| (~P | ~Q)
Out[52]:
One thing to beware of: this puts ==>
at the same precedence level as "|"
, which is not quite right. For example, we get this:
In [53]:
P & Q |'==>'| P | Q
Out[53]:
which is probably not what we meant; when in doubt, put in extra parens:
In [54]:
(P & Q) |'==>'| (P | Q)
Out[54]:
In [ ]:
from notebook import Canvas_fol_bc_ask
canvas_bc_ask = Canvas_fol_bc_ask('canvas_bc_ask', crime_kb, expr('Criminal(x)'))
This notebook by Chirag Vartak and Peter Norvig.