logic.ipynb

{
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {
    "collapsed": true
   },
   "source": [
    "# Logic: `logic.py`; Chapters 6-8"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "This notebook describes the [logic.py](https://github.com/aimacode/aima-python/blob/master/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](http://aima.cs.berkeley.edu)*. See the [intro notebook](https://github.com/aimacode/aima-python/blob/master/intro.ipynb) for instructions.\n",
    "\n",
    "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.\n",
    "\n",
    "But the first step is to load the code:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "metadata": {},
   "outputs": [],
   "source": [
    "from utils import *\n",
    "from logic import *\n",
    "from notebook import psource"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "collapsed": true
   },
   "source": [
    "## Logical Sentences"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "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`:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "x"
      ]
     },
     "execution_count": 2,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "Symbol('x')"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Or we can define multiple symbols at the same time with the function `symbols`:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "metadata": {},
   "outputs": [],
   "source": [
    "(x, y, P, Q, f) = symbols('x, y, P, Q, f')"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "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\":"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "(P & ~Q)"
      ]
     },
     "execution_count": 4,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "P & ~Q"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "This works because the `Expr` class overloads the `&` operator with this definition:\n",
    "\n",
    "```python\n",
    "def __and__(self, other): return Expr('&',  self, other)```\n",
    "     \n",
    "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:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "'&'"
      ]
     },
     "execution_count": 5,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "sentence = P & ~Q\n",
    "\n",
    "sentence.op"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "(P, ~Q)"
      ]
     },
     "execution_count": 6,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "sentence.args"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "'P'"
      ]
     },
     "execution_count": 7,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "P.op"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "()"
      ]
     },
     "execution_count": 8,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "P.args"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 9,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "'P'"
      ]
     },
     "execution_count": 9,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "Pxy = P(x, y)\n",
    "\n",
    "Pxy.op"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 10,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "(x, y)"
      ]
     },
     "execution_count": 10,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "Pxy.args"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "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](https://en.wikipedia.org/wiki/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`:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 11,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "(((3 * f(x, y)) + (P(y) / 2)) + 1)"
      ]
     },
     "execution_count": 11,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "3 * f(x, y) + P(y) / 2 + 1"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Operators for Constructing Logical Sentences\n",
    "\n",
    "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:\n",
    "\n",
    "| Operation                | Book | Python Infix Input | Python Output | Python `Expr` Input\n",
    "|--------------------------|----------------------|-------------------------|---|---|\n",
    "| Negation                 | &not; P      | `~P`                       | `~P` | `Expr('~', P)`\n",
    "| And                      | P &and; Q       | `P & Q`                     | `P & Q` | `Expr('&', P, Q)`\n",
    "| Or                       | P &or; Q | `P`<tt> &#124; </tt>`Q`| `P`<tt> &#124; </tt>`Q` | `Expr('`&#124;`', P, Q)`\n",
    "| Inequality (Xor)         | P &ne; Q     | `P ^ Q`                | `P ^ Q`  | `Expr('^', P, Q)`\n",
    "| Implication                  | P &rarr; Q    | `P` <tt>&#124;</tt>`'==>'`<tt>&#124;</tt> `Q`   | `P ==> Q` | `Expr('==>', P, Q)`\n",
    "| Reverse Implication      | Q &larr; P     | `Q` <tt>&#124;</tt>`'<=='`<tt>&#124;</tt> `P`  |`Q <== P` | `Expr('<==', Q, P)`\n",
    "| Equivalence            | P &harr; Q   | `P` <tt>&#124;</tt>`'<=>'`<tt>&#124;</tt> `Q`   |`P <=> Q` | `Expr('<=>', P, Q)`\n",
    "\n",
    "Here's an example of defining a sentence with an implication arrow:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 12,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "(~(P & Q) ==> (~P | ~Q))"
      ]
     },
     "execution_count": 12,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "~(P & Q)  |'==>'|  (~P | ~Q)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## `expr`: a Shortcut for Constructing Sentences\n",
    "\n",
    "If the `|'==>'|` notation looks ugly to you, you can use the function `expr` instead:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 13,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "(~(P & Q) ==> (~P | ~Q))"
      ]
     },
     "execution_count": 13,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "expr('~(P & Q)  ==>  (~P | ~Q)')"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "`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:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 14,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "sqrt(((b ** 2) - ((4 * a) * c)))"
      ]
     },
     "execution_count": 14,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "expr('sqrt(b ** 2 - 4 * a * c)')"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "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."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Propositional Knowledge Bases: `PropKB`\n",
    "\n",
    "The class `PropKB` can be used to represent a knowledge base of propositional logic sentences.\n",
    "\n",
    "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 (though you'll probably never need to, considering the ones we've created for you) will be the `ask_generator` function and not the `ask` function itself.\n",
    "\n",
    "The class `PropKB` now.\n",
    "* `__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.\n",
    "* `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.\n",
    "* `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`.\n",
    "* `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."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Wumpus World KB\n",
    "Let us create a `PropKB` for the wumpus world with the sentences mentioned in `section 7.4.3`."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 15,
   "metadata": {},
   "outputs": [],
   "source": [
    "wumpus_kb = PropKB()"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "We define the symbols we use in our clauses.<br/>\n",
    "$P_{x, y}$ is true if there is a pit in `[x, y]`.<br/>\n",
    "$B_{x, y}$ is true if the agent senses breeze in `[x, y]`.<br/>"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 16,
   "metadata": {},
   "outputs": [],
   "source": [
    "P11, P12, P21, P22, P31, B11, B21 = expr('P11, P12, P21, P22, P31, B11, B21')"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Now we tell sentences based on `section 7.4.3`.<br/>\n",
    "There is no pit in `[1,1]`."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 17,
   "metadata": {},
   "outputs": [],
   "source": [
    "wumpus_kb.tell(~P11)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "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."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 18,
   "metadata": {},
   "outputs": [],
   "source": [
    "wumpus_kb.tell(B11 | '<=>' | ((P12 | P21)))\n",
    "wumpus_kb.tell(B21 | '<=>' | ((P11 | P22 | P31)))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Now we include the breeze percepts for the first two squares leading up to the situation in `Figure 7.3(b)`"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 19,
   "metadata": {},
   "outputs": [],
   "source": [
    "wumpus_kb.tell(~B11)\n",
    "wumpus_kb.tell(B21)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "We can check the clauses stored in a `KB` by accessing its `clauses` variable"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 20,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "[~P11,\n",
       " (~P12 | B11),\n",
       " (~P21 | B11),\n",
       " (P12 | P21 | ~B11),\n",
       " (~P11 | B21),\n",
       " (~P22 | B21),\n",
       " (~P31 | B21),\n",
       " (P11 | P22 | P31 | ~B21),\n",
       " ~B11,\n",
       " B21]"
      ]
     },
     "execution_count": 20,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "wumpus_kb.clauses"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "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`.<br/>\n",
    "$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})$.<br/>\n",
    "$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}$.<br/>\n",
    "$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.<br/>\n",
    "$B_{2, 1} \\iff (P_{1, 1} \\lor P_{2, 2} \\lor P_{3, 2})$ is converted in similar manner."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Inference in Propositional Knowledge Base\n",
    "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$.\n",
    "### Truth Table Enumeration\n",
    "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$."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 21,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/html": [
       "<!DOCTYPE html PUBLIC \"-//W3C//DTD HTML 4.01//EN\"\n",
       "   \"http://www.w3.org/TR/html4/strict.dtd\">\n",
       "\n",
       "<html>\n",
       "<head>\n",
       "  <title></title>\n",
       "  <meta http-equiv=\"content-type\" content=\"text/html; charset=None\">\n",
       "  <style type=\"text/css\">\n",
       "td.linenos { background-color: #f0f0f0; padding-right: 10px; }\n",
       "span.lineno { background-color: #f0f0f0; padding: 0 5px 0 5px; }\n",
       "pre { line-height: 125%; }\n",
       "body .hll { background-color: #ffffcc }\n",
       "body  { background: #f8f8f8; }\n",
       "body .c { color: #408080; font-style: italic } /* Comment */\n",
       "body .err { border: 1px solid #FF0000 } /* Error */\n",
       "body .k { color: #008000; font-weight: bold } /* Keyword */\n",
       "body .o { color: #666666 } /* Operator */\n",
       "body .ch { color: #408080; font-style: italic } /* Comment.Hashbang */\n",
       "body .cm { color: #408080; font-style: italic } /* Comment.Multiline */\n",
       "body .cp { color: #BC7A00 } /* Comment.Preproc */\n",
       "body .cpf { color: #408080; font-style: italic } /* Comment.PreprocFile */\n",
       "body .c1 { color: #408080; font-style: italic } /* Comment.Single */\n",
       "body .cs { color: #408080; font-style: italic } /* Comment.Special */\n",
       "body .gd { color: #A00000 } /* Generic.Deleted */\n",
       "body .ge { font-style: italic } /* Generic.Emph */\n",
       "body .gr { color: #FF0000 } /* Generic.Error */\n",
       "body .gh { color: #000080; font-weight: bold } /* Generic.Heading */\n",
       "body .gi { color: #00A000 } /* Generic.Inserted */\n",
       "body .go { color: #888888 } /* Generic.Output */\n",
       "body .gp { color: #000080; font-weight: bold } /* Generic.Prompt */\n",
       "body .gs { font-weight: bold } /* Generic.Strong */\n",
       "body .gu { color: #800080; font-weight: bold } /* Generic.Subheading */\n",
       "body .gt { color: #0044DD } /* Generic.Traceback */\n",
       "body .kc { color: #008000; font-weight: bold } /* Keyword.Constant */\n",
       "body .kd { color: #008000; font-weight: bold } /* Keyword.Declaration */\n",
       "body .kn { color: #008000; font-weight: bold } /* Keyword.Namespace */\n",
       "body .kp { color: #008000 } /* Keyword.Pseudo */\n",
       "body .kr { color: #008000; font-weight: bold } /* Keyword.Reserved */\n",
       "body .kt { color: #B00040 } /* Keyword.Type */\n",
       "body .m { color: #666666 } /* Literal.Number */\n",
       "body .s { color: #BA2121 } /* Literal.String */\n",
       "body .na { color: #7D9029 } /* Name.Attribute */\n",
       "body .nb { color: #008000 } /* Name.Builtin */\n",
       "body .nc { color: #0000FF; font-weight: bold } /* Name.Class */\n",
       "body .no { color: #880000 } /* Name.Constant */\n",
       "body .nd { color: #AA22FF } /* Name.Decorator */\n",
       "body .ni { color: #999999; font-weight: bold } /* Name.Entity */\n",
       "body .ne { color: #D2413A; font-weight: bold } /* Name.Exception */\n",
       "body .nf { color: #0000FF } /* Name.Function */\n",
       "body .nl { color: #A0A000 } /* Name.Label */\n",
       "body .nn { color: #0000FF; font-weight: bold } /* Name.Namespace */\n",
       "body .nt { color: #008000; font-weight: bold } /* Name.Tag */\n",
       "body .nv { color: #19177C } /* Name.Variable */\n",
       "body .ow { color: #AA22FF; font-weight: bold } /* Operator.Word */\n",
       "body .w { color: #bbbbbb } /* Text.Whitespace */\n",
       "body .mb { color: #666666 } /* Literal.Number.Bin */\n",
       "body .mf { color: #666666 } /* Literal.Number.Float */\n",
       "body .mh { color: #666666 } /* Literal.Number.Hex */\n",
       "body .mi { color: #666666 } /* Literal.Number.Integer */\n",
       "body .mo { color: #666666 } /* Literal.Number.Oct */\n",
       "body .sa { color: #BA2121 } /* Literal.String.Affix */\n",
       "body .sb { color: #BA2121 } /* Literal.String.Backtick */\n",
       "body .sc { color: #BA2121 } /* Literal.String.Char */\n",
       "body .dl { color: #BA2121 } /* Literal.String.Delimiter */\n",
       "body .sd { color: #BA2121; font-style: italic } /* Literal.String.Doc */\n",
       "body .s2 { color: #BA2121 } /* Literal.String.Double */\n",
       "body .se { color: #BB6622; font-weight: bold } /* Literal.String.Escape */\n",
       "body .sh { color: #BA2121 } /* Literal.String.Heredoc */\n",
       "body .si { color: #BB6688; font-weight: bold } /* Literal.String.Interpol */\n",
       "body .sx { color: #008000 } /* Literal.String.Other */\n",
       "body .sr { color: #BB6688 } /* Literal.String.Regex */\n",
       "body .s1 { color: #BA2121 } /* Literal.String.Single */\n",
       "body .ss { color: #19177C } /* Literal.String.Symbol */\n",
       "body .bp { color: #008000 } /* Name.Builtin.Pseudo */\n",
       "body .fm { color: #0000FF } /* Name.Function.Magic */\n",
       "body .vc { color: #19177C } /* Name.Variable.Class */\n",
       "body .vg { color: #19177C } /* Name.Variable.Global */\n",
       "body .vi { color: #19177C } /* Name.Variable.Instance */\n",
       "body .vm { color: #19177C } /* Name.Variable.Magic */\n",
       "body .il { color: #666666 } /* Literal.Number.Integer.Long */\n",
       "\n",
       "  </style>\n",
       "</head>\n",
       "<body>\n",
       "<h2></h2>\n",
       "\n",
       "<div class=\"highlight\"><pre><span></span><span class=\"k\">def</span> <span class=\"nf\">tt_check_all</span><span class=\"p\">(</span><span class=\"n\">kb</span><span class=\"p\">,</span> <span class=\"n\">alpha</span><span class=\"p\">,</span> <span class=\"n\">symbols</span><span class=\"p\">,</span> <span class=\"n\">model</span><span class=\"p\">):</span>\n",
       "    <span class=\"sd\">&quot;&quot;&quot;Auxiliary routine to implement tt_entails.&quot;&quot;&quot;</span>\n",
       "    <span class=\"k\">if</span> <span class=\"ow\">not</span> <span class=\"n\">symbols</span><span class=\"p\">:</span>\n",
       "        <span class=\"k\">if</span> <span class=\"n\">pl_true</span><span class=\"p\">(</span><span class=\"n\">kb</span><span class=\"p\">,</span> <span class=\"n\">model</span><span class=\"p\">):</span>\n",
       "            <span class=\"n\">result</span> <span class=\"o\">=</span> <span class=\"n\">pl_true</span><span class=\"p\">(</span><span class=\"n\">alpha</span><span class=\"p\">,</span> <span class=\"n\">model</span><span class=\"p\">)</span>\n",
       "            <span class=\"k\">assert</span> <span class=\"n\">result</span> <span class=\"ow\">in</span> <span class=\"p\">(</span><span class=\"bp\">True</span><span class=\"p\">,</span> <span class=\"bp\">False</span><span class=\"p\">)</span>\n",
       "            <span class=\"k\">return</span> <span class=\"n\">result</span>\n",
       "        <span class=\"k\">else</span><span class=\"p\">:</span>\n",
       "            <span class=\"k\">return</span> <span class=\"bp\">True</span>\n",
       "    <span class=\"k\">else</span><span class=\"p\">:</span>\n",
       "        <span class=\"n\">P</span><span class=\"p\">,</span> <span class=\"n\">rest</span> <span class=\"o\">=</span> <span class=\"n\">symbols</span><span class=\"p\">[</span><span class=\"mi\">0</span><span class=\"p\">],</span> <span class=\"n\">symbols</span><span class=\"p\">[</span><span class=\"mi\">1</span><span class=\"p\">:]</span>\n",
       "        <span class=\"k\">return</span> <span class=\"p\">(</span><span class=\"n\">tt_check_all</span><span class=\"p\">(</span><span class=\"n\">kb</span><span class=\"p\">,</span> <span class=\"n\">alpha</span><span class=\"p\">,</span> <span class=\"n\">rest</span><span class=\"p\">,</span> <span class=\"n\">extend</span><span class=\"p\">(</span><span class=\"n\">model</span><span class=\"p\">,</span> <span class=\"n\">P</span><span class=\"p\">,</span> <span class=\"bp\">True</span><span class=\"p\">))</span> <span class=\"ow\">and</span>\n",
       "                <span class=\"n\">tt_check_all</span><span class=\"p\">(</span><span class=\"n\">kb</span><span class=\"p\">,</span> <span class=\"n\">alpha</span><span class=\"p\">,</span> <span class=\"n\">rest</span><span class=\"p\">,</span> <span class=\"n\">extend</span><span class=\"p\">(</span><span class=\"n\">model</span><span class=\"p\">,</span> <span class=\"n\">P</span><span class=\"p\">,</span> <span class=\"bp\">False</span><span class=\"p\">)))</span>\n",
       "</pre></div>\n",
       "</body>\n",
       "</html>\n"
      ],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "psource(tt_check_all)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "The algorithm basically computes every line of the truth table $KB\\implies \\alpha$ and checks if it is true everywhere.\n",
    "<br>\n",
    "If symbols are defined, the routine recursively constructs every combination of truth values for the symbols and then, \n",
    "it checks whether `model` is consistent with `kb`.\n",
    "The given models correspond to the lines in the truth table,\n",
    "which have a `true` in the KB column, \n",
    "and for these lines it checks whether the query evaluates to true\n",
    "<br>\n",
    "`result = pl_true(alpha, model)`.\n",
    "<br>\n",
    "<br>\n",
    "In short, `tt_check_all` evaluates this logical expression for each `model`\n",
    "<br>\n",
    "`pl_true(kb, model) => pl_true(alpha, model)`\n",
    "<br>\n",
    "which is logically equivalent to\n",
    "<br>\n",
    "`pl_true(kb, model) & ~pl_true(alpha, model)` \n",
    "<br>\n",
    "that is, the knowledge base and the negation of the query are logically inconsistent.\n",
    "<br>\n",
    "<br>\n",
    "`tt_entails()` just extracts the symbols from the query and calls `tt_check_all()` with the proper parameters.\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 22,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/html": [
       "<!DOCTYPE html PUBLIC \"-//W3C//DTD HTML 4.01//EN\"\n",
       "   \"http://www.w3.org/TR/html4/strict.dtd\">\n",
       "\n",
       "<html>\n",
       "<head>\n",
       "  <title></title>\n",
       "  <meta http-equiv=\"content-type\" content=\"text/html; charset=None\">\n",
       "  <style type=\"text/css\">\n",
       "td.linenos { background-color: #f0f0f0; padding-right: 10px; }\n",
       "span.lineno { background-color: #f0f0f0; padding: 0 5px 0 5px; }\n",
       "pre { line-height: 125%; }\n",
       "body .hll { background-color: #ffffcc }\n",
       "body  { background: #f8f8f8; }\n",
       "body .c { color: #408080; font-style: italic } /* Comment */\n",
       "body .err { border: 1px solid #FF0000 } /* Error */\n",
       "body .k { color: #008000; font-weight: bold } /* Keyword */\n",
       "body .o { color: #666666 } /* Operator */\n",
       "body .ch { color: #408080; font-style: italic } /* Comment.Hashbang */\n",
       "body .cm { color: #408080; font-style: italic } /* Comment.Multiline */\n",
       "body .cp { color: #BC7A00 } /* Comment.Preproc */\n",
       "body .cpf { color: #408080; font-style: italic } /* Comment.PreprocFile */\n",
       "body .c1 { color: #408080; font-style: italic } /* Comment.Single */\n",
       "body .cs { color: #408080; font-style: italic } /* Comment.Special */\n",
       "body .gd { color: #A00000 } /* Generic.Deleted */\n",
       "body .ge { font-style: italic } /* Generic.Emph */\n",
       "body .gr { color: #FF0000 } /* Generic.Error */\n",
       "body .gh { color: #000080; font-weight: bold } /* Generic.Heading */\n",
       "body .gi { color: #00A000 } /* Generic.Inserted */\n",
       "body .go { color: #888888 } /* Generic.Output */\n",
       "body .gp { color: #000080; font-weight: bold } /* Generic.Prompt */\n",
       "body .gs { font-weight: bold } /* Generic.Strong */\n",
       "body .gu { color: #800080; font-weight: bold } /* Generic.Subheading */\n",
       "body .gt { color: #0044DD } /* Generic.Traceback */\n",
       "body .kc { color: #008000; font-weight: bold } /* Keyword.Constant */\n",
       "body .kd { color: #008000; font-weight: bold } /* Keyword.Declaration */\n",
       "body .kn { color: #008000; font-weight: bold } /* Keyword.Namespace */\n",
       "body .kp { color: #008000 } /* Keyword.Pseudo */\n",
       "body .kr { color: #008000; font-weight: bold } /* Keyword.Reserved */\n",
       "body .kt { color: #B00040 } /* Keyword.Type */\n",
       "body .m { color: #666666 } /* Literal.Number */\n",
       "body .s { color: #BA2121 } /* Literal.String */\n",
       "body .na { color: #7D9029 } /* Name.Attribute */\n",
       "body .nb { color: #008000 } /* Name.Builtin */\n",
       "body .nc { color: #0000FF; font-weight: bold } /* Name.Class */\n",
       "body .no { color: #880000 } /* Name.Constant */\n",
       "body .nd { color: #AA22FF } /* Name.Decorator */\n",
       "body .ni { color: #999999; font-weight: bold } /* Name.Entity */\n",
       "body .ne { color: #D2413A; font-weight: bold } /* Name.Exception */\n",
       "body .nf { color: #0000FF } /* Name.Function */\n",
       "body .nl { color: #A0A000 } /* Name.Label */\n",
       "body .nn { color: #0000FF; font-weight: bold } /* Name.Namespace */\n",
       "body .nt { color: #008000; font-weight: bold } /* Name.Tag */\n",
       "body .nv { color: #19177C } /* Name.Variable */\n",
       "body .ow { color: #AA22FF; font-weight: bold } /* Operator.Word */\n",
       "body .w { color: #bbbbbb } /* Text.Whitespace */\n",
       "body .mb { color: #666666 } /* Literal.Number.Bin */\n",
       "body .mf { color: #666666 } /* Literal.Number.Float */\n",
       "body .mh { color: #666666 } /* Literal.Number.Hex */\n",
       "body .mi { color: #666666 } /* Literal.Number.Integer */\n",
       "body .mo { color: #666666 } /* Literal.Number.Oct */\n",
       "body .sa { color: #BA2121 } /* Literal.String.Affix */\n",
       "body .sb { color: #BA2121 } /* Literal.String.Backtick */\n",
       "body .sc { color: #BA2121 } /* Literal.String.Char */\n",
       "body .dl { color: #BA2121 } /* Literal.String.Delimiter */\n",
       "body .sd { color: #BA2121; font-style: italic } /* Literal.String.Doc */\n",
       "body .s2 { color: #BA2121 } /* Literal.String.Double */\n",
       "body .se { color: #BB6622; font-weight: bold } /* Literal.String.Escape */\n",
       "body .sh { color: #BA2121 } /* Literal.String.Heredoc */\n",
       "body .si { color: #BB6688; font-weight: bold } /* Literal.String.Interpol */\n",
       "body .sx { color: #008000 } /* Literal.String.Other */\n",
       "body .sr { color: #BB6688 } /* Literal.String.Regex */\n",
       "body .s1 { color: #BA2121 } /* Literal.String.Single */\n",
       "body .ss { color: #19177C } /* Literal.String.Symbol */\n",
       "body .bp { color: #008000 } /* Name.Builtin.Pseudo */\n",
       "body .fm { color: #0000FF } /* Name.Function.Magic */\n",
       "body .vc { color: #19177C } /* Name.Variable.Class */\n",
       "body .vg { color: #19177C } /* Name.Variable.Global */\n",
       "body .vi { color: #19177C } /* Name.Variable.Instance */\n",
       "body .vm { color: #19177C } /* Name.Variable.Magic */\n",
       "body .il { color: #666666 } /* Literal.Number.Integer.Long */\n",
       "\n",
       "  </style>\n",
       "</head>\n",
       "<body>\n",
       "<h2></h2>\n",
       "\n",
       "<div class=\"highlight\"><pre><span></span><span class=\"k\">def</span> <span class=\"nf\">tt_entails</span><span class=\"p\">(</span><span class=\"n\">kb</span><span class=\"p\">,</span> <span class=\"n\">alpha</span><span class=\"p\">):</span>\n",
       "    <span class=\"sd\">&quot;&quot;&quot;Does kb entail the sentence alpha? Use truth tables. For propositional</span>\n",
       "<span class=\"sd\">    kb&#39;s and sentences. [Figure 7.10]. Note that the &#39;kb&#39; should be an</span>\n",
       "<span class=\"sd\">    Expr which is a conjunction of clauses.</span>\n",
       "<span class=\"sd\">    &gt;&gt;&gt; tt_entails(expr(&#39;P &amp; Q&#39;), expr(&#39;Q&#39;))</span>\n",
       "<span class=\"sd\">    True</span>\n",
       "<span class=\"sd\">    &quot;&quot;&quot;</span>\n",
       "    <span class=\"k\">assert</span> <span class=\"ow\">not</span> <span class=\"n\">variables</span><span class=\"p\">(</span><span class=\"n\">alpha</span><span class=\"p\">)</span>\n",
       "    <span class=\"n\">symbols</span> <span class=\"o\">=</span> <span class=\"nb\">list</span><span class=\"p\">(</span><span class=\"n\">prop_symbols</span><span class=\"p\">(</span><span class=\"n\">kb</span> <span class=\"o\">&amp;</span> <span class=\"n\">alpha</span><span class=\"p\">))</span>\n",
       "    <span class=\"k\">return</span> <span class=\"n\">tt_check_all</span><span class=\"p\">(</span><span class=\"n\">kb</span><span class=\"p\">,</span> <span class=\"n\">alpha</span><span class=\"p\">,</span> <span class=\"n\">symbols</span><span class=\"p\">,</span> <span class=\"p\">{})</span>\n",
       "</pre></div>\n",
       "</body>\n",
       "</html>\n"
      ],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "psource(tt_entails)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Keep in mind that for two symbols P and Q, P => Q is false only when P is `True` and Q is `False`.\n",
    "Example usage of `tt_entails()`:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 23,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "execution_count": 23,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "tt_entails(P & Q, Q)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "P & Q is True only when both P and Q are True. Hence, (P & Q) => Q is True"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 24,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "False"
      ]
     },
     "execution_count": 24,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "tt_entails(P | Q, Q)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 25,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "False"
      ]
     },
     "execution_count": 25,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "tt_entails(P | Q, P)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "If we know that P | Q is true, we cannot infer the truth values of P and Q. \n",
    "Hence (P | Q) => Q is False and so is (P | Q) => P."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 26,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "execution_count": 26,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "(A, B, C, D, E, F, G) = symbols('A, B, C, D, E, F, G')\n",
    "tt_entails(A & (B | C) & D & E & ~(F | G), A & D & E & ~F & ~G)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "We can see that for the KB to be true, A, D, E have to be True and F and G have to be False.\n",
    "Nothing can be said about B or C."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Coming back to our problem, note that `tt_entails()` takes an `Expr` which is a conjunction of clauses as the input instead of the `KB` itself. \n",
    "You can use the `ask_if_true()` method of `PropKB` which does all the required conversions. \n",
    "Let's check what `wumpus_kb` tells us about $P_{1, 1}$."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 27,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "(True, False)"
      ]
     },
     "execution_count": 27,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "wumpus_kb.ask_if_true(~P11), wumpus_kb.ask_if_true(P11)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "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}$."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 28,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "(False, False)"
      ]
     },
     "execution_count": 28,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "wumpus_kb.ask_if_true(~P22), wumpus_kb.ask_if_true(P22)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Proof by Resolution\n",
    "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$ <em>if and only if</em> $\\text{KB} \\land \\neg \\alpha$ is unsatisfiable\".<br/>\n",
    "This technique corresponds to <em>proof by <strong>contradiction</strong></em>, 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, <strong>resolution</strong> 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:\n",
    "\n",
    "* There are no new clauses that can be added, in which case $\\text{KB} \\nvDash \\alpha$.\n",
    "* Two clauses resolve to yield the <em>empty clause</em>, in which case $\\text{KB} \\vDash \\alpha$.\n",
    "\n",
    "The <em>empty clause</em> is equivalent to <em>False</em> because it arises only from resolving two complementary\n",
    "unit clauses such as $P$ and $\\neg P$ which is a contradiction as both $P$ and $\\neg P$ can't be <em>True</em> at the same time."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "There is  one catch however, the algorithm that implements proof by resolution cannot handle complex sentences. \n",
    "Implications and bi-implications have to be simplified into simpler clauses. \n",
    "We already know that *every sentence of a propositional logic is logically equivalent to a conjunction of clauses*.\n",
    "We will use this fact to our advantage and simplify the input sentence into the **conjunctive normal form** (CNF) which is a conjunction of disjunctions of literals.\n",
    "For eg:\n",
    "<br>\n",
    "$$(A\\lor B)\\land (\\neg B\\lor C\\lor\\neg D)\\land (D\\lor\\neg E)$$\n",
    "This is equivalent to the POS (Product of sums) form in digital electronics.\n",
    "<br>\n",
    "Here's an outline of how the conversion is done:\n",
    "1. Convert bi-implications to implications\n",
    "<br>\n",
    "$\\alpha\\iff\\beta$ can be written as $(\\alpha\\implies\\beta)\\land(\\beta\\implies\\alpha)$\n",
    "<br>\n",
    "This also applies to compound sentences\n",
    "<br>\n",
    "$\\alpha\\iff(\\beta\\lor\\gamma)$ can be written as $(\\alpha\\implies(\\beta\\lor\\gamma))\\land((\\beta\\lor\\gamma)\\implies\\alpha)$\n",
    "<br>\n",
    "2. Convert implications to their logical equivalents\n",
    "<br>\n",
    "$\\alpha\\implies\\beta$ can be written as $\\neg\\alpha\\lor\\beta$\n",
    "<br>\n",
    "3. Move negation inwards\n",
    "<br>\n",
    "CNF requires atomic literals. Hence, negation cannot appear on a compound statement.\n",
    "De Morgan's laws will be helpful here.\n",
    "<br>\n",
    "$\\neg(\\alpha\\land\\beta)\\equiv(\\neg\\alpha\\lor\\neg\\beta)$\n",
    "<br>\n",
    "$\\neg(\\alpha\\lor\\beta)\\equiv(\\neg\\alpha\\land\\neg\\beta)$\n",
    "<br>\n",
    "4. Distribute disjunction over conjunction\n",
    "<br>\n",
    "Disjunction and conjunction are distributive over each other.\n",
    "Now that we only have conjunctions, disjunctions and negations in our expression, \n",
    "we will distribute disjunctions over conjunctions wherever possible as this will give us a sentence which is a conjunction of simpler clauses, \n",
    "which is what we wanted in the first place.\n",
    "<br>\n",
    "We need a term of the form\n",
    "<br>\n",
    "$(\\alpha_{1}\\lor\\alpha_{2}\\lor\\alpha_{3}...)\\land(\\beta_{1}\\lor\\beta_{2}\\lor\\beta_{3}...)\\land(\\gamma_{1}\\lor\\gamma_{2}\\lor\\gamma_{3}...)\\land...$\n",
    "<br>\n",
    "<br>\n",
    "The `to_cnf` function executes this conversion using helper subroutines."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 29,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/html": [
       "<!DOCTYPE html PUBLIC \"-//W3C//DTD HTML 4.01//EN\"\n",
       "   \"http://www.w3.org/TR/html4/strict.dtd\">\n",
       "\n",
       "<html>\n",
       "<head>\n",
       "  <title></title>\n",
       "  <meta http-equiv=\"content-type\" content=\"text/html; charset=None\">\n",
       "  <style type=\"text/css\">\n",
       "td.linenos { background-color: #f0f0f0; padding-right: 10px; }\n",
       "span.lineno { background-color: #f0f0f0; padding: 0 5px 0 5px; }\n",
       "pre { line-height: 125%; }\n",
       "body .hll { background-color: #ffffcc }\n",
       "body  { background: #f8f8f8; }\n",
       "body .c { color: #408080; font-style: italic } /* Comment */\n",
       "body .err { border: 1px solid #FF0000 } /* Error */\n",
       "body .k { color: #008000; font-weight: bold } /* Keyword */\n",
       "body .o { color: #666666 } /* Operator */\n",
       "body .ch { color: #408080; font-style: italic } /* Comment.Hashbang */\n",
       "body .cm { color: #408080; font-style: italic } /* Comment.Multiline */\n",
       "body .cp { color: #BC7A00 } /* Comment.Preproc */\n",
       "body .cpf { color: #408080; font-style: italic } /* Comment.PreprocFile */\n",
       "body .c1 { color: #408080; font-style: italic } /* Comment.Single */\n",
       "body .cs { color: #408080; font-style: italic } /* Comment.Special */\n",
       "body .gd { color: #A00000 } /* Generic.Deleted */\n",
       "body .ge { font-style: italic } /* Generic.Emph */\n",
       "body .gr { color: #FF0000 } /* Generic.Error */\n",
       "body .gh { color: #000080; font-weight: bold } /* Generic.Heading */\n",
       "body .gi { color: #00A000 } /* Generic.Inserted */\n",
       "body .go { color: #888888 } /* Generic.Output */\n",
       "body .gp { color: #000080; font-weight: bold } /* Generic.Prompt */\n",
       "body .gs { font-weight: bold } /* Generic.Strong */\n",
       "body .gu { color: #800080; font-weight: bold } /* Generic.Subheading */\n",
       "body .gt { color: #0044DD } /* Generic.Traceback */\n",
       "body .kc { color: #008000; font-weight: bold } /* Keyword.Constant */\n",
       "body .kd { color: #008000; font-weight: bold } /* Keyword.Declaration */\n",
       "body .kn { color: #008000; font-weight: bold } /* Keyword.Namespace */\n",
       "body .kp { color: #008000 } /* Keyword.Pseudo */\n",
       "body .kr { color: #008000; font-weight: bold } /* Keyword.Reserved */\n",
       "body .kt { color: #B00040 } /* Keyword.Type */\n",
       "body .m { color: #666666 } /* Literal.Number */\n",
       "body .s { color: #BA2121 } /* Literal.String */\n",
       "body .na { color: #7D9029 } /* Name.Attribute */\n",
       "body .nb { color: #008000 } /* Name.Builtin */\n",
       "body .nc { color: #0000FF; font-weight: bold } /* Name.Class */\n",
       "body .no { color: #880000 } /* Name.Constant */\n",
       "body .nd { color: #AA22FF } /* Name.Decorator */\n",
       "body .ni { color: #999999; font-weight: bold } /* Name.Entity */\n",
       "body .ne { color: #D2413A; font-weight: bold } /* Name.Exception */\n",
       "body .nf { color: #0000FF } /* Name.Function */\n",
       "body .nl { color: #A0A000 } /* Name.Label */\n",
       "body .nn { color: #0000FF; font-weight: bold } /* Name.Namespace */\n",
       "body .nt { color: #008000; font-weight: bold } /* Name.Tag */\n",
       "body .nv { color: #19177C } /* Name.Variable */\n",
       "body .ow { color: #AA22FF; font-weight: bold } /* Operator.Word */\n",
       "body .w { color: #bbbbbb } /* Text.Whitespace */\n",
       "body .mb { color: #666666 } /* Literal.Number.Bin */\n",
       "body .mf { color: #666666 } /* Literal.Number.Float */\n",
       "body .mh { color: #666666 } /* Literal.Number.Hex */\n",
       "body .mi { color: #666666 } /* Literal.Number.Integer */\n",
       "body .mo { color: #666666 } /* Literal.Number.Oct */\n",
       "body .sa { color: #BA2121 } /* Literal.String.Affix */\n",
       "body .sb { color: #BA2121 } /* Literal.String.Backtick */\n",
       "body .sc { color: #BA2121 } /* Literal.String.Char */\n",
       "body .dl { color: #BA2121 } /* Literal.String.Delimiter */\n",
       "body .sd { color: #BA2121; font-style: italic } /* Literal.String.Doc */\n",
       "body .s2 { color: #BA2121 } /* Literal.String.Double */\n",
       "body .se { color: #BB6622; font-weight: bold } /* Literal.String.Escape */\n",
       "body .sh { color: #BA2121 } /* Literal.String.Heredoc */\n",
       "body .si { color: #BB6688; font-weight: bold } /* Literal.String.Interpol */\n",
       "body .sx { color: #008000 } /* Literal.String.Other */\n",
       "body .sr { color: #BB6688 } /* Literal.String.Regex */\n",
       "body .s1 { color: #BA2121 } /* Literal.String.Single */\n",
       "body .ss { color: #19177C } /* Literal.String.Symbol */\n",
       "body .bp { color: #008000 } /* Name.Builtin.Pseudo */\n",
       "body .fm { color: #0000FF } /* Name.Function.Magic */\n",
       "body .vc { color: #19177C } /* Name.Variable.Class */\n",
       "body .vg { color: #19177C } /* Name.Variable.Global */\n",
       "body .vi { color: #19177C } /* Name.Variable.Instance */\n",
       "body .vm { color: #19177C } /* Name.Variable.Magic */\n",
       "body .il { color: #666666 } /* Literal.Number.Integer.Long */\n",
       "\n",
       "  </style>\n",
       "</head>\n",
       "<body>\n",
       "<h2></h2>\n",
       "\n",
       "<div class=\"highlight\"><pre><span></span><span class=\"k\">def</span> <span class=\"nf\">to_cnf</span><span class=\"p\">(</span><span class=\"n\">s</span><span class=\"p\">):</span>\n",
       "    <span class=\"sd\">&quot;&quot;&quot;Convert a propositional logical sentence to conjunctive normal form.</span>\n",
       "<span class=\"sd\">    That is, to the form ((A | ~B | ...) &amp; (B | C | ...) &amp; ...) [p. 253]</span>\n",
       "<span class=\"sd\">    &gt;&gt;&gt; to_cnf(&#39;~(B | C)&#39;)</span>\n",
       "<span class=\"sd\">    (~B &amp; ~C)</span>\n",
       "<span class=\"sd\">    &quot;&quot;&quot;</span>\n",
       "    <span class=\"n\">s</span> <span class=\"o\">=</span> <span class=\"n\">expr</span><span class=\"p\">(</span><span class=\"n\">s</span><span class=\"p\">)</span>\n",
       "    <span class=\"k\">if</span> <span class=\"nb\">isinstance</span><span class=\"p\">(</span><span class=\"n\">s</span><span class=\"p\">,</span> <span class=\"nb\">str</span><span class=\"p\">):</span>\n",
       "        <span class=\"n\">s</span> <span class=\"o\">=</span> <span class=\"n\">expr</span><span class=\"p\">(</span><span class=\"n\">s</span><span class=\"p\">)</span>\n",
       "    <span class=\"n\">s</span> <span class=\"o\">=</span> <span class=\"n\">eliminate_implications</span><span class=\"p\">(</span><span class=\"n\">s</span><span class=\"p\">)</span>  <span class=\"c1\"># Steps 1, 2 from p. 253</span>\n",
       "    <span class=\"n\">s</span> <span class=\"o\">=</span> <span class=\"n\">move_not_inwards</span><span class=\"p\">(</span><span class=\"n\">s</span><span class=\"p\">)</span>  <span class=\"c1\"># Step 3</span>\n",
       "    <span class=\"k\">return</span> <span class=\"n\">distribute_and_over_or</span><span class=\"p\">(</span><span class=\"n\">s</span><span class=\"p\">)</span>  <span class=\"c1\"># Step 4</span>\n",
       "</pre></div>\n",
       "</body>\n",
       "</html>\n"
      ],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "psource(to_cnf)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "`to_cnf` calls three subroutines.\n",
    "<br>\n",
    "`eliminate_implications` converts bi-implications and implications to their logical equivalents.\n",
    "<br>\n",
    "`move_not_inwards` removes negations from compound statements and moves them inwards using De Morgan's laws.\n",
    "<br>\n",
    "`distribute_and_over_or` distributes disjunctions over conjunctions.\n",
    "<br>\n",
    "Run the cells below for implementation details.\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 30,
   "metadata": {},
   "outputs": [],
   "source": [
    "%psource eliminate_implications"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 31,
   "metadata": {},
   "outputs": [],
   "source": [
    "%psource move_not_inwards"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 32,
   "metadata": {},
   "outputs": [],
   "source": [
    "%psource distribute_and_over_or"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Let's convert some sentences to see how it works\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 33,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "((A | ~B) & (B | ~A))"
      ]
     },
     "execution_count": 33,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "A, B, C, D = expr('A, B, C, D')\n",
    "to_cnf(A |'<=>'| B)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 34,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "((A | ~B | ~C) & (B | ~A) & (C | ~A))"
      ]
     },
     "execution_count": 34,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "to_cnf(A |'<=>'| (B & C))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 35,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "(A & (C | B) & (D | B))"
      ]
     },
     "execution_count": 35,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "to_cnf(A & (B | (C & D)))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 36,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "((B | ~A | C | ~D) & (A | ~A | C | ~D) & (B | ~B | C | ~D) & (A | ~B | C | ~D))"
      ]
     },
     "execution_count": 36,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "to_cnf((A |'<=>'| ~B) |'==>'| (C | ~D))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Coming back to our resolution problem, we can see how the `to_cnf` function is utilized here"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 37,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/html": [
       "<!DOCTYPE html PUBLIC \"-//W3C//DTD HTML 4.01//EN\"\n",
       "   \"http://www.w3.org/TR/html4/strict.dtd\">\n",
       "\n",
       "<html>\n",
       "<head>\n",
       "  <title></title>\n",
       "  <meta http-equiv=\"content-type\" content=\"text/html; charset=None\">\n",
       "  <style type=\"text/css\">\n",
       "td.linenos { background-color: #f0f0f0; padding-right: 10px; }\n",
       "span.lineno { background-color: #f0f0f0; padding: 0 5px 0 5px; }\n",
       "pre { line-height: 125%; }\n",
       "body .hll { background-color: #ffffcc }\n",
       "body  { background: #f8f8f8; }\n",
       "body .c { color: #408080; font-style: italic } /* Comment */\n",
       "body .err { border: 1px solid #FF0000 } /* Error */\n",
       "body .k { color: #008000; font-weight: bold } /* Keyword */\n",
       "body .o { color: #666666 } /* Operator */\n",
       "body .ch { color: #408080; font-style: italic } /* Comment.Hashbang */\n",
       "body .cm { color: #408080; font-style: italic } /* Comment.Multiline */\n",
       "body .cp { color: #BC7A00 } /* Comment.Preproc */\n",
       "body .cpf { color: #408080; font-style: italic } /* Comment.PreprocFile */\n",
       "body .c1 { color: #408080; font-style: italic } /* Comment.Single */\n",
       "body .cs { color: #408080; font-style: italic } /* Comment.Special */\n",
       "body .gd { color: #A00000 } /* Generic.Deleted */\n",
       "body .ge { font-style: italic } /* Generic.Emph */\n",
       "body .gr { color: #FF0000 } /* Generic.Error */\n",
       "body .gh { color: #000080; font-weight: bold } /* Generic.Heading */\n",
       "body .gi { color: #00A000 } /* Generic.Inserted */\n",
       "body .go { color: #888888 } /* Generic.Output */\n",
       "body .gp { color: #000080; font-weight: bold } /* Generic.Prompt */\n",
       "body .gs { font-weight: bold } /* Generic.Strong */\n",
       "body .gu { color: #800080; font-weight: bold } /* Generic.Subheading */\n",
       "body .gt { color: #0044DD } /* Generic.Traceback */\n",
       "body .kc { color: #008000; font-weight: bold } /* Keyword.Constant */\n",
       "body .kd { color: #008000; font-weight: bold } /* Keyword.Declaration */\n",
       "body .kn { color: #008000; font-weight: bold } /* Keyword.Namespace */\n",
       "body .kp { color: #008000 } /* Keyword.Pseudo */\n",
       "body .kr { color: #008000; font-weight: bold } /* Keyword.Reserved */\n",
       "body .kt { color: #B00040 } /* Keyword.Type */\n",
       "body .m { color: #666666 } /* Literal.Number */\n",
       "body .s { color: #BA2121 } /* Literal.String */\n",
       "body .na { color: #7D9029 } /* Name.Attribute */\n",
       "body .nb { color: #008000 } /* Name.Builtin */\n",
       "body .nc { color: #0000FF; font-weight: bold } /* Name.Class */\n",
       "body .no { color: #880000 } /* Name.Constant */\n",
       "body .nd { color: #AA22FF } /* Name.Decorator */\n",
       "body .ni { color: #999999; font-weight: bold } /* Name.Entity */\n",
       "body .ne { color: #D2413A; font-weight: bold } /* Name.Exception */\n",
       "body .nf { color: #0000FF } /* Name.Function */\n",
       "body .nl { color: #A0A000 } /* Name.Label */\n",
       "body .nn { color: #0000FF; font-weight: bold } /* Name.Namespace */\n",
       "body .nt { color: #008000; font-weight: bold } /* Name.Tag */\n",
       "body .nv { color: #19177C } /* Name.Variable */\n",
       "body .ow { color: #AA22FF; font-weight: bold } /* Operator.Word */\n",
       "body .w { color: #bbbbbb } /* Text.Whitespace */\n",
       "body .mb { color: #666666 } /* Literal.Number.Bin */\n",
       "body .mf { color: #666666 } /* Literal.Number.Float */\n",
       "body .mh { color: #666666 } /* Literal.Number.Hex */\n",
       "body .mi { color: #666666 } /* Literal.Number.Integer */\n",
       "body .mo { color: #666666 } /* Literal.Number.Oct */\n",
       "body .sa { color: #BA2121 } /* Literal.String.Affix */\n",
       "body .sb { color: #BA2121 } /* Literal.String.Backtick */\n",
       "body .sc { color: #BA2121 } /* Literal.String.Char */\n",
       "body .dl { color: #BA2121 } /* Literal.String.Delimiter */\n",
       "body .sd { color: #BA2121; font-style: italic } /* Literal.String.Doc */\n",
       "body .s2 { color: #BA2121 } /* Literal.String.Double */\n",
       "body .se { color: #BB6622; font-weight: bold } /* Literal.String.Escape */\n",
       "body .sh { color: #BA2121 } /* Literal.String.Heredoc */\n",
       "body .si { color: #BB6688; font-weight: bold } /* Literal.String.Interpol */\n",
       "body .sx { color: #008000 } /* Literal.String.Other */\n",
       "body .sr { color: #BB6688 } /* Literal.String.Regex */\n",
       "body .s1 { color: #BA2121 } /* Literal.String.Single */\n",
       "body .ss { color: #19177C } /* Literal.String.Symbol */\n",
       "body .bp { color: #008000 } /* Name.Builtin.Pseudo */\n",
       "body .fm { color: #0000FF } /* Name.Function.Magic */\n",
       "body .vc { color: #19177C } /* Name.Variable.Class */\n",
       "body .vg { color: #19177C } /* Name.Variable.Global */\n",
       "body .vi { color: #19177C } /* Name.Variable.Instance */\n",
       "body .vm { color: #19177C } /* Name.Variable.Magic */\n",
       "body .il { color: #666666 } /* Literal.Number.Integer.Long */\n",
       "\n",
       "  </style>\n",
       "</head>\n",
       "<body>\n",
       "<h2></h2>\n",
       "\n",
       "<div class=\"highlight\"><pre><span></span><span class=\"k\">def</span> <span class=\"nf\">pl_resolution</span><span class=\"p\">(</span><span class=\"n\">KB</span><span class=\"p\">,</span> <span class=\"n\">alpha</span><span class=\"p\">):</span>\n",
       "    <span class=\"sd\">&quot;&quot;&quot;Propositional-logic resolution: say if alpha follows from KB. [Figure 7.12]&quot;&quot;&quot;</span>\n",
       "    <span class=\"n\">clauses</span> <span class=\"o\">=</span> <span class=\"n\">KB</span><span class=\"o\">.</span><span class=\"n\">clauses</span> <span class=\"o\">+</span> <span class=\"n\">conjuncts</span><span class=\"p\">(</span><span class=\"n\">to_cnf</span><span class=\"p\">(</span><span class=\"o\">~</span><span class=\"n\">alpha</span><span class=\"p\">))</span>\n",
       "    <span class=\"n\">new</span> <span class=\"o\">=</span> <span class=\"nb\">set</span><span class=\"p\">()</span>\n",
       "    <span class=\"k\">while</span> <span class=\"bp\">True</span><span class=\"p\">:</span>\n",
       "        <span class=\"n\">n</span> <span class=\"o\">=</span> <span class=\"nb\">len</span><span class=\"p\">(</span><span class=\"n\">clauses</span><span class=\"p\">)</span>\n",
       "        <span class=\"n\">pairs</span> <span class=\"o\">=</span> <span class=\"p\">[(</span><span class=\"n\">clauses</span><span class=\"p\">[</span><span class=\"n\">i</span><span class=\"p\">],</span> <span class=\"n\">clauses</span><span class=\"p\">[</span><span class=\"n\">j</span><span class=\"p\">])</span>\n",
       "                 <span class=\"k\">for</span> <span class=\"n\">i</span> <span class=\"ow\">in</span> <span class=\"nb\">range</span><span class=\"p\">(</span><span class=\"n\">n</span><span class=\"p\">)</span> <span class=\"k\">for</span> <span class=\"n\">j</span> <span class=\"ow\">in</span> <span class=\"nb\">range</span><span class=\"p\">(</span><span class=\"n\">i</span><span class=\"o\">+</span><span class=\"mi\">1</span><span class=\"p\">,</span> <span class=\"n\">n</span><span class=\"p\">)]</span>\n",
       "        <span class=\"k\">for</span> <span class=\"p\">(</span><span class=\"n\">ci</span><span class=\"p\">,</span> <span class=\"n\">cj</span><span class=\"p\">)</span> <span class=\"ow\">in</span> <span class=\"n\">pairs</span><span class=\"p\">:</span>\n",
       "            <span class=\"n\">resolvents</span> <span class=\"o\">=</span> <span class=\"n\">pl_resolve</span><span class=\"p\">(</span><span class=\"n\">ci</span><span class=\"p\">,</span> <span class=\"n\">cj</span><span class=\"p\">)</span>\n",
       "            <span class=\"k\">if</span> <span class=\"bp\">False</span> <span class=\"ow\">in</span> <span class=\"n\">resolvents</span><span class=\"p\">:</span>\n",
       "                <span class=\"k\">return</span> <span class=\"bp\">True</span>\n",
       "            <span class=\"n\">new</span> <span class=\"o\">=</span> <span class=\"n\">new</span><span class=\"o\">.</span><span class=\"n\">union</span><span class=\"p\">(</span><span class=\"nb\">set</span><span class=\"p\">(</span><span class=\"n\">resolvents</span><span class=\"p\">))</span>\n",
       "        <span class=\"k\">if</span> <span class=\"n\">new</span><span class=\"o\">.</span><span class=\"n\">issubset</span><span class=\"p\">(</span><span class=\"nb\">set</span><span class=\"p\">(</span><span class=\"n\">clauses</span><span class=\"p\">)):</span>\n",
       "            <span class=\"k\">return</span> <span class=\"bp\">False</span>\n",
       "        <span class=\"k\">for</span> <span class=\"n\">c</span> <span class=\"ow\">in</span> <span class=\"n\">new</span><span class=\"p\">:</span>\n",
       "            <span class=\"k\">if</span> <span class=\"n\">c</span> <span class=\"ow\">not</span> <span class=\"ow\">in</span> <span class=\"n\">clauses</span><span class=\"p\">:</span>\n",
       "                <span class=\"n\">clauses</span><span class=\"o\">.</span><span class=\"n\">append</span><span class=\"p\">(</span><span class=\"n\">c</span><span class=\"p\">)</span>\n",
       "</pre></div>\n",
       "</body>\n",
       "</html>\n"
      ],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "psource(pl_resolution)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 38,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "(True, False)"
      ]
     },
     "execution_count": 38,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "pl_resolution(wumpus_kb, ~P11), pl_resolution(wumpus_kb, P11)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 39,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "(False, False)"
      ]
     },
     "execution_count": 39,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "pl_resolution(wumpus_kb, ~P22), pl_resolution(wumpus_kb, P22)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Forward and backward chaining\n",
    "Previously, we said we will look at two algorithms to check if a sentence is entailed by the `KB`, \n",
    "but here's a third one. \n",
    "The difference here is that our goal now is to determine if a knowledge base of definite clauses entails a single proposition symbol *q* - the query.\n",
    "There is a catch however, the knowledge base can only contain **Horn clauses**.\n",
    "<br>\n",
    "#### Horn Clauses\n",
    "Horn clauses can be defined as a *disjunction* of *literals* with **at most** one positive literal. \n",
    "<br>\n",
    "A Horn clause with exactly one positive literal is called a *definite clause*.\n",
    "<br>\n",
    "A Horn clause might look like \n",
    "<br>\n",
    "$\\neg a\\lor\\neg b\\lor\\neg c\\lor\\neg d... \\lor z$\n",
    "<br>\n",
    "This, coincidentally, is also a definite clause.\n",
    "<br>\n",
    "Using De Morgan's laws, the example above can be simplified to \n",
    "<br>\n",
    "$a\\land b\\land c\\land d ... \\implies z$\n",
    "<br>\n",
    "This seems like a logical representation of how humans process known data and facts. \n",
    "Assuming percepts `a`, `b`, `c`, `d` ... to be true simultaneously, we can infer `z` to also be true at that point in time. \n",
    "There are some interesting aspects of Horn clauses that make algorithmic inference or *resolution* easier.\n",
    "- Definite clauses can be written as implications:\n",
    "<br>\n",
    "The most important simplification a definite clause provides is that it can be written as an implication.\n",
    "The premise (or the knowledge that leads to the implication) is a conjunction of positive literals.\n",
    "The conclusion (the implied statement) is also a positive literal.\n",
    "The sentence thus becomes easier to understand.\n",
    "The premise and the conclusion are conventionally called the *body* and the *head* respectively.\n",
    "A single positive literal is called a *fact*.\n",
    "- Forward chaining and backward chaining can be used for inference from Horn clauses:\n",
    "<br>\n",
    "Forward chaining is semantically identical to `AND-OR-Graph-Search` from the chapter on search algorithms.\n",
    "Implementational details will be explained shortly.\n",
    "- Deciding entailment with Horn clauses is linear in size of the knowledge base:\n",
    "<br>\n",
    "Surprisingly, the forward and backward chaining algorithms traverse each element of the knowledge base at most once, greatly simplifying the problem.\n",
    "<br>\n",
    "<br>\n",
    "The function `pl_fc_entails` implements forward chaining to see if a knowledge base `KB` entails a symbol `q`.\n",
    "<br>\n",
    "Before we proceed further, note that `pl_fc_entails` doesn't use an ordinary `KB` instance. \n",
    "The knowledge base here is an instance of the `PropDefiniteKB` class, derived from the `PropKB` class, \n",
    "but modified to store definite clauses.\n",
    "<br>\n",
    "The main point of difference arises in the inclusion of a helper method to `PropDefiniteKB` that returns a list of clauses in KB that have a given symbol `p` in their premise."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 40,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/html": [
       "<!DOCTYPE html PUBLIC \"-//W3C//DTD HTML 4.01//EN\"\n",
       "   \"http://www.w3.org/TR/html4/strict.dtd\">\n",
       "\n",
       "<html>\n",
       "<head>\n",
       "  <title></title>\n",
       "  <meta http-equiv=\"content-type\" content=\"text/html; charset=None\">\n",
       "  <style type=\"text/css\">\n",
       "td.linenos { background-color: #f0f0f0; padding-right: 10px; }\n",
       "span.lineno { background-color: #f0f0f0; padding: 0 5px 0 5px; }\n",
       "pre { line-height: 125%; }\n",
       "body .hll { background-color: #ffffcc }\n",
       "body  { background: #f8f8f8; }\n",
       "body .c { color: #408080; font-style: italic } /* Comment */\n",
       "body .err { border: 1px solid #FF0000 } /* Error */\n",
       "body .k { color: #008000; font-weight: bold } /* Keyword */\n",
       "body .o { color: #666666 } /* Operator */\n",
       "body .ch { color: #408080; font-style: italic } /* Comment.Hashbang */\n",
       "body .cm { color: #408080; font-style: italic } /* Comment.Multiline */\n",
       "body .cp { color: #BC7A00 } /* Comment.Preproc */\n",
       "body .cpf { color: #408080; font-style: italic } /* Comment.PreprocFile */\n",
       "body .c1 { color: #408080; font-style: italic } /* Comment.Single */\n",
       "body .cs { color: #408080; font-style: italic } /* Comment.Special */\n",
       "body .gd { color: #A00000 } /* Generic.Deleted */\n",
       "body .ge { font-style: italic } /* Generic.Emph */\n",
       "body .gr { color: #FF0000 } /* Generic.Error */\n",
       "body .gh { color: #000080; font-weight: bold } /* Generic.Heading */\n",
       "body .gi { color: #00A000 } /* Generic.Inserted */\n",
       "body .go { color: #888888 } /* Generic.Output */\n",
       "body .gp { color: #000080; font-weight: bold } /* Generic.Prompt */\n",
       "body .gs { font-weight: bold } /* Generic.Strong */\n",
       "body .gu { color: #800080; font-weight: bold } /* Generic.Subheading */\n",
       "body .gt { color: #0044DD } /* Generic.Traceback */\n",
       "body .kc { color: #008000; font-weight: bold } /* Keyword.Constant */\n",
       "body .kd { color: #008000; font-weight: bold } /* Keyword.Declaration */\n",
       "body .kn { color: #008000; font-weight: bold } /* Keyword.Namespace */\n",
       "body .kp { color: #008000 } /* Keyword.Pseudo */\n",
       "body .kr { color: #008000; font-weight: bold } /* Keyword.Reserved */\n",
       "body .kt { color: #B00040 } /* Keyword.Type */\n",
       "body .m { color: #666666 } /* Literal.Number */\n",
       "body .s { color: #BA2121 } /* Literal.String */\n",
       "body .na { color: #7D9029 } /* Name.Attribute */\n",
       "body .nb { color: #008000 } /* Name.Builtin */\n",
       "body .nc { color: #0000FF; font-weight: bold } /* Name.Class */\n",
       "body .no { color: #880000 } /* Name.Constant */\n",
       "body .nd { color: #AA22FF } /* Name.Decorator */\n",
       "body .ni { color: #999999; font-weight: bold } /* Name.Entity */\n",
       "body .ne { color: #D2413A; font-weight: bold } /* Name.Exception */\n",
       "body .nf { color: #0000FF } /* Name.Function */\n",
       "body .nl { color: #A0A000 } /* Name.Label */\n",
       "body .nn { color: #0000FF; font-weight: bold } /* Name.Namespace */\n",
       "body .nt { color: #008000; font-weight: bold } /* Name.Tag */\n",
       "body .nv { color: #19177C } /* Name.Variable */\n",
       "body .ow { color: #AA22FF; font-weight: bold } /* Operator.Word */\n",
       "body .w { color: #bbbbbb } /* Text.Whitespace */\n",
       "body .mb { color: #666666 } /* Literal.Number.Bin */\n",
       "body .mf { color: #666666 } /* Literal.Number.Float */\n",
       "body .mh { color: #666666 } /* Literal.Number.Hex */\n",
       "body .mi { color: #666666 } /* Literal.Number.Integer */\n",
       "body .mo { color: #666666 } /* Literal.Number.Oct */\n",
       "body .sa { color: #BA2121 } /* Literal.String.Affix */\n",
       "body .sb { color: #BA2121 } /* Literal.String.Backtick */\n",
       "body .sc { color: #BA2121 } /* Literal.String.Char */\n",
       "body .dl { color: #BA2121 } /* Literal.String.Delimiter */\n",
       "body .sd { color: #BA2121; font-style: italic } /* Literal.String.Doc */\n",
       "body .s2 { color: #BA2121 } /* Literal.String.Double */\n",
       "body .se { color: #BB6622; font-weight: bold } /* Literal.String.Escape */\n",
       "body .sh { color: #BA2121 } /* Literal.String.Heredoc */\n",
       "body .si { color: #BB6688; font-weight: bold } /* Literal.String.Interpol */\n",
       "body .sx { color: #008000 } /* Literal.String.Other */\n",
       "body .sr { color: #BB6688 } /* Literal.String.Regex */\n",
       "body .s1 { color: #BA2121 } /* Literal.String.Single */\n",
       "body .ss { color: #19177C } /* Literal.String.Symbol */\n",
       "body .bp { color: #008000 } /* Name.Builtin.Pseudo */\n",
       "body .fm { color: #0000FF } /* Name.Function.Magic */\n",
       "body .vc { color: #19177C } /* Name.Variable.Class */\n",
       "body .vg { color: #19177C } /* Name.Variable.Global */\n",
       "body .vi { color: #19177C } /* Name.Variable.Instance */\n",
       "body .vm { color: #19177C } /* Name.Variable.Magic */\n",
       "body .il { color: #666666 } /* Literal.Number.Integer.Long */\n",
       "\n",
       "  </style>\n",
       "</head>\n",
       "<body>\n",
       "<h2></h2>\n",
       "\n",
       "<div class=\"highlight\"><pre><span></span>    <span class=\"k\">def</span> <span class=\"nf\">clauses_with_premise</span><span class=\"p\">(</span><span class=\"bp\">self</span><span class=\"p\">,</span> <span class=\"n\">p</span><span class=\"p\">):</span>\n",
       "        <span class=\"sd\">&quot;&quot;&quot;Return a list of the clauses in KB that have p in their premise.</span>\n",
       "<span class=\"sd\">        This could be cached away for O(1) speed, but we&#39;ll recompute it.&quot;&quot;&quot;</span>\n",
       "        <span class=\"k\">return</span> <span class=\"p\">[</span><span class=\"n\">c</span> <span class=\"k\">for</span> <span class=\"n\">c</span> <span class=\"ow\">in</span> <span class=\"bp\">self</span><span class=\"o\">.</span><span class=\"n\">clauses</span>\n",
       "                <span class=\"k\">if</span> <span class=\"n\">c</span><span class=\"o\">.</span><span class=\"n\">op</span> <span class=\"o\">==</span> <span class=\"s1\">&#39;==&gt;&#39;</span> <span class=\"ow\">and</span> <span class=\"n\">p</span> <span class=\"ow\">in</span> <span class=\"n\">conjuncts</span><span class=\"p\">(</span><span class=\"n\">c</span><span class=\"o\">.</span><span class=\"n\">args</span><span class=\"p\">[</span><span class=\"mi\">0</span><span class=\"p\">])]</span>\n",
       "</pre></div>\n",
       "</body>\n",
       "</html>\n"
      ],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "psource(PropDefiniteKB.clauses_with_premise)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Let's now have a look at the `pl_fc_entails` algorithm."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 41,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/html": [
       "<!DOCTYPE html PUBLIC \"-//W3C//DTD HTML 4.01//EN\"\n",
       "   \"http://www.w3.org/TR/html4/strict.dtd\">\n",
       "\n",
       "<html>\n",
       "<head>\n",
       "  <title></title>\n",
       "  <meta http-equiv=\"content-type\" content=\"text/html; charset=None\">\n",
       "  <style type=\"text/css\">\n",
       "td.linenos { background-color: #f0f0f0; padding-right: 10px; }\n",
       "span.lineno { background-color: #f0f0f0; padding: 0 5px 0 5px; }\n",
       "pre { line-height: 125%; }\n",
       "body .hll { background-color: #ffffcc }\n",
       "body  { background: #f8f8f8; }\n",
       "body .c { color: #408080; font-style: italic } /* Comment */\n",
       "body .err { border: 1px solid #FF0000 } /* Error */\n",
       "body .k { color: #008000; font-weight: bold } /* Keyword */\n",
       "body .o { color: #666666 } /* Operator */\n",
       "body .ch { color: #408080; font-style: italic } /* Comment.Hashbang */\n",
       "body .cm { color: #408080; font-style: italic } /* Comment.Multiline */\n",
       "body .cp { color: #BC7A00 } /* Comment.Preproc */\n",
       "body .cpf { color: #408080; font-style: italic } /* Comment.PreprocFile */\n",
       "body .c1 { color: #408080; font-style: italic } /* Comment.Single */\n",
       "body .cs { color: #408080; font-style: italic } /* Comment.Special */\n",
       "body .gd { color: #A00000 } /* Generic.Deleted */\n",
       "body .ge { font-style: italic } /* Generic.Emph */\n",
       "body .gr { color: #FF0000 } /* Generic.Error */\n",
       "body .gh { color: #000080; font-weight: bold } /* Generic.Heading */\n",
       "body .gi { color: #00A000 } /* Generic.Inserted */\n",
       "body .go { color: #888888 } /* Generic.Output */\n",
       "body .gp { color: #000080; font-weight: bold } /* Generic.Prompt */\n",
       "body .gs { font-weight: bold } /* Generic.Strong */\n",
       "body .gu { color: #800080; font-weight: bold } /* Generic.Subheading */\n",
       "body .gt { color: #0044DD } /* Generic.Traceback */\n",
       "body .kc { color: #008000; font-weight: bold } /* Keyword.Constant */\n",
       "body .kd { color: #008000; font-weight: bold } /* Keyword.Declaration */\n",
       "body .kn { color: #008000; font-weight: bold } /* Keyword.Namespace */\n",
       "body .kp { color: #008000 } /* Keyword.Pseudo */\n",
       "body .kr { color: #008000; font-weight: bold } /* Keyword.Reserved */\n",
       "body .kt { color: #B00040 } /* Keyword.Type */\n",
       "body .m { color: #666666 } /* Literal.Number */\n",
       "body .s { color: #BA2121 } /* Literal.String */\n",
       "body .na { color: #7D9029 } /* Name.Attribute */\n",
       "body .nb { color: #008000 } /* Name.Builtin */\n",
       "body .nc { color: #0000FF; font-weight: bold } /* Name.Class */\n",
       "body .no { color: #880000 } /* Name.Constant */\n",
       "body .nd { color: #AA22FF } /* Name.Decorator */\n",
       "body .ni { color: #999999; font-weight: bold } /* Name.Entity */\n",
       "body .ne { color: #D2413A; font-weight: bold } /* Name.Exception */\n",
       "body .nf { color: #0000FF } /* Name.Function */\n",
       "body .nl { color: #A0A000 } /* Name.Label */\n",
       "body .nn { color: #0000FF; font-weight: bold } /* Name.Namespace */\n",
       "body .nt { color: #008000; font-weight: bold } /* Name.Tag */\n",
       "body .nv { color: #19177C } /* Name.Variable */\n",
       "body .ow { color: #AA22FF; font-weight: bold } /* Operator.Word */\n",
       "body .w { color: #bbbbbb } /* Text.Whitespace */\n",
       "body .mb { color: #666666 } /* Literal.Number.Bin */\n",
       "body .mf { color: #666666 } /* Literal.Number.Float */\n",
       "body .mh { color: #666666 } /* Literal.Number.Hex */\n",
       "body .mi { color: #666666 } /* Literal.Number.Integer */\n",
       "body .mo { color: #666666 } /* Literal.Number.Oct */\n",
       "body .sa { color: #BA2121 } /* Literal.String.Affix */\n",
       "body .sb { color: #BA2121 } /* Literal.String.Backtick */\n",
       "body .sc { color: #BA2121 } /* Literal.String.Char */\n",
       "body .dl { color: #BA2121 } /* Literal.String.Delimiter */\n",
       "body .sd { color: #BA2121; font-style: italic } /* Literal.String.Doc */\n",
       "body .s2 { color: #BA2121 } /* Literal.String.Double */\n",
       "body .se { color: #BB6622; font-weight: bold } /* Literal.String.Escape */\n",
       "body .sh { color: #BA2121 } /* Literal.String.Heredoc */\n",
       "body .si { color: #BB6688; font-weight: bold } /* Literal.String.Interpol */\n",
       "body .sx { color: #008000 } /* Literal.String.Other */\n",
       "body .sr { color: #BB6688 } /* Literal.String.Regex */\n",
       "body .s1 { color: #BA2121 } /* Literal.String.Single */\n",
       "body .ss { color: #19177C } /* Literal.String.Symbol */\n",
       "body .bp { color: #008000 } /* Name.Builtin.Pseudo */\n",
       "body .fm { color: #0000FF } /* Name.Function.Magic */\n",
       "body .vc { color: #19177C } /* Name.Variable.Class */\n",
       "body .vg { color: #19177C } /* Name.Variable.Global */\n",
       "body .vi { color: #19177C } /* Name.Variable.Instance */\n",
       "body .vm { color: #19177C } /* Name.Variable.Magic */\n",
       "body .il { color: #666666 } /* Literal.Number.Integer.Long */\n",
       "\n",
       "  </style>\n",
       "</head>\n",
       "<body>\n",
       "<h2></h2>\n",
       "\n",
       "<div class=\"highlight\"><pre><span></span><span class=\"k\">def</span> <span class=\"nf\">pl_fc_entails</span><span class=\"p\">(</span><span class=\"n\">KB</span><span class=\"p\">,</span> <span class=\"n\">q</span><span class=\"p\">):</span>\n",
       "    <span class=\"sd\">&quot;&quot;&quot;Use forward chaining to see if a PropDefiniteKB entails symbol q.</span>\n",
       "<span class=\"sd\">    [Figure 7.15]</span>\n",
       "<span class=\"sd\">    &gt;&gt;&gt; pl_fc_entails(horn_clauses_KB, expr(&#39;Q&#39;))</span>\n",
       "<span class=\"sd\">    True</span>\n",
       "<span class=\"sd\">    &quot;&quot;&quot;</span>\n",
       "    <span class=\"n\">count</span> <span class=\"o\">=</span> <span class=\"p\">{</span><span class=\"n\">c</span><span class=\"p\">:</span> <span class=\"nb\">len</span><span class=\"p\">(</span><span class=\"n\">conjuncts</span><span class=\"p\">(</span><span class=\"n\">c</span><span class=\"o\">.</span><span class=\"n\">args</span><span class=\"p\">[</span><span class=\"mi\">0</span><span class=\"p\">]))</span>\n",
       "             <span class=\"k\">for</span> <span class=\"n\">c</span> <span class=\"ow\">in</span> <span class=\"n\">KB</span><span class=\"o\">.</span><span class=\"n\">clauses</span>\n",
       "             <span class=\"k\">if</span> <span class=\"n\">c</span><span class=\"o\">.</span><span class=\"n\">op</span> <span class=\"o\">==</span> <span class=\"s1\">&#39;==&gt;&#39;</span><span class=\"p\">}</span>\n",
       "    <span class=\"n\">inferred</span> <span class=\"o\">=</span> <span class=\"n\">defaultdict</span><span class=\"p\">(</span><span class=\"nb\">bool</span><span class=\"p\">)</span>\n",
       "    <span class=\"n\">agenda</span> <span class=\"o\">=</span> <span class=\"p\">[</span><span class=\"n\">s</span> <span class=\"k\">for</span> <span class=\"n\">s</span> <span class=\"ow\">in</span> <span class=\"n\">KB</span><span class=\"o\">.</span><span class=\"n\">clauses</span> <span class=\"k\">if</span> <span class=\"n\">is_prop_symbol</span><span class=\"p\">(</span><span class=\"n\">s</span><span class=\"o\">.</span><span class=\"n\">op</span><span class=\"p\">)]</span>\n",
       "    <span class=\"k\">while</span> <span class=\"n\">agenda</span><span class=\"p\">:</span>\n",
       "        <span class=\"n\">p</span> <span class=\"o\">=</span> <span class=\"n\">agenda</span><span class=\"o\">.</span><span class=\"n\">pop</span><span class=\"p\">()</span>\n",
       "        <span class=\"k\">if</span> <span class=\"n\">p</span> <span class=\"o\">==</span> <span class=\"n\">q</span><span class=\"p\">:</span>\n",
       "            <span class=\"k\">return</span> <span class=\"bp\">True</span>\n",
       "        <span class=\"k\">if</span> <span class=\"ow\">not</span> <span class=\"n\">inferred</span><span class=\"p\">[</span><span class=\"n\">p</span><span class=\"p\">]:</span>\n",
       "            <span class=\"n\">inferred</span><span class=\"p\">[</span><span class=\"n\">p</span><span class=\"p\">]</span> <span class=\"o\">=</span> <span class=\"bp\">True</span>\n",
       "            <span class=\"k\">for</span> <span class=\"n\">c</span> <span class=\"ow\">in</span> <span class=\"n\">KB</span><span class=\"o\">.</span><span class=\"n\">clauses_with_premise</span><span class=\"p\">(</span><span class=\"n\">p</span><span class=\"p\">):</span>\n",
       "                <span class=\"n\">count</span><span class=\"p\">[</span><span class=\"n\">c</span><span class=\"p\">]</span> <span class=\"o\">-=</span> <span class=\"mi\">1</span>\n",
       "                <span class=\"k\">if</span> <span class=\"n\">count</span><span class=\"p\">[</span><span class=\"n\">c</span><span class=\"p\">]</span> <span class=\"o\">==</span> <span class=\"mi\">0</span><span class=\"p\">:</span>\n",
       "                    <span class=\"n\">agenda</span><span class=\"o\">.</span><span class=\"n\">append</span><span class=\"p\">(</span><span class=\"n\">c</span><span class=\"o\">.</span><span class=\"n\">args</span><span class=\"p\">[</span><span class=\"mi\">1</span><span class=\"p\">])</span>\n",
       "    <span class=\"k\">return</span> <span class=\"bp\">False</span>\n",
       "</pre></div>\n",
       "</body>\n",
       "</html>\n"
      ],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "psource(pl_fc_entails)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "The function accepts a knowledge base `KB` (an instance of `PropDefiniteKB`) and a query `q` as inputs.\n",
    "<br>\n",
    "<br>\n",
    "`count` initially stores the number of symbols in the premise of each sentence in the knowledge base.\n",
    "<br>\n",
    "The `conjuncts` helper function separates a given sentence at conjunctions.\n",
    "<br>\n",
    "`inferred` is initialized as a *boolean* defaultdict. \n",
    "This will be used later to check if we have inferred all premises of each clause of the agenda.\n",
    "<br>\n",
    "`agenda` initially stores a list of clauses that the knowledge base knows to be true.\n",
    "The `is_prop_symbol` helper function checks if the given symbol is a valid propositional logic symbol.\n",
    "<br>\n",
    "<br>\n",
    "We now iterate through `agenda`, popping a symbol `p` on each iteration.\n",
    "If the query `q` is the same as `p`, we know that entailment holds.\n",
    "<br>\n",
    "The agenda is processed, reducing `count` by one for each implication with a premise `p`.\n",
    "A conclusion is added to the agenda when `count` reaches zero. This means we know all the premises of that particular implication to be true.\n",
    "<br>\n",
    "`clauses_with_premise` is a helpful method of the `PropKB` class.\n",
    "It returns a list of clauses in the knowledge base that have `p` in their premise.\n",
    "<br>\n",
    "<br>\n",
    "Now that we have an idea of how this function works, let's see a few examples of its usage, but we first need to define our knowledge base. We assume we know the following clauses to be true."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 42,
   "metadata": {},
   "outputs": [],
   "source": [
    "clauses = ['(B & F)==>E', \n",
    "           '(A & E & F)==>G', \n",
    "           '(B & C)==>F', \n",
    "           '(A & B)==>D', \n",
    "           '(E & F)==>H', \n",
    "           '(H & I)==>J',\n",
    "           'A', \n",
    "           'B', \n",
    "           'C']"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "We will now `tell` this information to our knowledge base."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 43,
   "metadata": {},
   "outputs": [],
   "source": [
    "definite_clauses_KB = PropDefiniteKB()\n",
    "for clause in clauses:\n",
    "    definite_clauses_KB.tell(expr(clause))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "We can now check if our knowledge base entails the following queries."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 44,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "execution_count": 44,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "pl_fc_entails(definite_clauses_KB, expr('G'))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 45,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "execution_count": 45,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "pl_fc_entails(definite_clauses_KB, expr('H'))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 46,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "False"
      ]
     },
     "execution_count": 46,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "pl_fc_entails(definite_clauses_KB, expr('I'))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 47,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "False"
      ]
     },
     "execution_count": 47,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "pl_fc_entails(definite_clauses_KB, expr('J'))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Effective Propositional Model Checking\n",
    "\n",
    "The previous segments elucidate the algorithmic procedure for model checking. \n",
    "In this segment, we look at ways of making them computationally efficient.\n",
    "<br>\n",
    "The problem we are trying to solve is conventionally called the _propositional satisfiability problem_, abbreviated as the _SAT_ problem.\n",
    "In layman terms, if there exists a model that satisfies a given Boolean formula, the formula is called satisfiable.\n",
    "<br>\n",
    "The SAT problem was the first problem to be proven _NP-complete_.\n",
    "The main characteristics of an NP-complete problem are:\n",
    "- Given a solution to such a problem, it is easy to verify if the solution solves the problem.\n",
    "- The time required to actually solve the problem using any known algorithm increases exponentially with respect to the size of the problem.\n",
    "<br>\n",
    "<br>\n",
    "Due to these properties, heuristic and approximational methods are often applied to find solutions to these problems.\n",
    "<br>\n",
    "It is extremely important to be able to solve large scale SAT problems efficiently because \n",
    "many combinatorial problems in computer science can be conveniently reduced to checking the satisfiability of a propositional sentence under some constraints.\n",
    "<br>\n",
    "We will introduce two new algorithms that perform propositional model checking in a computationally effective way.\n",
    "<br>\n"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### 1. DPLL (Davis-Putnam-Logeman-Loveland) algorithm\n",
    "This algorithm is very similar to Backtracking-Search.\n",
    "It recursively enumerates possible models in a depth-first fashion with the following improvements over algorithms like `tt_entails`:\n",
    "1. Early termination:\n",
    "<br>\n",
    "In certain cases, the algorithm can detect the truth value of a statement using just a partially completed model.\n",
    "For example, $(P\\lor Q)\\land(P\\lor R)$ is true if P is true, regardless of other variables.\n",
    "This reduces the search space significantly.\n",
    "2. Pure symbol heuristic:\n",
    "<br>\n",
    "A symbol that has the same sign (positive or negative) in all clauses is called a _pure symbol_.\n",
    "It isn't difficult to see that any satisfiable model will have the pure symbols assigned such that its parent clause becomes _true_.\n",
    "For example, $(P\\lor\\neg Q)\\land(\\neg Q\\lor\\neg R)\\land(R\\lor P)$ has P and Q as pure symbols\n",
    "and for the sentence to be true, P _has_ to be true and Q _has_ to be false.\n",
    "The pure symbol heuristic thus simplifies the problem a bit.\n",
    "3. Unit clause heuristic:\n",
    "<br>\n",
    "In the context of DPLL, clauses with just one literal and clauses with all but one _false_ literals are called unit clauses.\n",
    "If a clause is a unit clause, it can only be satisfied by assigning the necessary value to make the last literal true.\n",
    "We have no other choice.\n",
    "<br>\n",
    "Assigning one unit clause can create another unit clause.\n",
    "For example, when P is false, $(P\\lor Q)$ becomes a unit clause, causing _true_ to be assigned to Q.\n",
    "A series of forced assignments derived from previous unit clauses is called _unit propagation_.\n",
    "In this way, this heuristic simplifies the problem further.\n",
    "<br>\n",
    "The algorithm often employs other tricks to scale up to large problems.\n",
    "However, these tricks are currently out of the scope of this notebook. Refer to section 7.6 of the book for more details.\n",
    "<br>\n",
    "<br>\n",
    "Let's have a look at the algorithm."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 48,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/html": [
       "<!DOCTYPE html PUBLIC \"-//W3C//DTD HTML 4.01//EN\"\n",
       "   \"http://www.w3.org/TR/html4/strict.dtd\">\n",
       "\n",
       "<html>\n",
       "<head>\n",
       "  <title></title>\n",
       "  <meta http-equiv=\"content-type\" content=\"text/html; charset=None\">\n",
       "  <style type=\"text/css\">\n",
       "td.linenos { background-color: #f0f0f0; padding-right: 10px; }\n",
       "span.lineno { background-color: #f0f0f0; padding: 0 5px 0 5px; }\n",
       "pre { line-height: 125%; }\n",
       "body .hll { background-color: #ffffcc }\n",
       "body  { background: #f8f8f8; }\n",
       "body .c { color: #408080; font-style: italic } /* Comment */\n",
       "body .err { border: 1px solid #FF0000 } /* Error */\n",
       "body .k { color: #008000; font-weight: bold } /* Keyword */\n",
       "body .o { color: #666666 } /* Operator */\n",
       "body .ch { color: #408080; font-style: italic } /* Comment.Hashbang */\n",
       "body .cm { color: #408080; font-style: italic } /* Comment.Multiline */\n",
       "body .cp { color: #BC7A00 } /* Comment.Preproc */\n",
       "body .cpf { color: #408080; font-style: italic } /* Comment.PreprocFile */\n",
       "body .c1 { color: #408080; font-style: italic } /* Comment.Single */\n",
       "body .cs { color: #408080; font-style: italic } /* Comment.Special */\n",
       "body .gd { color: #A00000 } /* Generic.Deleted */\n",
       "body .ge { font-style: italic } /* Generic.Emph */\n",
       "body .gr { color: #FF0000 } /* Generic.Error */\n",
       "body .gh { color: #000080; font-weight: bold } /* Generic.Heading */\n",
       "body .gi { color: #00A000 } /* Generic.Inserted */\n",
       "body .go { color: #888888 } /* Generic.Output */\n",
       "body .gp { color: #000080; font-weight: bold } /* Generic.Prompt */\n",
       "body .gs { font-weight: bold } /* Generic.Strong */\n",
       "body .gu { color: #800080; font-weight: bold } /* Generic.Subheading */\n",
       "body .gt { color: #0044DD } /* Generic.Traceback */\n",
       "body .kc { color: #008000; font-weight: bold } /* Keyword.Constant */\n",
       "body .kd { color: #008000; font-weight: bold } /* Keyword.Declaration */\n",
       "body .kn { color: #008000; font-weight: bold } /* Keyword.Namespace */\n",
       "body .kp { color: #008000 } /* Keyword.Pseudo */\n",
       "body .kr { color: #008000; font-weight: bold } /* Keyword.Reserved */\n",
       "body .kt { color: #B00040 } /* Keyword.Type */\n",
       "body .m { color: #666666 } /* Literal.Number */\n",
       "body .s { color: #BA2121 } /* Literal.String */\n",
       "body .na { color: #7D9029 } /* Name.Attribute */\n",
       "body .nb { color: #008000 } /* Name.Builtin */\n",
       "body .nc { color: #0000FF; font-weight: bold } /* Name.Class */\n",
       "body .no { color: #880000 } /* Name.Constant */\n",
       "body .nd { color: #AA22FF } /* Name.Decorator */\n",
       "body .ni { color: #999999; font-weight: bold } /* Name.Entity */\n",
       "body .ne { color: #D2413A; font-weight: bold } /* Name.Exception */\n",
       "body .nf { color: #0000FF } /* Name.Function */\n",
       "body .nl { color: #A0A000 } /* Name.Label */\n",
       "body .nn { color: #0000FF; font-weight: bold } /* Name.Namespace */\n",
       "body .nt { color: #008000; font-weight: bold } /* Name.Tag */\n",
       "body .nv { color: #19177C } /* Name.Variable */\n",
       "body .ow { color: #AA22FF; font-weight: bold } /* Operator.Word */\n",
       "body .w { color: #bbbbbb } /* Text.Whitespace */\n",
       "body .mb { color: #666666 } /* Literal.Number.Bin */\n",
       "body .mf { color: #666666 } /* Literal.Number.Float */\n",
       "body .mh { color: #666666 } /* Literal.Number.Hex */\n",
       "body .mi { color: #666666 } /* Literal.Number.Integer */\n",
       "body .mo { color: #666666 } /* Literal.Number.Oct */\n",
       "body .sa { color: #BA2121 } /* Literal.String.Affix */\n",
       "body .sb { color: #BA2121 } /* Literal.String.Backtick */\n",
       "body .sc { color: #BA2121 } /* Literal.String.Char */\n",
       "body .dl { color: #BA2121 } /* Literal.String.Delimiter */\n",
       "body .sd { color: #BA2121; font-style: italic } /* Literal.String.Doc */\n",
       "body .s2 { color: #BA2121 } /* Literal.String.Double */\n",
       "body .se { color: #BB6622; font-weight: bold } /* Literal.String.Escape */\n",
       "body .sh { color: #BA2121 } /* Literal.String.Heredoc */\n",
       "body .si { color: #BB6688; font-weight: bold } /* Literal.String.Interpol */\n",
       "body .sx { color: #008000 } /* Literal.String.Other */\n",
       "body .sr { color: #BB6688 } /* Literal.String.Regex */\n",
       "body .s1 { color: #BA2121 } /* Literal.String.Single */\n",
       "body .ss { color: #19177C } /* Literal.String.Symbol */\n",
       "body .bp { color: #008000 } /* Name.Builtin.Pseudo */\n",
       "body .fm { color: #0000FF } /* Name.Function.Magic */\n",
       "body .vc { color: #19177C } /* Name.Variable.Class */\n",
       "body .vg { color: #19177C } /* Name.Variable.Global */\n",
       "body .vi { color: #19177C } /* Name.Variable.Instance */\n",
       "body .vm { color: #19177C } /* Name.Variable.Magic */\n",
       "body .il { color: #666666 } /* Literal.Number.Integer.Long */\n",
       "\n",
       "  </style>\n",
       "</head>\n",
       "<body>\n",
       "<h2></h2>\n",
       "\n",
       "<div class=\"highlight\"><pre><span></span><span class=\"k\">def</span> <span class=\"nf\">dpll</span><span class=\"p\">(</span><span class=\"n\">clauses</span><span class=\"p\">,</span> <span class=\"n\">symbols</span><span class=\"p\">,</span> <span class=\"n\">model</span><span class=\"p\">):</span>\n",
       "    <span class=\"sd\">&quot;&quot;&quot;See if the clauses are true in a partial model.&quot;&quot;&quot;</span>\n",
       "    <span class=\"n\">unknown_clauses</span> <span class=\"o\">=</span> <span class=\"p\">[]</span>  <span class=\"c1\"># clauses with an unknown truth value</span>\n",
       "    <span class=\"k\">for</span> <span class=\"n\">c</span> <span class=\"ow\">in</span> <span class=\"n\">clauses</span><span class=\"p\">:</span>\n",
       "        <span class=\"n\">val</span> <span class=\"o\">=</span> <span class=\"n\">pl_true</span><span class=\"p\">(</span><span class=\"n\">c</span><span class=\"p\">,</span> <span class=\"n\">model</span><span class=\"p\">)</span>\n",
       "        <span class=\"k\">if</span> <span class=\"n\">val</span> <span class=\"ow\">is</span> <span class=\"bp\">False</span><span class=\"p\">:</span>\n",
       "            <span class=\"k\">return</span> <span class=\"bp\">False</span>\n",
       "        <span class=\"k\">if</span> <span class=\"n\">val</span> <span class=\"ow\">is</span> <span class=\"ow\">not</span> <span class=\"bp\">True</span><span class=\"p\">:</span>\n",
       "            <span class=\"n\">unknown_clauses</span><span class=\"o\">.</span><span class=\"n\">append</span><span class=\"p\">(</span><span class=\"n\">c</span><span class=\"p\">)</span>\n",
       "    <span class=\"k\">if</span> <span class=\"ow\">not</span> <span class=\"n\">unknown_clauses</span><span class=\"p\">:</span>\n",
       "        <span class=\"k\">return</span> <span class=\"n\">model</span>\n",
       "    <span class=\"n\">P</span><span class=\"p\">,</span> <span class=\"n\">value</span> <span class=\"o\">=</span> <span class=\"n\">find_pure_symbol</span><span class=\"p\">(</span><span class=\"n\">symbols</span><span class=\"p\">,</span> <span class=\"n\">unknown_clauses</span><span class=\"p\">)</span>\n",
       "    <span class=\"k\">if</span> <span class=\"n\">P</span><span class=\"p\">:</span>\n",
       "        <span class=\"k\">return</span> <span class=\"n\">dpll</span><span class=\"p\">(</span><span class=\"n\">clauses</span><span class=\"p\">,</span> <span class=\"n\">removeall</span><span class=\"p\">(</span><span class=\"n\">P</span><span class=\"p\">,</span> <span class=\"n\">symbols</span><span class=\"p\">),</span> <span class=\"n\">extend</span><span class=\"p\">(</span><span class=\"n\">model</span><span class=\"p\">,</span> <span class=\"n\">P</span><span class=\"p\">,</span> <span class=\"n\">value</span><span class=\"p\">))</span>\n",
       "    <span class=\"n\">P</span><span class=\"p\">,</span> <span class=\"n\">value</span> <span class=\"o\">=</span> <span class=\"n\">find_unit_clause</span><span class=\"p\">(</span><span class=\"n\">clauses</span><span class=\"p\">,</span> <span class=\"n\">model</span><span class=\"p\">)</span>\n",
       "    <span class=\"k\">if</span> <span class=\"n\">P</span><span class=\"p\">:</span>\n",
       "        <span class=\"k\">return</span> <span class=\"n\">dpll</span><span class=\"p\">(</span><span class=\"n\">clauses</span><span class=\"p\">,</span> <span class=\"n\">removeall</span><span class=\"p\">(</span><span class=\"n\">P</span><span class=\"p\">,</span> <span class=\"n\">symbols</span><span class=\"p\">),</span> <span class=\"n\">extend</span><span class=\"p\">(</span><span class=\"n\">model</span><span class=\"p\">,</span> <span class=\"n\">P</span><span class=\"p\">,</span> <span class=\"n\">value</span><span class=\"p\">))</span>\n",
       "    <span class=\"k\">if</span> <span class=\"ow\">not</span> <span class=\"n\">symbols</span><span class=\"p\">:</span>\n",
       "        <span class=\"k\">raise</span> <span class=\"ne\">TypeError</span><span class=\"p\">(</span><span class=\"s2\">&quot;Argument should be of the type Expr.&quot;</span><span class=\"p\">)</span>\n",
       "    <span class=\"n\">P</span><span class=\"p\">,</span> <span class=\"n\">symbols</span> <span class=\"o\">=</span> <span class=\"n\">symbols</span><span class=\"p\">[</span><span class=\"mi\">0</span><span class=\"p\">],</span> <span class=\"n\">symbols</span><span class=\"p\">[</span><span class=\"mi\">1</span><span class=\"p\">:]</span>\n",
       "    <span class=\"k\">return</span> <span class=\"p\">(</span><span class=\"n\">dpll</span><span class=\"p\">(</span><span class=\"n\">clauses</span><span class=\"p\">,</span> <span class=\"n\">symbols</span><span class=\"p\">,</span> <span class=\"n\">extend</span><span class=\"p\">(</span><span class=\"n\">model</span><span class=\"p\">,</span> <span class=\"n\">P</span><span class=\"p\">,</span> <span class=\"bp\">True</span><span class=\"p\">))</span> <span class=\"ow\">or</span>\n",
       "            <span class=\"n\">dpll</span><span class=\"p\">(</span><span class=\"n\">clauses</span><span class=\"p\">,</span> <span class=\"n\">symbols</span><span class=\"p\">,</span> <span class=\"n\">extend</span><span class=\"p\">(</span><span class=\"n\">model</span><span class=\"p\">,</span> <span class=\"n\">P</span><span class=\"p\">,</span> <span class=\"bp\">False</span><span class=\"p\">)))</span>\n",
       "</pre></div>\n",
       "</body>\n",
       "</html>\n"
      ],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "psource(dpll)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "The algorithm uses the ideas described above to check satisfiability of a sentence in propositional logic.\n",
    "It recursively calls itself, simplifying the problem at each step. It also uses helper functions `find_pure_symbol` and `find_unit_clause` to carry out steps 2 and 3 above.\n",
    "<br>\n",
    "The `dpll_satisfiable` helper function converts the input clauses to _conjunctive normal form_ and calls the `dpll` function with the correct parameters."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 49,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/html": [
       "<!DOCTYPE html PUBLIC \"-//W3C//DTD HTML 4.01//EN\"\n",
       "   \"http://www.w3.org/TR/html4/strict.dtd\">\n",
       "\n",
       "<html>\n",
       "<head>\n",
       "  <title></title>\n",
       "  <meta http-equiv=\"content-type\" content=\"text/html; charset=None\">\n",
       "  <style type=\"text/css\">\n",
       "td.linenos { background-color: #f0f0f0; padding-right: 10px; }\n",
       "span.lineno { background-color: #f0f0f0; padding: 0 5px 0 5px; }\n",
       "pre { line-height: 125%; }\n",
       "body .hll { background-color: #ffffcc }\n",
       "body  { background: #f8f8f8; }\n",
       "body .c { color: #408080; font-style: italic } /* Comment */\n",
       "body .err { border: 1px solid #FF0000 } /* Error */\n",
       "body .k { color: #008000; font-weight: bold } /* Keyword */\n",
       "body .o { color: #666666 } /* Operator */\n",
       "body .ch { color: #408080; font-style: italic } /* Comment.Hashbang */\n",
       "body .cm { color: #408080; font-style: italic } /* Comment.Multiline */\n",
       "body .cp { color: #BC7A00 } /* Comment.Preproc */\n",
       "body .cpf { color: #408080; font-style: italic } /* Comment.PreprocFile */\n",
       "body .c1 { color: #408080; font-style: italic } /* Comment.Single */\n",
       "body .cs { color: #408080; font-style: italic } /* Comment.Special */\n",
       "body .gd { color: #A00000 } /* Generic.Deleted */\n",
       "body .ge { font-style: italic } /* Generic.Emph */\n",
       "body .gr { color: #FF0000 } /* Generic.Error */\n",
       "body .gh { color: #000080; font-weight: bold } /* Generic.Heading */\n",
       "body .gi { color: #00A000 } /* Generic.Inserted */\n",
       "body .go { color: #888888 } /* Generic.Output */\n",
       "body .gp { color: #000080; font-weight: bold } /* Generic.Prompt */\n",
       "body .gs { font-weight: bold } /* Generic.Strong */\n",
       "body .gu { color: #800080; font-weight: bold } /* Generic.Subheading */\n",
       "body .gt { color: #0044DD } /* Generic.Traceback */\n",
       "body .kc { color: #008000; font-weight: bold } /* Keyword.Constant */\n",
       "body .kd { color: #008000; font-weight: bold } /* Keyword.Declaration */\n",
       "body .kn { color: #008000; font-weight: bold } /* Keyword.Namespace */\n",
       "body .kp { color: #008000 } /* Keyword.Pseudo */\n",
       "body .kr { color: #008000; font-weight: bold } /* Keyword.Reserved */\n",
       "body .kt { color: #B00040 } /* Keyword.Type */\n",
       "body .m { color: #666666 } /* Literal.Number */\n",
       "body .s { color: #BA2121 } /* Literal.String */\n",
       "body .na { color: #7D9029 } /* Name.Attribute */\n",
       "body .nb { color: #008000 } /* Name.Builtin */\n",
       "body .nc { color: #0000FF; font-weight: bold } /* Name.Class */\n",
       "body .no { color: #880000 } /* Name.Constant */\n",
       "body .nd { color: #AA22FF } /* Name.Decorator */\n",
       "body .ni { color: #999999; font-weight: bold } /* Name.Entity */\n",
       "body .ne { color: #D2413A; font-weight: bold } /* Name.Exception */\n",
       "body .nf { color: #0000FF } /* Name.Function */\n",
       "body .nl { color: #A0A000 } /* Name.Label */\n",
       "body .nn { color: #0000FF; font-weight: bold } /* Name.Namespace */\n",
       "body .nt { color: #008000; font-weight: bold } /* Name.Tag */\n",
       "body .nv { color: #19177C } /* Name.Variable */\n",
       "body .ow { color: #AA22FF; font-weight: bold } /* Operator.Word */\n",
       "body .w { color: #bbbbbb } /* Text.Whitespace */\n",
       "body .mb { color: #666666 } /* Literal.Number.Bin */\n",
       "body .mf { color: #666666 } /* Literal.Number.Float */\n",
       "body .mh { color: #666666 } /* Literal.Number.Hex */\n",
       "body .mi { color: #666666 } /* Literal.Number.Integer */\n",
       "body .mo { color: #666666 } /* Literal.Number.Oct */\n",
       "body .sa { color: #BA2121 } /* Literal.String.Affix */\n",
       "body .sb { color: #BA2121 } /* Literal.String.Backtick */\n",
       "body .sc { color: #BA2121 } /* Literal.String.Char */\n",
       "body .dl { color: #BA2121 } /* Literal.String.Delimiter */\n",
       "body .sd { color: #BA2121; font-style: italic } /* Literal.String.Doc */\n",
       "body .s2 { color: #BA2121 } /* Literal.String.Double */\n",
       "body .se { color: #BB6622; font-weight: bold } /* Literal.String.Escape */\n",
       "body .sh { color: #BA2121 } /* Literal.String.Heredoc */\n",
       "body .si { color: #BB6688; font-weight: bold } /* Literal.String.Interpol */\n",
       "body .sx { color: #008000 } /* Literal.String.Other */\n",
       "body .sr { color: #BB6688 } /* Literal.String.Regex */\n",
       "body .s1 { color: #BA2121 } /* Literal.String.Single */\n",
       "body .ss { color: #19177C } /* Literal.String.Symbol */\n",
       "body .bp { color: #008000 } /* Name.Builtin.Pseudo */\n",
       "body .fm { color: #0000FF } /* Name.Function.Magic */\n",
       "body .vc { color: #19177C } /* Name.Variable.Class */\n",
       "body .vg { color: #19177C } /* Name.Variable.Global */\n",
       "body .vi { color: #19177C } /* Name.Variable.Instance */\n",
       "body .vm { color: #19177C } /* Name.Variable.Magic */\n",
       "body .il { color: #666666 } /* Literal.Number.Integer.Long */\n",
       "\n",
       "  </style>\n",
       "</head>\n",
       "<body>\n",
       "<h2></h2>\n",
       "\n",
       "<div class=\"highlight\"><pre><span></span><span class=\"k\">def</span> <span class=\"nf\">dpll_satisfiable</span><span class=\"p\">(</span><span class=\"n\">s</span><span class=\"p\">):</span>\n",
       "    <span class=\"sd\">&quot;&quot;&quot;Check satisfiability of a propositional sentence.</span>\n",
       "<span class=\"sd\">    This differs from the book code in two ways: (1) it returns a model</span>\n",
       "<span class=\"sd\">    rather than True when it succeeds; this is more useful. (2) The</span>\n",
       "<span class=\"sd\">    function find_pure_symbol is passed a list of unknown clauses, rather</span>\n",
       "<span class=\"sd\">    than a list of all clauses and the model; this is more efficient.&quot;&quot;&quot;</span>\n",
       "    <span class=\"n\">clauses</span> <span class=\"o\">=</span> <span class=\"n\">conjuncts</span><span class=\"p\">(</span><span class=\"n\">to_cnf</span><span class=\"p\">(</span><span class=\"n\">s</span><span class=\"p\">))</span>\n",
       "    <span class=\"n\">symbols</span> <span class=\"o\">=</span> <span class=\"nb\">list</span><span class=\"p\">(</span><span class=\"n\">prop_symbols</span><span class=\"p\">(</span><span class=\"n\">s</span><span class=\"p\">))</span>\n",
       "    <span class=\"k\">return</span> <span class=\"n\">dpll</span><span class=\"p\">(</span><span class=\"n\">clauses</span><span class=\"p\">,</span> <span class=\"n\">symbols</span><span class=\"p\">,</span> <span class=\"p\">{})</span>\n",
       "</pre></div>\n",
       "</body>\n",
       "</html>\n"
      ],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "psource(dpll_satisfiable)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Let's see a few examples of usage."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 50,
   "metadata": {},
   "outputs": [],
   "source": [
    "A, B, C, D = expr('A, B, C, D')"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 51,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "{A: True, B: True, C: False, D: True}"
      ]
     },
     "execution_count": 51,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "dpll_satisfiable(A & B & ~C & D)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "This is a simple case to highlight that the algorithm actually works."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 52,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "{B: True, D: False}"
      ]
     },
     "execution_count": 52,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "dpll_satisfiable((A & B) | (C & ~A) | (B & ~D))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "If a particular symbol isn't present in the solution, \n",
    "it means that the solution is independent of the value of that symbol.\n",
    "In this case, the solution is independent of A."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 53,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "{A: True, B: True}"
      ]
     },
     "execution_count": 53,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "dpll_satisfiable(A |'<=>'| B)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 54,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "{A: False, B: True, C: True}"
      ]
     },
     "execution_count": 54,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "dpll_satisfiable((A |'<=>'| B) |'==>'| (C & ~A))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 55,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "{B: True, C: True}"
      ]
     },
     "execution_count": 55,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "dpll_satisfiable((A | (B & C)) |'<=>'| ((A | B) & (A | C)))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### 2. WalkSAT algorithm\n",
    "This algorithm is very similar to Hill climbing.\n",
    "On every iteration, the algorithm picks an unsatisfied clause and flips a symbol in the clause.\n",
    "This is similar to finding a neighboring state in the `hill_climbing` algorithm.\n",
    "<br>\n",
    "The symbol to be flipped is decided by an evaluation function that counts the number of unsatisfied clauses.\n",
    "Sometimes, symbols are also flipped randomly, to avoid local optima. A subtle balance between greediness and randomness is required. Alternatively, some versions of the algorithm restart with a completely new random assignment if no solution has been found for too long, as a way of getting out of local minima of numbers of unsatisfied clauses.\n",
    "<br>\n",
    "<br>\n",
    "Let's have a look at the algorithm."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 56,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/html": [
       "<!DOCTYPE html PUBLIC \"-//W3C//DTD HTML 4.01//EN\"\n",
       "   \"http://www.w3.org/TR/html4/strict.dtd\">\n",
       "\n",
       "<html>\n",
       "<head>\n",
       "  <title></title>\n",
       "  <meta http-equiv=\"content-type\" content=\"text/html; charset=None\">\n",
       "  <style type=\"text/css\">\n",
       "td.linenos { background-color: #f0f0f0; padding-right: 10px; }\n",
       "span.lineno { background-color: #f0f0f0; padding: 0 5px 0 5px; }\n",
       "pre { line-height: 125%; }\n",
       "body .hll { background-color: #ffffcc }\n",
       "body  { background: #f8f8f8; }\n",
       "body .c { color: #408080; font-style: italic } /* Comment */\n",
       "body .err { border: 1px solid #FF0000 } /* Error */\n",
       "body .k { color: #008000; font-weight: bold } /* Keyword */\n",
       "body .o { color: #666666 } /* Operator */\n",
       "body .ch { color: #408080; font-style: italic } /* Comment.Hashbang */\n",
       "body .cm { color: #408080; font-style: italic } /* Comment.Multiline */\n",
       "body .cp { color: #BC7A00 } /* Comment.Preproc */\n",
       "body .cpf { color: #408080; font-style: italic } /* Comment.PreprocFile */\n",
       "body .c1 { color: #408080; font-style: italic } /* Comment.Single */\n",
       "body .cs { color: #408080; font-style: italic } /* Comment.Special */\n",
       "body .gd { color: #A00000 } /* Generic.Deleted */\n",
       "body .ge { font-style: italic } /* Generic.Emph */\n",
       "body .gr { color: #FF0000 } /* Generic.Error */\n",
       "body .gh { color: #000080; font-weight: bold } /* Generic.Heading */\n",
       "body .gi { color: #00A000 } /* Generic.Inserted */\n",
       "body .go { color: #888888 } /* Generic.Output */\n",
       "body .gp { color: #000080; font-weight: bold } /* Generic.Prompt */\n",
       "body .gs { font-weight: bold } /* Generic.Strong */\n",
       "body .gu { color: #800080; font-weight: bold } /* Generic.Subheading */\n",
       "body .gt { color: #0044DD } /* Generic.Traceback */\n",
       "body .kc { color: #008000; font-weight: bold } /* Keyword.Constant */\n",
       "body .kd { color: #008000; font-weight: bold } /* Keyword.Declaration */\n",
       "body .kn { color: #008000; font-weight: bold } /* Keyword.Namespace */\n",
       "body .kp { color: #008000 } /* Keyword.Pseudo */\n",
       "body .kr { color: #008000; font-weight: bold } /* Keyword.Reserved */\n",
       "body .kt { color: #B00040 } /* Keyword.Type */\n",
       "body .m { color: #666666 } /* Literal.Number */\n",
       "body .s { color: #BA2121 } /* Literal.String */\n",
       "body .na { color: #7D9029 } /* Name.Attribute */\n",
       "body .nb { color: #008000 } /* Name.Builtin */\n",
       "body .nc { color: #0000FF; font-weight: bold } /* Name.Class */\n",
       "body .no { color: #880000 } /* Name.Constant */\n",
       "body .nd { color: #AA22FF } /* Name.Decorator */\n",
       "body .ni { color: #999999; font-weight: bold } /* Name.Entity */\n",
       "body .ne { color: #D2413A; font-weight: bold } /* Name.Exception */\n",
       "body .nf { color: #0000FF } /* Name.Function */\n",
       "body .nl { color: #A0A000 } /* Name.Label */\n",
       "body .nn { color: #0000FF; font-weight: bold } /* Name.Namespace */\n",
       "body .nt { color: #008000; font-weight: bold } /* Name.Tag */\n",
       "body .nv { color: #19177C } /* Name.Variable */\n",
       "body .ow { color: #AA22FF; font-weight: bold } /* Operator.Word */\n",
       "body .w { color: #bbbbbb } /* Text.Whitespace */\n",
       "body .mb { color: #666666 } /* Literal.Number.Bin */\n",
       "body .mf { color: #666666 } /* Literal.Number.Float */\n",
       "body .mh { color: #666666 } /* Literal.Number.Hex */\n",
       "body .mi { color: #666666 } /* Literal.Number.Integer */\n",
       "body .mo { color: #666666 } /* Literal.Number.Oct */\n",
       "body .sa { color: #BA2121 } /* Literal.String.Affix */\n",
       "body .sb { color: #BA2121 } /* Literal.String.Backtick */\n",
       "body .sc { color: #BA2121 } /* Literal.String.Char */\n",
       "body .dl { color: #BA2121 } /* Literal.String.Delimiter */\n",
       "body .sd { color: #BA2121; font-style: italic } /* Literal.String.Doc */\n",
       "body .s2 { color: #BA2121 } /* Literal.String.Double */\n",
       "body .se { color: #BB6622; font-weight: bold } /* Literal.String.Escape */\n",
       "body .sh { color: #BA2121 } /* Literal.String.Heredoc */\n",
       "body .si { color: #BB6688; font-weight: bold } /* Literal.String.Interpol */\n",
       "body .sx { color: #008000 } /* Literal.String.Other */\n",
       "body .sr { color: #BB6688 } /* Literal.String.Regex */\n",
       "body .s1 { color: #BA2121 } /* Literal.String.Single */\n",
       "body .ss { color: #19177C } /* Literal.String.Symbol */\n",
       "body .bp { color: #008000 } /* Name.Builtin.Pseudo */\n",
       "body .fm { color: #0000FF } /* Name.Function.Magic */\n",
       "body .vc { color: #19177C } /* Name.Variable.Class */\n",
       "body .vg { color: #19177C } /* Name.Variable.Global */\n",
       "body .vi { color: #19177C } /* Name.Variable.Instance */\n",
       "body .vm { color: #19177C } /* Name.Variable.Magic */\n",
       "body .il { color: #666666 } /* Literal.Number.Integer.Long */\n",
       "\n",
       "  </style>\n",
       "</head>\n",
       "<body>\n",
       "<h2></h2>\n",
       "\n",
       "<div class=\"highlight\"><pre><span></span><span class=\"k\">def</span> <span class=\"nf\">WalkSAT</span><span class=\"p\">(</span><span class=\"n\">clauses</span><span class=\"p\">,</span> <span class=\"n\">p</span><span class=\"o\">=</span><span class=\"mf\">0.5</span><span class=\"p\">,</span> <span class=\"n\">max_flips</span><span class=\"o\">=</span><span class=\"mi\">10000</span><span class=\"p\">):</span>\n",
       "    <span class=\"sd\">&quot;&quot;&quot;Checks for satisfiability of all clauses by randomly flipping values of variables</span>\n",
       "<span class=\"sd\">    &quot;&quot;&quot;</span>\n",
       "    <span class=\"c1\"># Set of all symbols in all clauses</span>\n",
       "    <span class=\"n\">symbols</span> <span class=\"o\">=</span> <span class=\"p\">{</span><span class=\"n\">sym</span> <span class=\"k\">for</span> <span class=\"n\">clause</span> <span class=\"ow\">in</span> <span class=\"n\">clauses</span> <span class=\"k\">for</span> <span class=\"n\">sym</span> <span class=\"ow\">in</span> <span class=\"n\">prop_symbols</span><span class=\"p\">(</span><span class=\"n\">clause</span><span class=\"p\">)}</span>\n",
       "    <span class=\"c1\"># model is a random assignment of true/false to the symbols in clauses</span>\n",
       "    <span class=\"n\">model</span> <span class=\"o\">=</span> <span class=\"p\">{</span><span class=\"n\">s</span><span class=\"p\">:</span> <span class=\"n\">random</span><span class=\"o\">.</span><span class=\"n\">choice</span><span class=\"p\">([</span><span class=\"bp\">True</span><span class=\"p\">,</span> <span class=\"bp\">False</span><span class=\"p\">])</span> <span class=\"k\">for</span> <span class=\"n\">s</span> <span class=\"ow\">in</span> <span class=\"n\">symbols</span><span class=\"p\">}</span>\n",
       "    <span class=\"k\">for</span> <span class=\"n\">i</span> <span class=\"ow\">in</span> <span class=\"nb\">range</span><span class=\"p\">(</span><span class=\"n\">max_flips</span><span class=\"p\">):</span>\n",
       "        <span class=\"n\">satisfied</span><span class=\"p\">,</span> <span class=\"n\">unsatisfied</span> <span class=\"o\">=</span> <span class=\"p\">[],</span> <span class=\"p\">[]</span>\n",
       "        <span class=\"k\">for</span> <span class=\"n\">clause</span> <span class=\"ow\">in</span> <span class=\"n\">clauses</span><span class=\"p\">:</span>\n",
       "            <span class=\"p\">(</span><span class=\"n\">satisfied</span> <span class=\"k\">if</span> <span class=\"n\">pl_true</span><span class=\"p\">(</span><span class=\"n\">clause</span><span class=\"p\">,</span> <span class=\"n\">model</span><span class=\"p\">)</span> <span class=\"k\">else</span> <span class=\"n\">unsatisfied</span><span class=\"p\">)</span><span class=\"o\">.</span><span class=\"n\">append</span><span class=\"p\">(</span><span class=\"n\">clause</span><span class=\"p\">)</span>\n",
       "        <span class=\"k\">if</span> <span class=\"ow\">not</span> <span class=\"n\">unsatisfied</span><span class=\"p\">:</span>  <span class=\"c1\"># if model satisfies all the clauses</span>\n",
       "            <span class=\"k\">return</span> <span class=\"n\">model</span>\n",
       "        <span class=\"n\">clause</span> <span class=\"o\">=</span> <span class=\"n\">random</span><span class=\"o\">.</span><span class=\"n\">choice</span><span class=\"p\">(</span><span class=\"n\">unsatisfied</span><span class=\"p\">)</span>\n",
       "        <span class=\"k\">if</span> <span class=\"n\">probability</span><span class=\"p\">(</span><span class=\"n\">p</span><span class=\"p\">):</span>\n",
       "            <span class=\"n\">sym</span> <span class=\"o\">=</span> <span class=\"n\">random</span><span class=\"o\">.</span><span class=\"n\">choice</span><span class=\"p\">(</span><span class=\"nb\">list</span><span class=\"p\">(</span><span class=\"n\">prop_symbols</span><span class=\"p\">(</span><span class=\"n\">clause</span><span class=\"p\">)))</span>\n",
       "        <span class=\"k\">else</span><span class=\"p\">:</span>\n",
       "            <span class=\"c1\"># Flip the symbol in clause that maximizes number of sat. clauses</span>\n",
       "            <span class=\"k\">def</span> <span class=\"nf\">sat_count</span><span class=\"p\">(</span><span class=\"n\">sym</span><span class=\"p\">):</span>\n",
       "                <span class=\"c1\"># Return the the number of clauses satisfied after flipping the symbol.</span>\n",
       "                <span class=\"n\">model</span><span class=\"p\">[</span><span class=\"n\">sym</span><span class=\"p\">]</span> <span class=\"o\">=</span> <span class=\"ow\">not</span> <span class=\"n\">model</span><span class=\"p\">[</span><span class=\"n\">sym</span><span class=\"p\">]</span>\n",
       "                <span class=\"n\">count</span> <span class=\"o\">=</span> <span class=\"nb\">len</span><span class=\"p\">([</span><span class=\"n\">clause</span> <span class=\"k\">for</span> <span class=\"n\">clause</span> <span class=\"ow\">in</span> <span class=\"n\">clauses</span> <span class=\"k\">if</span> <span class=\"n\">pl_true</span><span class=\"p\">(</span><span class=\"n\">clause</span><span class=\"p\">,</span> <span class=\"n\">model</span><span class=\"p\">)])</span>\n",
       "                <span class=\"n\">model</span><span class=\"p\">[</span><span class=\"n\">sym</span><span class=\"p\">]</span> <span class=\"o\">=</span> <span class=\"ow\">not</span> <span class=\"n\">model</span><span class=\"p\">[</span><span class=\"n\">sym</span><span class=\"p\">]</span>\n",
       "                <span class=\"k\">return</span> <span class=\"n\">count</span>\n",
       "            <span class=\"n\">sym</span> <span class=\"o\">=</span> <span class=\"n\">argmax</span><span class=\"p\">(</span><span class=\"n\">prop_symbols</span><span class=\"p\">(</span><span class=\"n\">clause</span><span class=\"p\">),</span> <span class=\"n\">key</span><span class=\"o\">=</span><span class=\"n\">sat_count</span><span class=\"p\">)</span>\n",
       "        <span class=\"n\">model</span><span class=\"p\">[</span><span class=\"n\">sym</span><span class=\"p\">]</span> <span class=\"o\">=</span> <span class=\"ow\">not</span> <span class=\"n\">model</span><span class=\"p\">[</span><span class=\"n\">sym</span><span class=\"p\">]</span>\n",
       "    <span class=\"c1\"># If no solution is found within the flip limit, we return failure</span>\n",
       "    <span class=\"k\">return</span> <span class=\"bp\">None</span>\n",
       "</pre></div>\n",
       "</body>\n",
       "</html>\n"
      ],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "psource(WalkSAT)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "The function takes three arguments:\n",
    "<br>\n",
    "1. The `clauses` we want to satisfy.\n",
    "<br>\n",
    "2. The probability `p` of randomly changing a symbol.\n",
    "<br>\n",
    "3. The maximum number of flips (`max_flips`) the algorithm will run for. If the clauses are still unsatisfied, the algorithm returns `None` to denote failure.\n",
    "<br>\n",
    "The algorithm is identical in concept to Hill climbing and the code isn't difficult to understand.\n",
    "<br>\n",
    "<br>\n",
    "Let's see a few examples of usage."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 57,
   "metadata": {},
   "outputs": [],
   "source": [
    "A, B, C, D = expr('A, B, C, D')"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 58,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "{A: True, B: True, C: False, D: True}"
      ]
     },
     "execution_count": 58,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "WalkSAT([A, B, ~C, D], 0.5, 100)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "This is a simple case to show that the algorithm converges."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 59,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "{A: True, B: True, C: True}"
      ]
     },
     "execution_count": 59,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "WalkSAT([A & B, A & C], 0.5, 100)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 60,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "{A: True, B: True, C: True, D: True}"
      ]
     },
     "execution_count": 60,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "WalkSAT([A & B, C & D, C & B], 0.5, 100)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 61,
   "metadata": {},
   "outputs": [],
   "source": [
    "WalkSAT([A & B, C | D, ~(D | B)], 0.5, 1000)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "This one doesn't give any output because WalkSAT did not find any model where these clauses hold. We can solve these clauses to see that they together form a contradiction and hence, it isn't supposed to have a solution."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "One point of difference between this algorithm and the `dpll_satisfiable` algorithms is that both these algorithms take inputs differently. \n",
    "For WalkSAT to take complete sentences as input, \n",
    "we can write a helper function that converts the input sentence into conjunctive normal form and then calls WalkSAT with the list of conjuncts of the CNF form of the sentence."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 62,
   "metadata": {},
   "outputs": [],
   "source": [
    "def WalkSAT_CNF(sentence, p=0.5, max_flips=10000):\n",
    "    return WalkSAT(conjuncts(to_cnf(sentence)), 0, max_flips)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Now we can call `WalkSAT_CNF` and `DPLL_Satisfiable` with the same arguments."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 63,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "{A: False, B: False, C: True, D: False}"
      ]
     },
     "execution_count": 63,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "WalkSAT_CNF((A & B) | (C & ~A) | (B & ~D), 0.5, 1000)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "It works!\n",
    "<br>\n",
    "Notice that the solution generated by WalkSAT doesn't omit variables that the sentence doesn't depend upon. \n",
    "If the sentence is independent of a particular variable, the solution contains a random value for that variable because of the stochastic nature of the algorithm.\n",
    "<br>\n",
    "<br>\n",
    "Let's compare the runtime of WalkSAT and DPLL for a few cases. We will use the `%%timeit` magic to do this."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 64,
   "metadata": {},
   "outputs": [],
   "source": [
    "sentence_1 = A |'<=>'| B\n",
    "sentence_2 = (A & B) | (C & ~A) | (B & ~D)\n",
    "sentence_3 = (A | (B & C)) |'<=>'| ((A | B) & (A | C))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 65,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "6.78 ms ± 238 µs per loop (mean ± std. dev. of 7 runs, 100 loops each)\n"
     ]
    }
   ],
   "source": [
    "%%timeit\n",
    "dpll_satisfiable(sentence_1)\n",
    "dpll_satisfiable(sentence_2)\n",
    "dpll_satisfiable(sentence_3)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 66,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "4.64 ms ± 65.3 µs per loop (mean ± std. dev. of 7 runs, 100 loops each)\n"
     ]
    }
   ],
   "source": [
    "%%timeit\n",
    "WalkSAT_CNF(sentence_1)\n",
    "WalkSAT_CNF(sentence_2)\n",
    "WalkSAT_CNF(sentence_3)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "On an average, for solvable cases, `WalkSAT` is quite faster than `dpll` because, for a small number of variables, \n",
    "`WalkSAT` can reduce the search space significantly. \n",
    "Results can be different for sentences with more symbols though.\n",
    "Feel free to play around with this to understand the trade-offs of these algorithms better."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### SATPlan"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "In this section we show how to make plans by logical inference. The basic idea is very simple. It includes the following three steps:\n",
    "1. Constuct a sentence that includes:\n",
    "    1. A colection of assertions about the initial state.\n",
    "    2. The successor-state axioms for all the possible actions at each time up to some maximum time t.\n",
    "    3. The assertion that the goal is achieved at time t.\n",
    "2. Present the whole sentence to a SAT solver.\n",
    "3. Assuming a model is found, extract from the model those variables that represent actions and are assigned true. Together they represent a plan to achieve the goals.\n",
    "\n",
    "\n",
    "Lets have a look at the algorithm"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 67,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/html": [
       "<!DOCTYPE html PUBLIC \"-//W3C//DTD HTML 4.01//EN\"\n",
       "   \"http://www.w3.org/TR/html4/strict.dtd\">\n",
       "\n",
       "<html>\n",
       "<head>\n",
       "  <title></title>\n",
       "  <meta http-equiv=\"content-type\" content=\"text/html; charset=None\">\n",
       "  <style type=\"text/css\">\n",
       "td.linenos { background-color: #f0f0f0; padding-right: 10px; }\n",
       "span.lineno { background-color: #f0f0f0; padding: 0 5px 0 5px; }\n",
       "pre { line-height: 125%; }\n",
       "body .hll { background-color: #ffffcc }\n",
       "body  { background: #f8f8f8; }\n",
       "body .c { color: #408080; font-style: italic } /* Comment */\n",
       "body .err { border: 1px solid #FF0000 } /* Error */\n",
       "body .k { color: #008000; font-weight: bold } /* Keyword */\n",
       "body .o { color: #666666 } /* Operator */\n",
       "body .ch { color: #408080; font-style: italic } /* Comment.Hashbang */\n",
       "body .cm { color: #408080; font-style: italic } /* Comment.Multiline */\n",
       "body .cp { color: #BC7A00 } /* Comment.Preproc */\n",
       "body .cpf { color: #408080; font-style: italic } /* Comment.PreprocFile */\n",
       "body .c1 { color: #408080; font-style: italic } /* Comment.Single */\n",
       "body .cs { color: #408080; font-style: italic } /* Comment.Special */\n",
       "body .gd { color: #A00000 } /* Generic.Deleted */\n",
       "body .ge { font-style: italic } /* Generic.Emph */\n",
       "body .gr { color: #FF0000 } /* Generic.Error */\n",
       "body .gh { color: #000080; font-weight: bold } /* Generic.Heading */\n",
       "body .gi { color: #00A000 } /* Generic.Inserted */\n",
       "body .go { color: #888888 } /* Generic.Output */\n",
       "body .gp { color: #000080; font-weight: bold } /* Generic.Prompt */\n",
       "body .gs { font-weight: bold } /* Generic.Strong */\n",
       "body .gu { color: #800080; font-weight: bold } /* Generic.Subheading */\n",
       "body .gt { color: #0044DD } /* Generic.Traceback */\n",
       "body .kc { color: #008000; font-weight: bold } /* Keyword.Constant */\n",
       "body .kd { color: #008000; font-weight: bold } /* Keyword.Declaration */\n",
       "body .kn { color: #008000; font-weight: bold } /* Keyword.Namespace */\n",
       "body .kp { color: #008000 } /* Keyword.Pseudo */\n",
       "body .kr { color: #008000; font-weight: bold } /* Keyword.Reserved */\n",
       "body .kt { color: #B00040 } /* Keyword.Type */\n",
       "body .m { color: #666666 } /* Literal.Number */\n",
       "body .s { color: #BA2121 } /* Literal.String */\n",
       "body .na { color: #7D9029 } /* Name.Attribute */\n",
       "body .nb { color: #008000 } /* Name.Builtin */\n",
       "body .nc { color: #0000FF; font-weight: bold } /* Name.Class */\n",
       "body .no { color: #880000 } /* Name.Constant */\n",
       "body .nd { color: #AA22FF } /* Name.Decorator */\n",
       "body .ni { color: #999999; font-weight: bold } /* Name.Entity */\n",
       "body .ne { color: #D2413A; font-weight: bold } /* Name.Exception */\n",
       "body .nf { color: #0000FF } /* Name.Function */\n",
       "body .nl { color: #A0A000 } /* Name.Label */\n",
       "body .nn { color: #0000FF; font-weight: bold } /* Name.Namespace */\n",
       "body .nt { color: #008000; font-weight: bold } /* Name.Tag */\n",
       "body .nv { color: #19177C } /* Name.Variable */\n",
       "body .ow { color: #AA22FF; font-weight: bold } /* Operator.Word */\n",
       "body .w { color: #bbbbbb } /* Text.Whitespace */\n",
       "body .mb { color: #666666 } /* Literal.Number.Bin */\n",
       "body .mf { color: #666666 } /* Literal.Number.Float */\n",
       "body .mh { color: #666666 } /* Literal.Number.Hex */\n",
       "body .mi { color: #666666 } /* Literal.Number.Integer */\n",
       "body .mo { color: #666666 } /* Literal.Number.Oct */\n",
       "body .sa { color: #BA2121 } /* Literal.String.Affix */\n",
       "body .sb { color: #BA2121 } /* Literal.String.Backtick */\n",
       "body .sc { color: #BA2121 } /* Literal.String.Char */\n",
       "body .dl { color: #BA2121 } /* Literal.String.Delimiter */\n",
       "body .sd { color: #BA2121; font-style: italic } /* Literal.String.Doc */\n",
       "body .s2 { color: #BA2121 } /* Literal.String.Double */\n",
       "body .se { color: #BB6622; font-weight: bold } /* Literal.String.Escape */\n",
       "body .sh { color: #BA2121 } /* Literal.String.Heredoc */\n",
       "body .si { color: #BB6688; font-weight: bold } /* Literal.String.Interpol */\n",
       "body .sx { color: #008000 } /* Literal.String.Other */\n",
       "body .sr { color: #BB6688 } /* Literal.String.Regex */\n",
       "body .s1 { color: #BA2121 } /* Literal.String.Single */\n",
       "body .ss { color: #19177C } /* Literal.String.Symbol */\n",
       "body .bp { color: #008000 } /* Name.Builtin.Pseudo */\n",
       "body .fm { color: #0000FF } /* Name.Function.Magic */\n",
       "body .vc { color: #19177C } /* Name.Variable.Class */\n",
       "body .vg { color: #19177C } /* Name.Variable.Global */\n",
       "body .vi { color: #19177C } /* Name.Variable.Instance */\n",
       "body .vm { color: #19177C } /* Name.Variable.Magic */\n",
       "body .il { color: #666666 } /* Literal.Number.Integer.Long */\n",
       "\n",
       "  </style>\n",
       "</head>\n",
       "<body>\n",
       "<h2></h2>\n",
       "\n",
       "<div class=\"highlight\"><pre><span></span><span class=\"k\">def</span> <span class=\"nf\">SAT_plan</span><span class=\"p\">(</span><span class=\"n\">init</span><span class=\"p\">,</span> <span class=\"n\">transition</span><span class=\"p\">,</span> <span class=\"n\">goal</span><span class=\"p\">,</span> <span class=\"n\">t_max</span><span class=\"p\">,</span> <span class=\"n\">SAT_solver</span><span class=\"o\">=</span><span class=\"n\">dpll_satisfiable</span><span class=\"p\">):</span>\n",
       "    <span class=\"sd\">&quot;&quot;&quot;Converts a planning problem to Satisfaction problem by translating it to a cnf sentence.</span>\n",
       "<span class=\"sd\">    [Figure 7.22]&quot;&quot;&quot;</span>\n",
       "\n",
       "    <span class=\"c1\"># Functions used by SAT_plan</span>\n",
       "    <span class=\"k\">def</span> <span class=\"nf\">translate_to_SAT</span><span class=\"p\">(</span><span class=\"n\">init</span><span class=\"p\">,</span> <span class=\"n\">transition</span><span class=\"p\">,</span> <span class=\"n\">goal</span><span class=\"p\">,</span> <span class=\"n\">time</span><span class=\"p\">):</span>\n",
       "        <span class=\"n\">clauses</span> <span class=\"o\">=</span> <span class=\"p\">[]</span>\n",
       "        <span class=\"n\">states</span> <span class=\"o\">=</span> <span class=\"p\">[</span><span class=\"n\">state</span> <span class=\"k\">for</span> <span class=\"n\">state</span> <span class=\"ow\">in</span> <span class=\"n\">transition</span><span class=\"p\">]</span>\n",
       "\n",
       "        <span class=\"c1\"># Symbol claiming state s at time t</span>\n",
       "        <span class=\"n\">state_counter</span> <span class=\"o\">=</span> <span class=\"n\">itertools</span><span class=\"o\">.</span><span class=\"n\">count</span><span class=\"p\">()</span>\n",
       "        <span class=\"k\">for</span> <span class=\"n\">s</span> <span class=\"ow\">in</span> <span class=\"n\">states</span><span class=\"p\">:</span>\n",
       "            <span class=\"k\">for</span> <span class=\"n\">t</span> <span class=\"ow\">in</span> <span class=\"nb\">range</span><span class=\"p\">(</span><span class=\"n\">time</span><span class=\"o\">+</span><span class=\"mi\">1</span><span class=\"p\">):</span>\n",
       "                <span class=\"n\">state_sym</span><span class=\"p\">[</span><span class=\"n\">s</span><span class=\"p\">,</span> <span class=\"n\">t</span><span class=\"p\">]</span> <span class=\"o\">=</span> <span class=\"n\">Expr</span><span class=\"p\">(</span><span class=\"s2\">&quot;State_{}&quot;</span><span class=\"o\">.</span><span class=\"n\">format</span><span class=\"p\">(</span><span class=\"nb\">next</span><span class=\"p\">(</span><span class=\"n\">state_counter</span><span class=\"p\">)))</span>\n",
       "\n",
       "        <span class=\"c1\"># Add initial state axiom</span>\n",
       "        <span class=\"n\">clauses</span><span class=\"o\">.</span><span class=\"n\">append</span><span class=\"p\">(</span><span class=\"n\">state_sym</span><span class=\"p\">[</span><span class=\"n\">init</span><span class=\"p\">,</span> <span class=\"mi\">0</span><span class=\"p\">])</span>\n",
       "\n",
       "        <span class=\"c1\"># Add goal state axiom</span>\n",
       "        <span class=\"n\">clauses</span><span class=\"o\">.</span><span class=\"n\">append</span><span class=\"p\">(</span><span class=\"n\">state_sym</span><span class=\"p\">[</span><span class=\"n\">goal</span><span class=\"p\">,</span> <span class=\"n\">time</span><span class=\"p\">])</span>\n",
       "\n",
       "        <span class=\"c1\"># All possible transitions</span>\n",
       "        <span class=\"n\">transition_counter</span> <span class=\"o\">=</span> <span class=\"n\">itertools</span><span class=\"o\">.</span><span class=\"n\">count</span><span class=\"p\">()</span>\n",
       "        <span class=\"k\">for</span> <span class=\"n\">s</span> <span class=\"ow\">in</span> <span class=\"n\">states</span><span class=\"p\">:</span>\n",
       "            <span class=\"k\">for</span> <span class=\"n\">action</span> <span class=\"ow\">in</span> <span class=\"n\">transition</span><span class=\"p\">[</span><span class=\"n\">s</span><span class=\"p\">]:</span>\n",
       "                <span class=\"n\">s_</span> <span class=\"o\">=</span> <span class=\"n\">transition</span><span class=\"p\">[</span><span class=\"n\">s</span><span class=\"p\">][</span><span class=\"n\">action</span><span class=\"p\">]</span>\n",
       "                <span class=\"k\">for</span> <span class=\"n\">t</span> <span class=\"ow\">in</span> <span class=\"nb\">range</span><span class=\"p\">(</span><span class=\"n\">time</span><span class=\"p\">):</span>\n",
       "                    <span class=\"c1\"># Action &#39;action&#39; taken from state &#39;s&#39; at time &#39;t&#39; to reach &#39;s_&#39;</span>\n",
       "                    <span class=\"n\">action_sym</span><span class=\"p\">[</span><span class=\"n\">s</span><span class=\"p\">,</span> <span class=\"n\">action</span><span class=\"p\">,</span> <span class=\"n\">t</span><span class=\"p\">]</span> <span class=\"o\">=</span> <span class=\"n\">Expr</span><span class=\"p\">(</span>\n",
       "                        <span class=\"s2\">&quot;Transition_{}&quot;</span><span class=\"o\">.</span><span class=\"n\">format</span><span class=\"p\">(</span><span class=\"nb\">next</span><span class=\"p\">(</span><span class=\"n\">transition_counter</span><span class=\"p\">)))</span>\n",
       "\n",
       "                    <span class=\"c1\"># Change the state from s to s_</span>\n",
       "                    <span class=\"n\">clauses</span><span class=\"o\">.</span><span class=\"n\">append</span><span class=\"p\">(</span><span class=\"n\">action_sym</span><span class=\"p\">[</span><span class=\"n\">s</span><span class=\"p\">,</span> <span class=\"n\">action</span><span class=\"p\">,</span> <span class=\"n\">t</span><span class=\"p\">]</span> <span class=\"o\">|</span><span class=\"s1\">&#39;==&gt;&#39;</span><span class=\"o\">|</span> <span class=\"n\">state_sym</span><span class=\"p\">[</span><span class=\"n\">s</span><span class=\"p\">,</span> <span class=\"n\">t</span><span class=\"p\">])</span>\n",
       "                    <span class=\"n\">clauses</span><span class=\"o\">.</span><span class=\"n\">append</span><span class=\"p\">(</span><span class=\"n\">action_sym</span><span class=\"p\">[</span><span class=\"n\">s</span><span class=\"p\">,</span> <span class=\"n\">action</span><span class=\"p\">,</span> <span class=\"n\">t</span><span class=\"p\">]</span> <span class=\"o\">|</span><span class=\"s1\">&#39;==&gt;&#39;</span><span class=\"o\">|</span> <span class=\"n\">state_sym</span><span class=\"p\">[</span><span class=\"n\">s_</span><span class=\"p\">,</span> <span class=\"n\">t</span> <span class=\"o\">+</span> <span class=\"mi\">1</span><span class=\"p\">])</span>\n",
       "\n",
       "        <span class=\"c1\"># Allow only one state at any time</span>\n",
       "        <span class=\"k\">for</span> <span class=\"n\">t</span> <span class=\"ow\">in</span> <span class=\"nb\">range</span><span class=\"p\">(</span><span class=\"n\">time</span><span class=\"o\">+</span><span class=\"mi\">1</span><span class=\"p\">):</span>\n",
       "            <span class=\"c1\"># must be a state at any time</span>\n",
       "            <span class=\"n\">clauses</span><span class=\"o\">.</span><span class=\"n\">append</span><span class=\"p\">(</span><span class=\"n\">associate</span><span class=\"p\">(</span><span class=\"s1\">&#39;|&#39;</span><span class=\"p\">,</span> <span class=\"p\">[</span><span class=\"n\">state_sym</span><span class=\"p\">[</span><span class=\"n\">s</span><span class=\"p\">,</span> <span class=\"n\">t</span><span class=\"p\">]</span> <span class=\"k\">for</span> <span class=\"n\">s</span> <span class=\"ow\">in</span> <span class=\"n\">states</span><span class=\"p\">]))</span>\n",
       "\n",
       "            <span class=\"k\">for</span> <span class=\"n\">s</span> <span class=\"ow\">in</span> <span class=\"n\">states</span><span class=\"p\">:</span>\n",
       "                <span class=\"k\">for</span> <span class=\"n\">s_</span> <span class=\"ow\">in</span> <span class=\"n\">states</span><span class=\"p\">[</span><span class=\"n\">states</span><span class=\"o\">.</span><span class=\"n\">index</span><span class=\"p\">(</span><span class=\"n\">s</span><span class=\"p\">)</span> <span class=\"o\">+</span> <span class=\"mi\">1</span><span class=\"p\">:]:</span>\n",
       "                    <span class=\"c1\"># for each pair of states s, s_ only one is possible at time t</span>\n",
       "                    <span class=\"n\">clauses</span><span class=\"o\">.</span><span class=\"n\">append</span><span class=\"p\">((</span><span class=\"o\">~</span><span class=\"n\">state_sym</span><span class=\"p\">[</span><span class=\"n\">s</span><span class=\"p\">,</span> <span class=\"n\">t</span><span class=\"p\">])</span> <span class=\"o\">|</span> <span class=\"p\">(</span><span class=\"o\">~</span><span class=\"n\">state_sym</span><span class=\"p\">[</span><span class=\"n\">s_</span><span class=\"p\">,</span> <span class=\"n\">t</span><span class=\"p\">]))</span>\n",
       "\n",
       "        <span class=\"c1\"># Restrict to one transition per timestep</span>\n",
       "        <span class=\"k\">for</span> <span class=\"n\">t</span> <span class=\"ow\">in</span> <span class=\"nb\">range</span><span class=\"p\">(</span><span class=\"n\">time</span><span class=\"p\">):</span>\n",
       "            <span class=\"c1\"># list of possible transitions at time t</span>\n",
       "            <span class=\"n\">transitions_t</span> <span class=\"o\">=</span> <span class=\"p\">[</span><span class=\"n\">tr</span> <span class=\"k\">for</span> <span class=\"n\">tr</span> <span class=\"ow\">in</span> <span class=\"n\">action_sym</span> <span class=\"k\">if</span> <span class=\"n\">tr</span><span class=\"p\">[</span><span class=\"mi\">2</span><span class=\"p\">]</span> <span class=\"o\">==</span> <span class=\"n\">t</span><span class=\"p\">]</span>\n",
       "\n",
       "            <span class=\"c1\"># make sure at least one of the transitions happens</span>\n",
       "            <span class=\"n\">clauses</span><span class=\"o\">.</span><span class=\"n\">append</span><span class=\"p\">(</span><span class=\"n\">associate</span><span class=\"p\">(</span><span class=\"s1\">&#39;|&#39;</span><span class=\"p\">,</span> <span class=\"p\">[</span><span class=\"n\">action_sym</span><span class=\"p\">[</span><span class=\"n\">tr</span><span class=\"p\">]</span> <span class=\"k\">for</span> <span class=\"n\">tr</span> <span class=\"ow\">in</span> <span class=\"n\">transitions_t</span><span class=\"p\">]))</span>\n",
       "\n",
       "            <span class=\"k\">for</span> <span class=\"n\">tr</span> <span class=\"ow\">in</span> <span class=\"n\">transitions_t</span><span class=\"p\">:</span>\n",
       "                <span class=\"k\">for</span> <span class=\"n\">tr_</span> <span class=\"ow\">in</span> <span class=\"n\">transitions_t</span><span class=\"p\">[</span><span class=\"n\">transitions_t</span><span class=\"o\">.</span><span class=\"n\">index</span><span class=\"p\">(</span><span class=\"n\">tr</span><span class=\"p\">)</span> <span class=\"o\">+</span> <span class=\"mi\">1</span><span class=\"p\">:]:</span>\n",
       "                    <span class=\"c1\"># there cannot be two transitions tr and tr_ at time t</span>\n",
       "                    <span class=\"n\">clauses</span><span class=\"o\">.</span><span class=\"n\">append</span><span class=\"p\">(</span><span class=\"o\">~</span><span class=\"n\">action_sym</span><span class=\"p\">[</span><span class=\"n\">tr</span><span class=\"p\">]</span> <span class=\"o\">|</span> <span class=\"o\">~</span><span class=\"n\">action_sym</span><span class=\"p\">[</span><span class=\"n\">tr_</span><span class=\"p\">])</span>\n",
       "\n",
       "        <span class=\"c1\"># Combine the clauses to form the cnf</span>\n",
       "        <span class=\"k\">return</span> <span class=\"n\">associate</span><span class=\"p\">(</span><span class=\"s1\">&#39;&amp;&#39;</span><span class=\"p\">,</span> <span class=\"n\">clauses</span><span class=\"p\">)</span>\n",
       "\n",
       "    <span class=\"k\">def</span> <span class=\"nf\">extract_solution</span><span class=\"p\">(</span><span class=\"n\">model</span><span class=\"p\">):</span>\n",
       "        <span class=\"n\">true_transitions</span> <span class=\"o\">=</span> <span class=\"p\">[</span><span class=\"n\">t</span> <span class=\"k\">for</span> <span class=\"n\">t</span> <span class=\"ow\">in</span> <span class=\"n\">action_sym</span> <span class=\"k\">if</span> <span class=\"n\">model</span><span class=\"p\">[</span><span class=\"n\">action_sym</span><span class=\"p\">[</span><span class=\"n\">t</span><span class=\"p\">]]]</span>\n",
       "        <span class=\"c1\"># Sort transitions based on time, which is the 3rd element of the tuple</span>\n",
       "        <span class=\"n\">true_transitions</span><span class=\"o\">.</span><span class=\"n\">sort</span><span class=\"p\">(</span><span class=\"n\">key</span><span class=\"o\">=</span><span class=\"k\">lambda</span> <span class=\"n\">x</span><span class=\"p\">:</span> <span class=\"n\">x</span><span class=\"p\">[</span><span class=\"mi\">2</span><span class=\"p\">])</span>\n",
       "        <span class=\"k\">return</span> <span class=\"p\">[</span><span class=\"n\">action</span> <span class=\"k\">for</span> <span class=\"n\">s</span><span class=\"p\">,</span> <span class=\"n\">action</span><span class=\"p\">,</span> <span class=\"n\">time</span> <span class=\"ow\">in</span> <span class=\"n\">true_transitions</span><span class=\"p\">]</span>\n",
       "\n",
       "    <span class=\"c1\"># Body of SAT_plan algorithm</span>\n",
       "    <span class=\"k\">for</span> <span class=\"n\">t</span> <span class=\"ow\">in</span> <span class=\"nb\">range</span><span class=\"p\">(</span><span class=\"n\">t_max</span><span class=\"p\">):</span>\n",
       "        <span class=\"c1\"># dictionaries to help extract the solution from model</span>\n",
       "        <span class=\"n\">state_sym</span> <span class=\"o\">=</span> <span class=\"p\">{}</span>\n",
       "        <span class=\"n\">action_sym</span> <span class=\"o\">=</span> <span class=\"p\">{}</span>\n",
       "\n",
       "        <span class=\"n\">cnf</span> <span class=\"o\">=</span> <span class=\"n\">translate_to_SAT</span><span class=\"p\">(</span><span class=\"n\">init</span><span class=\"p\">,</span> <span class=\"n\">transition</span><span class=\"p\">,</span> <span class=\"n\">goal</span><span class=\"p\">,</span> <span class=\"n\">t</span><span class=\"p\">)</span>\n",
       "        <span class=\"n\">model</span> <span class=\"o\">=</span> <span class=\"n\">SAT_solver</span><span class=\"p\">(</span><span class=\"n\">cnf</span><span class=\"p\">)</span>\n",
       "        <span class=\"k\">if</span> <span class=\"n\">model</span> <span class=\"ow\">is</span> <span class=\"ow\">not</span> <span class=\"bp\">False</span><span class=\"p\">:</span>\n",
       "            <span class=\"k\">return</span> <span class=\"n\">extract_solution</span><span class=\"p\">(</span><span class=\"n\">model</span><span class=\"p\">)</span>\n",
       "    <span class=\"k\">return</span> <span class=\"bp\">None</span>\n",
       "</pre></div>\n",
       "</body>\n",
       "</html>\n"
      ],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "psource(SAT_plan)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Let's see few examples of its usage. First we define a transition and then call `SAT_plan`."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 68,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "None\n",
      "['Right']\n",
      "['Left', 'Left']\n"
     ]
    }
   ],
   "source": [
    "transition = {'A': {'Left': 'A', 'Right': 'B'},\n",
    "            'B': {'Left': 'A', 'Right': 'C'},\n",
    "            'C': {'Left': 'B', 'Right': 'C'}}\n",
    "\n",
    "\n",
    "print(SAT_plan('A', transition, 'C', 2)) \n",
    "print(SAT_plan('A', transition, 'B', 3))\n",
    "print(SAT_plan('C', transition, 'A', 3))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Let us do the same for another transition."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 69,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "['Right', 'Down']\n"
     ]
    }
   ],
   "source": [
    "transition = {(0, 0): {'Right': (0, 1), 'Down': (1, 0)},\n",
    "            (0, 1): {'Left': (1, 0), 'Down': (1, 1)},\n",
    "            (1, 0): {'Right': (1, 0), 'Up': (1, 0), 'Left': (1, 0), 'Down': (1, 0)},\n",
    "            (1, 1): {'Left': (1, 0), 'Up': (0, 1)}}\n",
    "\n",
    "\n",
    "print(SAT_plan((0, 0), transition, (1, 1), 4))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## First-Order Logic Knowledge Bases: `FolKB`\n",
    "\n",
    "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."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Criminal KB\n",
    "In this section we create a `FolKB` based on the following paragraph.<br/>\n",
    "<em>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.</em><br/>\n",
    "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. Fortunately, we have a small paragraph and can do extraction and conversion manually. We'll store the clauses in list aptly named `clauses`."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 48,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "clauses = []"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "<em>“... it is a crime for an American to sell weapons to hostile nations”</em><br/>\n",
    "The keywords to look for here are 'crime', 'American', 'sell', 'weapon' and 'hostile'. We use predicate symbols to make meaning of them.\n",
    "\n",
    "* `Criminal(x)`: `x` is a criminal\n",
    "* `American(x)`: `x` is an American\n",
    "* `Sells(x ,y, z)`: `x` sells `y` to `z`\n",
    "* `Weapon(x)`: `x` is a weapon\n",
    "* `Hostile(x)`: `x` is a hostile nation\n",
    "\n",
    "Let us now combine them with appropriate variable naming to depict the meaning of the sentence. The criminal `x` is also the American `x` who sells weapon `y` to `z`, which is a hostile nation.\n",
    "\n",
    "$\\text{American}(x) \\land \\text{Weapon}(y) \\land \\text{Sells}(x, y, z) \\land \\text{Hostile}(z) \\implies \\text{Criminal} (x)$"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 49,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "clauses.append(expr(\"(American(x) & Weapon(y) & Sells(x, y, z) & Hostile(z)) ==> Criminal(x)\"))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "<em>\"The country Nono, an enemy of America\"</em><br/>\n",
    "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`.\n",
    "\n",
    "$\\text{Enemy}(\\text{Nono}, \\text{America})$"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 50,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "clauses.append(expr(\"Enemy(Nono, America)\"))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "<em>\"Nono ... has some missiles\"</em><br/>\n",
    "This states the existence 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.\n",
    "\n",
    "$\\text{Owns}(\\text{Nono}, \\text{M1}), \\text{Missile}(\\text{M1})$"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 51,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "clauses.append(expr(\"Owns(Nono, M1)\"))\n",
    "clauses.append(expr(\"Missile(M1)\"))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "collapsed": true
   },
   "source": [
    "<em>\"All of its missiles were sold to it by Colonel West\"</em><br/>\n",
    "If Nono owns something and it classifies as a missile, then it was sold to Nono by West.\n",
    "\n",
    "$\\text{Missile}(x) \\land \\text{Owns}(\\text{Nono}, x) \\implies \\text{Sells}(\\text{West}, x, \\text{Nono})$"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 52,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "clauses.append(expr(\"(Missile(x) & Owns(Nono, x)) ==> Sells(West, x, Nono)\"))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "<em>\"West, who is American\"</em><br/>\n",
    "West is an American.\n",
    "\n",
    "$\\text{American}(\\text{West})$"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 53,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "clauses.append(expr(\"American(West)\"))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "We also know, from our understanding of language, that missiles are weapons and that an enemy of America counts as “hostile”.\n",
    "\n",
    "$\\text{Missile}(x) \\implies \\text{Weapon}(x), \\text{Enemy}(x, \\text{America}) \\implies \\text{Hostile}(x)$"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 54,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "clauses.append(expr(\"Missile(x) ==> Weapon(x)\"))\n",
    "clauses.append(expr(\"Enemy(x, America) ==> Hostile(x)\"))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Now that we have converted the information into first-order definite clauses we can create our first-order logic knowledge base."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 55,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "crime_kb = FolKB(clauses)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Inference in First-Order Logic\n",
    "In this section we look at a forward chaining and a backward chaining algorithm for `FolKB`. Both aforementioned algorithms rely on a process called <strong>unification</strong>, a key component of all first-order inference algorithms."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Unification\n",
    "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 <em>unifier</em> 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."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 56,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "{x: 3}"
      ]
     },
     "execution_count": 56,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "unify(expr('x'), 3)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 57,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "{x: B}"
      ]
     },
     "execution_count": 57,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "unify(expr('A(x)'), expr('A(B)'))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 58,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "{x: Bella, y: Dobby}"
      ]
     },
     "execution_count": 58,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "unify(expr('Cat(x) & Dog(Dobby)'), expr('Cat(Bella) & Dog(y)'))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "In cases where there is no possible substitution that unifies the two sentences the function return `None`."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 59,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "None\n"
     ]
    }
   ],
   "source": [
    "print(unify(expr('Cat(x)'), expr('Dog(Dobby)')))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "We also need to take care we do not unintentionally use the same variable name. Unify treats them as a single variable which prevents it from taking multiple value."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 60,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "None\n"
     ]
    }
   ],
   "source": [
    "print(unify(expr('Cat(x) & Dog(Dobby)'), expr('Cat(Bella) & Dog(x)')))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Forward Chaining Algorithm\n",
    "We consider the simple forward-chaining algorithm presented in <em>Figure 9.3</em>. 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 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 added. 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.\n",
    "\n",
    "The function `fol_fc_ask` is a generator which yields all substitutions which validate the query."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 61,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/html": [
       "<!DOCTYPE html PUBLIC \"-//W3C//DTD HTML 4.01//EN\"\n",
       "   \"http://www.w3.org/TR/html4/strict.dtd\">\n",
       "\n",
       "<html>\n",
       "<head>\n",
       "  <title></title>\n",
       "  <meta http-equiv=\"content-type\" content=\"text/html; charset=None\">\n",
       "  <style type=\"text/css\">\n",
       "td.linenos { background-color: #f0f0f0; padding-right: 10px; }\n",
       "span.lineno { background-color: #f0f0f0; padding: 0 5px 0 5px; }\n",
       "pre { line-height: 125%; }\n",
       "body .hll { background-color: #ffffcc }\n",
       "body  { background: #f8f8f8; }\n",
       "body .c { color: #408080; font-style: italic } /* Comment */\n",
       "body .err { border: 1px solid #FF0000 } /* Error */\n",
       "body .k { color: #008000; font-weight: bold } /* Keyword */\n",
       "body .o { color: #666666 } /* Operator */\n",
       "body .ch { color: #408080; font-style: italic } /* Comment.Hashbang */\n",
       "body .cm { color: #408080; font-style: italic } /* Comment.Multiline */\n",
       "body .cp { color: #BC7A00 } /* Comment.Preproc */\n",
       "body .cpf { color: #408080; font-style: italic } /* Comment.PreprocFile */\n",
       "body .c1 { color: #408080; font-style: italic } /* Comment.Single */\n",
       "body .cs { color: #408080; font-style: italic } /* Comment.Special */\n",
       "body .gd { color: #A00000 } /* Generic.Deleted */\n",
       "body .ge { font-style: italic } /* Generic.Emph */\n",
       "body .gr { color: #FF0000 } /* Generic.Error */\n",
       "body .gh { color: #000080; font-weight: bold } /* Generic.Heading */\n",
       "body .gi { color: #00A000 } /* Generic.Inserted */\n",
       "body .go { color: #888888 } /* Generic.Output */\n",
       "body .gp { color: #000080; font-weight: bold } /* Generic.Prompt */\n",
       "body .gs { font-weight: bold } /* Generic.Strong */\n",
       "body .gu { color: #800080; font-weight: bold } /* Generic.Subheading */\n",
       "body .gt { color: #0044DD } /* Generic.Traceback */\n",
       "body .kc { color: #008000; font-weight: bold } /* Keyword.Constant */\n",
       "body .kd { color: #008000; font-weight: bold } /* Keyword.Declaration */\n",
       "body .kn { color: #008000; font-weight: bold } /* Keyword.Namespace */\n",
       "body .kp { color: #008000 } /* Keyword.Pseudo */\n",
       "body .kr { color: #008000; font-weight: bold } /* Keyword.Reserved */\n",
       "body .kt { color: #B00040 } /* Keyword.Type */\n",
       "body .m { color: #666666 } /* Literal.Number */\n",
       "body .s { color: #BA2121 } /* Literal.String */\n",
       "body .na { color: #7D9029 } /* Name.Attribute */\n",
       "body .nb { color: #008000 } /* Name.Builtin */\n",
       "body .nc { color: #0000FF; font-weight: bold } /* Name.Class */\n",
       "body .no { color: #880000 } /* Name.Constant */\n",
       "body .nd { color: #AA22FF } /* Name.Decorator */\n",
       "body .ni { color: #999999; font-weight: bold } /* Name.Entity */\n",
       "body .ne { color: #D2413A; font-weight: bold } /* Name.Exception */\n",
       "body .nf { color: #0000FF } /* Name.Function */\n",
       "body .nl { color: #A0A000 } /* Name.Label */\n",
       "body .nn { color: #0000FF; font-weight: bold } /* Name.Namespace */\n",
       "body .nt { color: #008000; font-weight: bold } /* Name.Tag */\n",
       "body .nv { color: #19177C } /* Name.Variable */\n",
       "body .ow { color: #AA22FF; font-weight: bold } /* Operator.Word */\n",
       "body .w { color: #bbbbbb } /* Text.Whitespace */\n",
       "body .mb { color: #666666 } /* Literal.Number.Bin */\n",
       "body .mf { color: #666666 } /* Literal.Number.Float */\n",
       "body .mh { color: #666666 } /* Literal.Number.Hex */\n",
       "body .mi { color: #666666 } /* Literal.Number.Integer */\n",
       "body .mo { color: #666666 } /* Literal.Number.Oct */\n",
       "body .sa { color: #BA2121 } /* Literal.String.Affix */\n",
       "body .sb { color: #BA2121 } /* Literal.String.Backtick */\n",
       "body .sc { color: #BA2121 } /* Literal.String.Char */\n",
       "body .dl { color: #BA2121 } /* Literal.String.Delimiter */\n",
       "body .sd { color: #BA2121; font-style: italic } /* Literal.String.Doc */\n",
       "body .s2 { color: #BA2121 } /* Literal.String.Double */\n",
       "body .se { color: #BB6622; font-weight: bold } /* Literal.String.Escape */\n",
       "body .sh { color: #BA2121 } /* Literal.String.Heredoc */\n",
       "body .si { color: #BB6688; font-weight: bold } /* Literal.String.Interpol */\n",
       "body .sx { color: #008000 } /* Literal.String.Other */\n",
       "body .sr { color: #BB6688 } /* Literal.String.Regex */\n",
       "body .s1 { color: #BA2121 } /* Literal.String.Single */\n",
       "body .ss { color: #19177C } /* Literal.String.Symbol */\n",
       "body .bp { color: #008000 } /* Name.Builtin.Pseudo */\n",
       "body .fm { color: #0000FF } /* Name.Function.Magic */\n",
       "body .vc { color: #19177C } /* Name.Variable.Class */\n",
       "body .vg { color: #19177C } /* Name.Variable.Global */\n",
       "body .vi { color: #19177C } /* Name.Variable.Instance */\n",
       "body .vm { color: #19177C } /* Name.Variable.Magic */\n",
       "body .il { color: #666666 } /* Literal.Number.Integer.Long */\n",
       "\n",
       "  </style>\n",
       "</head>\n",
       "<body>\n",
       "<h2></h2>\n",
       "\n",
       "<div class=\"highlight\"><pre><span></span><span class=\"k\">def</span> <span class=\"nf\">fol_fc_ask</span><span class=\"p\">(</span><span class=\"n\">KB</span><span class=\"p\">,</span> <span class=\"n\">alpha</span><span class=\"p\">):</span>\n",
       "    <span class=\"sd\">&quot;&quot;&quot;A simple forward-chaining algorithm. [Figure 9.3]&quot;&quot;&quot;</span>\n",
       "    <span class=\"c1\"># TODO: Improve efficiency</span>\n",
       "    <span class=\"n\">kb_consts</span> <span class=\"o\">=</span> <span class=\"nb\">list</span><span class=\"p\">({</span><span class=\"n\">c</span> <span class=\"k\">for</span> <span class=\"n\">clause</span> <span class=\"ow\">in</span> <span class=\"n\">KB</span><span class=\"o\">.</span><span class=\"n\">clauses</span> <span class=\"k\">for</span> <span class=\"n\">c</span> <span class=\"ow\">in</span> <span class=\"n\">constant_symbols</span><span class=\"p\">(</span><span class=\"n\">clause</span><span class=\"p\">)})</span>\n",
       "    <span class=\"k\">def</span> <span class=\"nf\">enum_subst</span><span class=\"p\">(</span><span class=\"n\">p</span><span class=\"p\">):</span>\n",
       "        <span class=\"n\">query_vars</span> <span class=\"o\">=</span> <span class=\"nb\">list</span><span class=\"p\">({</span><span class=\"n\">v</span> <span class=\"k\">for</span> <span class=\"n\">clause</span> <span class=\"ow\">in</span> <span class=\"n\">p</span> <span class=\"k\">for</span> <span class=\"n\">v</span> <span class=\"ow\">in</span> <span class=\"n\">variables</span><span class=\"p\">(</span><span class=\"n\">clause</span><span class=\"p\">)})</span>\n",
       "        <span class=\"k\">for</span> <span class=\"n\">assignment_list</span> <span class=\"ow\">in</span> <span class=\"n\">itertools</span><span class=\"o\">.</span><span class=\"n\">product</span><span class=\"p\">(</span><span class=\"n\">kb_consts</span><span class=\"p\">,</span> <span class=\"n\">repeat</span><span class=\"o\">=</span><span class=\"nb\">len</span><span class=\"p\">(</span><span class=\"n\">query_vars</span><span class=\"p\">)):</span>\n",
       "            <span class=\"n\">theta</span> <span class=\"o\">=</span> <span class=\"p\">{</span><span class=\"n\">x</span><span class=\"p\">:</span> <span class=\"n\">y</span> <span class=\"k\">for</span> <span class=\"n\">x</span><span class=\"p\">,</span> <span class=\"n\">y</span> <span class=\"ow\">in</span> <span class=\"nb\">zip</span><span class=\"p\">(</span><span class=\"n\">query_vars</span><span class=\"p\">,</span> <span class=\"n\">assignment_list</span><span class=\"p\">)}</span>\n",
       "            <span class=\"k\">yield</span> <span class=\"n\">theta</span>\n",
       "\n",
       "    <span class=\"c1\"># check if we can answer without new inferences</span>\n",
       "    <span class=\"k\">for</span> <span class=\"n\">q</span> <span class=\"ow\">in</span> <span class=\"n\">KB</span><span class=\"o\">.</span><span class=\"n\">clauses</span><span class=\"p\">:</span>\n",
       "        <span class=\"n\">phi</span> <span class=\"o\">=</span> <span class=\"n\">unify</span><span class=\"p\">(</span><span class=\"n\">q</span><span class=\"p\">,</span> <span class=\"n\">alpha</span><span class=\"p\">,</span> <span class=\"p\">{})</span>\n",
       "        <span class=\"k\">if</span> <span class=\"n\">phi</span> <span class=\"ow\">is</span> <span class=\"ow\">not</span> <span class=\"bp\">None</span><span class=\"p\">:</span>\n",
       "            <span class=\"k\">yield</span> <span class=\"n\">phi</span>\n",
       "\n",
       "    <span class=\"k\">while</span> <span class=\"bp\">True</span><span class=\"p\">:</span>\n",
       "        <span class=\"n\">new</span> <span class=\"o\">=</span> <span class=\"p\">[]</span>\n",
       "        <span class=\"k\">for</span> <span class=\"n\">rule</span> <span class=\"ow\">in</span> <span class=\"n\">KB</span><span class=\"o\">.</span><span class=\"n\">clauses</span><span class=\"p\">:</span>\n",
       "            <span class=\"n\">p</span><span class=\"p\">,</span> <span class=\"n\">q</span> <span class=\"o\">=</span> <span class=\"n\">parse_definite_clause</span><span class=\"p\">(</span><span class=\"n\">rule</span><span class=\"p\">)</span>\n",
       "            <span class=\"k\">for</span> <span class=\"n\">theta</span> <span class=\"ow\">in</span> <span class=\"n\">enum_subst</span><span class=\"p\">(</span><span class=\"n\">p</span><span class=\"p\">):</span>\n",
       "                <span class=\"k\">if</span> <span class=\"nb\">set</span><span class=\"p\">(</span><span class=\"n\">subst</span><span class=\"p\">(</span><span class=\"n\">theta</span><span class=\"p\">,</span> <span class=\"n\">p</span><span class=\"p\">))</span><span class=\"o\">.</span><span class=\"n\">issubset</span><span class=\"p\">(</span><span class=\"nb\">set</span><span class=\"p\">(</span><span class=\"n\">KB</span><span class=\"o\">.</span><span class=\"n\">clauses</span><span class=\"p\">)):</span>\n",
       "                    <span class=\"n\">q_</span> <span class=\"o\">=</span> <span class=\"n\">subst</span><span class=\"p\">(</span><span class=\"n\">theta</span><span class=\"p\">,</span> <span class=\"n\">q</span><span class=\"p\">)</span>\n",
       "                    <span class=\"k\">if</span> <span class=\"nb\">all</span><span class=\"p\">([</span><span class=\"n\">unify</span><span class=\"p\">(</span><span class=\"n\">x</span><span class=\"p\">,</span> <span class=\"n\">q_</span><span class=\"p\">,</span> <span class=\"p\">{})</span> <span class=\"ow\">is</span> <span class=\"bp\">None</span> <span class=\"k\">for</span> <span class=\"n\">x</span> <span class=\"ow\">in</span> <span class=\"n\">KB</span><span class=\"o\">.</span><span class=\"n\">clauses</span> <span class=\"o\">+</span> <span class=\"n\">new</span><span class=\"p\">]):</span>\n",
       "                        <span class=\"n\">new</span><span class=\"o\">.</span><span class=\"n\">append</span><span class=\"p\">(</span><span class=\"n\">q_</span><span class=\"p\">)</span>\n",
       "                        <span class=\"n\">phi</span> <span class=\"o\">=</span> <span class=\"n\">unify</span><span class=\"p\">(</span><span class=\"n\">q_</span><span class=\"p\">,</span> <span class=\"n\">alpha</span><span class=\"p\">,</span> <span class=\"p\">{})</span>\n",
       "                        <span class=\"k\">if</span> <span class=\"n\">phi</span> <span class=\"ow\">is</span> <span class=\"ow\">not</span> <span class=\"bp\">None</span><span class=\"p\">:</span>\n",
       "                            <span class=\"k\">yield</span> <span class=\"n\">phi</span>\n",
       "        <span class=\"k\">if</span> <span class=\"ow\">not</span> <span class=\"n\">new</span><span class=\"p\">:</span>\n",
       "            <span class=\"k\">break</span>\n",
       "        <span class=\"k\">for</span> <span class=\"n\">clause</span> <span class=\"ow\">in</span> <span class=\"n\">new</span><span class=\"p\">:</span>\n",
       "            <span class=\"n\">KB</span><span class=\"o\">.</span><span class=\"n\">tell</span><span class=\"p\">(</span><span class=\"n\">clause</span><span class=\"p\">)</span>\n",
       "    <span class=\"k\">return</span> <span class=\"bp\">None</span>\n",
       "</pre></div>\n",
       "</body>\n",
       "</html>\n"
      ],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "psource(fol_fc_ask)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "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."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 62,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "[{x: Nono}]\n"
     ]
    }
   ],
   "source": [
    "answer = fol_fc_ask(crime_kb, expr('Hostile(x)'))\n",
    "print(list(answer))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "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."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 63,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "[{x: Nono}, {x: JaJa}]\n"
     ]
    }
   ],
   "source": [
    "crime_kb.tell(expr('Enemy(JaJa, America)'))\n",
    "answer = fol_fc_ask(crime_kb, expr('Hostile(x)'))\n",
    "print(list(answer))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "<strong><em>Note</em>:</strong> `fol_fc_ask` makes changes to the `KB` by adding sentences to it."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Backward Chaining Algorithm\n",
    "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 <em>And/Or</em> search."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "#### OR\n",
    "The <em>OR</em> 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."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 64,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "%psource fol_bc_or"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "#### AND\n",
    "The <em>AND</em> corresponds to proving all the conjuncts in the `lhs`. We need to find a substitution which proves each <em>and</em> every clause in the list of conjuncts."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 65,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "%psource fol_bc_and"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "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."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 66,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "# Rebuild KB because running fol_fc_ask would add new facts to the KB\n",
    "crime_kb = FolKB(clauses)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 67,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "{v_5: x, x: Nono}"
      ]
     },
     "execution_count": 67,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "crime_kb.ask(expr('Hostile(x)'))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "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](#Unification)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Appendix: The Implementation of `|'==>'|`\n",
    "\n",
    "Consider the `Expr` formed by this syntax:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 68,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "(P ==> ~Q)"
      ]
     },
     "execution_count": 68,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "P |'==>'| ~Q"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "What is the funny `|'==>'|` syntax? The trick is that \"`|`\" is just the regular Python or-operator, and so is exactly equivalent to this: "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 69,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "(P ==> ~Q)"
      ]
     },
     "execution_count": 69,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "(P | '==>') | ~Q"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "In other words, there are two applications of or-operators. Here's the first one:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 70,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "PartialExpr('==>', P)"
      ]
     },
     "execution_count": 70,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "P | '==>'"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "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.\n",
    "\n",
    "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`:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 71,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "(P ==> ~Q)"
      ]
     },
     "execution_count": 71,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "partial = PartialExpr('==>', P) \n",
    "partial | ~Q"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "This  [trick](http://code.activestate.com/recipes/384122-infix-operators/) is due to [Ferdinand Jamitzky](http://code.activestate.com/recipes/users/98863/), with a modification by [C. G. Vedant](https://github.com/Chipe1),\n",
    "who suggested using a string inside the or-bars.\n",
    "\n",
    "## Appendix: The Implementation of `expr`\n",
    "\n",
    "How does `expr` parse a string into an `Expr`? It turns out there are two tricks (besides the Jamitzky/Vedant trick):\n",
    "\n",
    "1. We do a string substitution, replacing \"`==>`\" with \"`|'==>'|`\" (and likewise for other operators).\n",
    "2. We `eval` the resulting string in an environment in which every identifier\n",
    "is bound to a symbol with that identifier as the `op`.\n",
    "\n",
    "In other words,"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 72,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "(~(P & Q) ==> (~P | ~Q))"
      ]
     },
     "execution_count": 72,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "expr('~(P & Q)  ==>  (~P | ~Q)')"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "is equivalent to doing:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 73,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "(~(P & Q) ==> (~P | ~Q))"
      ]
     },
     "execution_count": 73,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "P, Q = symbols('P, Q')\n",
    "~(P & Q)  |'==>'|  (~P | ~Q)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "One thing to beware of: this puts `==>` at the same precedence level as `\"|\"`, which is not quite right. For example, we get this:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 74,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "(((P & Q) ==> P) | Q)"
      ]
     },
     "execution_count": 74,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "P & Q  |'==>'|  P | Q"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "which is probably not what we meant; when in doubt, put in extra parens:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 75,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "((P & Q) ==> (P | Q))"
      ]
     },
     "execution_count": 75,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "(P & Q)  |'==>'|  (P | Q)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Examples"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 76,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/html": [
       "\n",
       "<script type=\"text/javascript\" src=\"./js/canvas.js\"></script>\n",
       "<div>\n",
       "<canvas id=\"canvas_bc_ask\" width=\"800\" height=\"600\" style=\"background:rgba(158, 167, 184, 0.2);\" onclick='click_callback(this, event, \"canvas_bc_ask\")'></canvas>\n",
       "</div>\n",
       "\n",
       "<script> var canvas_bc_ask_canvas_object = new Canvas(\"canvas_bc_ask\");</script>\n"
      ],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/html": [
       "<script>\n",
       "canvas_bc_ask_canvas_object.clear();\n",
       "canvas_bc_ask_canvas_object.strokeWidth(3);\n",
       "canvas_bc_ask_canvas_object.stroke(0, 0, 0);\n",
       "canvas_bc_ask_canvas_object.font(\"12px Arial\");\n",
       "canvas_bc_ask_canvas_object.fill(200, 200, 200);\n",
       "canvas_bc_ask_canvas_object.rect(340, 85, 120, 30);\n",
       "canvas_bc_ask_canvas_object.line(340, 85, 460, 85);\n",
       "canvas_bc_ask_canvas_object.line(340, 85, 340, 115);\n",
       "canvas_bc_ask_canvas_object.line(460, 85, 460, 115);\n",
       "canvas_bc_ask_canvas_object.line(340, 115, 460, 115);\n",
       "canvas_bc_ask_canvas_object.fill(0, 0, 0);\n",
       "canvas_bc_ask_canvas_object.fill_text(\"Criminal(West)\", 348, 109);\n",
       "canvas_bc_ask_canvas_object.fill(200, 200, 200);\n",
       "canvas_bc_ask_canvas_object.rect(55, 255, 120, 30);\n",
       "canvas_bc_ask_canvas_object.line(55, 255, 175, 255);\n",
       "canvas_bc_ask_canvas_object.line(55, 255, 55, 285);\n",
       "canvas_bc_ask_canvas_object.line(175, 255, 175, 285);\n",
       "canvas_bc_ask_canvas_object.line(55, 285, 175, 285);\n",
       "canvas_bc_ask_canvas_object.fill(0, 0, 0);\n",
       "canvas_bc_ask_canvas_object.fill_text(\"American(West)\", 63, 279);\n",
       "canvas_bc_ask_canvas_object.fill(200, 200, 200);\n",
       "canvas_bc_ask_canvas_object.rect(245, 255, 120, 30);\n",
       "canvas_bc_ask_canvas_object.line(245, 255, 365, 255);\n",
       "canvas_bc_ask_canvas_object.line(245, 255, 245, 285);\n",
       "canvas_bc_ask_canvas_object.line(365, 255, 365, 285);\n",
       "canvas_bc_ask_canvas_object.line(245, 285, 365, 285);\n",
       "canvas_bc_ask_canvas_object.fill(0, 0, 0);\n",
       "canvas_bc_ask_canvas_object.fill_text(\"Weapon(M1)\", 253, 279);\n",
       "canvas_bc_ask_canvas_object.fill(200, 200, 200);\n",
       "canvas_bc_ask_canvas_object.rect(435, 255, 120, 30);\n",
       "canvas_bc_ask_canvas_object.line(435, 255, 555, 255);\n",
       "canvas_bc_ask_canvas_object.line(435, 255, 435, 285);\n",
       "canvas_bc_ask_canvas_object.line(555, 255, 555, 285);\n",
       "canvas_bc_ask_canvas_object.line(435, 285, 555, 285);\n",
       "canvas_bc_ask_canvas_object.fill(0, 0, 0);\n",
       "canvas_bc_ask_canvas_object.fill_text(\"Sells(West, M1, Nono)\", 443, 279);\n",
       "canvas_bc_ask_canvas_object.fill(200, 200, 200);\n",
       "canvas_bc_ask_canvas_object.rect(625, 255, 120, 30);\n",
       "canvas_bc_ask_canvas_object.line(625, 255, 745, 255);\n",
       "canvas_bc_ask_canvas_object.line(625, 255, 625, 285);\n",
       "canvas_bc_ask_canvas_object.line(745, 255, 745, 285);\n",
       "canvas_bc_ask_canvas_object.line(625, 285, 745, 285);\n",
       "canvas_bc_ask_canvas_object.fill(0, 0, 0);\n",
       "canvas_bc_ask_canvas_object.fill_text(\"Hostile(Nono)\", 633, 279);\n",
       "canvas_bc_ask_canvas_object.fill(200, 200, 200);\n",
       "canvas_bc_ask_canvas_object.rect(55, 425, 120, 30);\n",
       "canvas_bc_ask_canvas_object.line(55, 425, 175, 425);\n",
       "canvas_bc_ask_canvas_object.line(55, 425, 55, 455);\n",
       "canvas_bc_ask_canvas_object.line(175, 425, 175, 455);\n",
       "canvas_bc_ask_canvas_object.line(55, 455, 175, 455);\n",
       "canvas_bc_ask_canvas_object.fill(0, 0, 0);\n",
       "canvas_bc_ask_canvas_object.fill_text(\"Missile(M1)\", 63, 449);\n",
       "canvas_bc_ask_canvas_object.fill(200, 200, 200);\n",
       "canvas_bc_ask_canvas_object.rect(245, 425, 120, 30);\n",
       "canvas_bc_ask_canvas_object.line(245, 425, 365, 425);\n",
       "canvas_bc_ask_canvas_object.line(245, 425, 245, 455);\n",
       "canvas_bc_ask_canvas_object.line(365, 425, 365, 455);\n",
       "canvas_bc_ask_canvas_object.line(245, 455, 365, 455);\n",
       "canvas_bc_ask_canvas_object.fill(0, 0, 0);\n",
       "canvas_bc_ask_canvas_object.fill_text(\"Missile(M1)\", 253, 449);\n",
       "canvas_bc_ask_canvas_object.fill(200, 200, 200);\n",
       "canvas_bc_ask_canvas_object.rect(435, 425, 120, 30);\n",
       "canvas_bc_ask_canvas_object.line(435, 425, 555, 425);\n",
       "canvas_bc_ask_canvas_object.line(435, 425, 435, 455);\n",
       "canvas_bc_ask_canvas_object.line(555, 425, 555, 455);\n",
       "canvas_bc_ask_canvas_object.line(435, 455, 555, 455);\n",
       "canvas_bc_ask_canvas_object.fill(0, 0, 0);\n",
       "canvas_bc_ask_canvas_object.fill_text(\"Owns(Nono, M1)\", 443, 449);\n",
       "canvas_bc_ask_canvas_object.fill(200, 200, 200);\n",
       "canvas_bc_ask_canvas_object.rect(625, 425, 120, 30);\n",
       "canvas_bc_ask_canvas_object.line(625, 425, 745, 425);\n",
       "canvas_bc_ask_canvas_object.line(625, 425, 625, 455);\n",
       "canvas_bc_ask_canvas_object.line(745, 425, 745, 455);\n",
       "canvas_bc_ask_canvas_object.line(625, 455, 745, 455);\n",
       "canvas_bc_ask_canvas_object.fill(0, 0, 0);\n",
       "canvas_bc_ask_canvas_object.fill_text(\"Enemy(Nono, America)\", 633, 449);\n",
       "canvas_bc_ask_canvas_object.line(400, 115, 495, 255);\n",
       "canvas_bc_ask_canvas_object.line(305, 285, 115, 425);\n",
       "canvas_bc_ask_canvas_object.line(495, 285, 305, 425);\n",
       "canvas_bc_ask_canvas_object.line(685, 285, 685, 425);\n",
       "canvas_bc_ask_canvas_object.line(400, 115, 685, 255);\n",
       "canvas_bc_ask_canvas_object.line(400, 115, 305, 255);\n",
       "canvas_bc_ask_canvas_object.line(400, 115, 115, 255);\n",
       "canvas_bc_ask_canvas_object.line(495, 285, 495, 425);\n",
       "canvas_bc_ask_canvas_object.fill(255, 255, 255);\n",
       "canvas_bc_ask_canvas_object.rect(0, 540, 800, 60);\n",
       "canvas_bc_ask_canvas_object.strokeWidth(5);\n",
       "canvas_bc_ask_canvas_object.stroke(0, 0, 0);\n",
       "canvas_bc_ask_canvas_object.line(0, 540, 800, 540);\n",
       "canvas_bc_ask_canvas_object.font(\"22px Arial\");\n",
       "canvas_bc_ask_canvas_object.fill(0, 0, 0);\n",
       "canvas_bc_ask_canvas_object.fill_text(\"Click for text\", 20, 585);\n",
       "</script>"
      ],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "from notebook import Canvas_fol_bc_ask\n",
    "canvas_bc_ask = Canvas_fol_bc_ask('canvas_bc_ask', crime_kb, expr('Criminal(x)'))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "collapsed": true
   },
   "source": [
    "# Authors\n",
    "\n",
    "This notebook by [Chirag Vartak](https://github.com/chiragvartak) and [Peter Norvig](https://github.com/norvig).\n",
    "\n"
   ]
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "Python 3",
   "language": "python",
   "name": "python3"
  },
  "language_info": {
   "codemirror_mode": {
    "name": "ipython",
    "version": 3
   },
   "file_extension": ".py",
   "mimetype": "text/x-python",
   "name": "python",
   "nbconvert_exporter": "python",
   "pygments_lexer": "ipython3",
   "version": "3.6.4"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 1
}