InferencePropLogic.ipynb

{
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Inference in a Propositional Knowledge Base"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "This Jupyter notebook demonstrates how to create a knowledge base for propositional logic and how to apply different inference algorithms to ask questions to the knowledge base."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Import modules:"
   ]
  },
  {
   "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": {},
   "source": [
    "## Wumpus World Knowledge Base"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "We first construct the knowledge base for the Wumpus World example from the lecture. The proposition symbols are:\n",
    "\n",
    "<br/>\n",
    "$P_{y, x}$ is true if there is a pit at position [y,x].<br/>\n",
    "$B_{y, x}$ is true if the agent senses breeze at position [y,x].<br/>\n",
    "\n",
    "We create all required proposition symbols with the `symbols` function:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "metadata": {},
   "outputs": [],
   "source": [
    "(P11,P12,P13,P21,P22,P31,B11,B12,B21) = symbols('P11, P12, P13, P21, P22, P31, B11, B12, B21')"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Next, we create an empty propositional knowledge base by calling the constructor of the class `PropKB`:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "metadata": {},
   "outputs": [],
   "source": [
    "wumpus_kb = PropKB()"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Now we can add all the knowledge we have about the Wumpus World environment to our knowledge base:\n",
    "\n",
    "There is no pit in `[1,1]`."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "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": 5,
   "metadata": {},
   "outputs": [],
   "source": [
    "wumpus_kb.tell(B11 | '<=>' | ((P12 | P21)))\n",
    "wumpus_kb.tell(B21 | '<=>' | ((P11 | P22 | P31)))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Finally, we include the breeze percepts for the first two squares:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "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 knowledge base by accessing its `clauses` property:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "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": 7,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "wumpus_kb.clauses"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "We see that some equivalences automatically got converted into two implications which afterwards got converted to Conjunctive Normal Form (CNF)."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Inference by Enumeration\n",
    "Given our knowledge base descibing the Wumpus World environment we now want to infere if the adjacent squares are safe. To solve this problem, we can use logical inference. The inference algorithm that is considered first is *Truth Table Enumeration*. To deside if a sentence $\\alpha$ is entailed by the knowledge base, *Truth Table Enumeration* enumerates all models and checks if $\\alpha$ is true for all models where the knowledge base is true. The algorithm is implemented in the function `tt_entails`:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "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",
       "generated by Pygments <http://pygments.org>\n",
       "Copyright 2006-2019 by the Pygments team.\n",
       "Licensed under the BSD license, see LICENSE for details.\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",
       "/*\n",
       "generated by Pygments <http://pygments.org>\n",
       "Copyright 2006-2019 by the Pygments team.\n",
       "Licensed under the BSD license, see LICENSE for details.\n",
       "*/\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;</span>\n",
       "<span class=\"sd\">    [Figure 7.10]</span>\n",
       "<span class=\"sd\">    Does kb entail the sentence alpha? Use truth tables. For propositional</span>\n",
       "<span class=\"sd\">    kb&#39;s and sentences. Note that the &#39;kb&#39; should be an Expr which is a</span>\n",
       "<span class=\"sd\">    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": [
    "Internally, the function `tt_entails` calls the function `tt_check_all` to check if the sentence $\\alpha$ and the knowledge base are true for a certain model:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 9,
   "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",
       "generated by Pygments <http://pygments.org>\n",
       "Copyright 2006-2019 by the Pygments team.\n",
       "Licensed under the BSD license, see LICENSE for details.\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",
       "/*\n",
       "generated by Pygments <http://pygments.org>\n",
       "Copyright 2006-2019 by the Pygments team.\n",
       "Licensed under the BSD license, see LICENSE for details.\n",
       "*/\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": [
    "Before we apply *Truth Table Enumeration* to our Wumpus World knowledge base we demonstrate the usage of the function `tt_entails` on some simple examples. Given two proposition symbols $P$ and $Q$, let us consider the knowledge base $KB = P \\wedge Q$ and the sentence $\\alpha = Q$. Since $P \\wedge Q$ can only become true if $Q$ is true, the knowledge base obviously entails the sentence $\\alpha$:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 10,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "execution_count": 10,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "(P,Q) = symbols('P, Q')\n",
    "tt_entails(P & Q, Q)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "If we instead consider the knowledge base $KB = P \\vee Q$, the sentence $\\alpha$ is not entailed by the knowledge base:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 11,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "False"
      ]
     },
     "execution_count": 11,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "tt_entails(P | Q, Q)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Now let's come back to our Wumpus World problem. The function `tt_entails()` takes an object of the class `Expr` which is a conjunction of clauses as the input instead of the `KB` itself. Instead of manually converting our knowledge base we can use the `ask_if_true` method of the `PropKB` class which does all the required conversions automatically. Let's check if there is a pit in the square [1,2]:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 12,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "execution_count": 12,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "wumpus_kb.ask_if_true(~P12)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Proof by Resolution\n"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "One alternative to the computational expensive *Truth Table Enumeration* is to proof the entailment using resolution. The algorithm that implements proof by resolution requires a knowledge base in Conjunctive Normal Form (CNF). We can apply the function `to_cnf` to convert logical sentences to CNF:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 13,
   "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",
       "generated by Pygments <http://pygments.org>\n",
       "Copyright 2006-2019 by the Pygments team.\n",
       "Licensed under the BSD license, see LICENSE for details.\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",
       "/*\n",
       "generated by Pygments <http://pygments.org>\n",
       "Copyright 2006-2019 by the Pygments team.\n",
       "Licensed under the BSD license, see LICENSE for details.\n",
       "*/\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;</span>\n",
       "<span class=\"sd\">    [Page 253]</span>\n",
       "<span class=\"sd\">    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; ...)</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": [
    "Here some examples that demsonstrate the automated conversion to CNF:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 14,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "((A | ~B) & (B | ~A))"
      ]
     },
     "execution_count": 14,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "(A,B,C,D) = symbols('A, B, C, D')\n",
    "to_cnf(A |'<=>'| B)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 15,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "((B | ~A | C | ~D) & (A | ~A | C | ~D) & (B | ~B | C | ~D) & (A | ~B | C | ~D))"
      ]
     },
     "execution_count": 15,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "to_cnf((A |'<=>'| ~B) |'==>'| (C | ~D))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "The resolution algorithm, which is implemented by the function `pl_resolution`, internally utilizes the function `to_cnf` to convert the knowledge base to CNF:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 16,
   "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",
       "generated by Pygments <http://pygments.org>\n",
       "Copyright 2006-2019 by the Pygments team.\n",
       "Licensed under the BSD license, see LICENSE for details.\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",
       "/*\n",
       "generated by Pygments <http://pygments.org>\n",
       "Copyright 2006-2019 by the Pygments team.\n",
       "Licensed under the BSD license, see LICENSE for details.\n",
       "*/\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;</span>\n",
       "<span class=\"sd\">    [Figure 7.12]</span>\n",
       "<span class=\"sd\">    Propositional-logic resolution: say if alpha follows from KB.</span>\n",
       "<span class=\"sd\">    &gt;&gt;&gt; pl_resolution(horn_clauses_KB, A)</span>\n",
       "<span class=\"sd\">    True</span>\n",
       "<span class=\"sd\">    &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": "markdown",
   "metadata": {},
   "source": [
    "Let's come back to our Wumpus World example. As done in the lecture slides, we first add some additional facts to our knowledge base:\n",
    "\n",
    "There is no breeze in square [1,2]:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 17,
   "metadata": {},
   "outputs": [],
   "source": [
    "wumpus_kb.tell(~B12)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "A square is breezy if and only if there is a pit in a neighboring square:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 18,
   "metadata": {},
   "outputs": [],
   "source": [
    "wumpus_kb.tell(B12 | '<=>' | ((P11 | P22 | P13)))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Now we apply the resolution algorithm to check if there is a pit in the square [3,1]:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 19,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "execution_count": 19,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "pl_resolution(wumpus_kb, P31)"
   ]
  }
 ],
 "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.9"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 1
}