logic.ipynb 259 ko
Newer Older
jeff3456's avatar
jeff3456 a validé
  {
   "cell_type": "markdown",
jeff3456's avatar
jeff3456 a validé
   "metadata": {
    "collapsed": true
jeff3456's avatar
jeff3456 a validé
   },
   "source": [
    "# Logic"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "This Jupyter notebook acts as supporting material for topics covered in __Chapter 6 Logical Agents__, __Chapter 7 First-Order Logic__ and __Chapter 8 Inference in First-Order Logic__ of the book *[Artificial Intelligence: A Modern Approach](http://aima.cs.berkeley.edu)*. We make use the implementations in the [logic.py](https://github.com/aimacode/aima-python/blob/master/logic.py) module. See the [intro notebook](https://github.com/aimacode/aima-python/blob/master/intro.ipynb) for instructions.\n",
    "Let's first import everything from the `logic` module."
jeff3456's avatar
jeff3456 a validé
   ]
  },
Peter Norvig's avatar
Peter Norvig a validé
   "cell_type": "code",
   "execution_count": 1,
   "metadata": {},
Peter Norvig's avatar
Peter Norvig a validé
   "outputs": [],
    "from utils import *\n",
    "from logic import *\n",
    "from notebook import psource"
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## CONTENTS\n",
    "- Logical sentences\n",
    "    - Expr\n",
    "    - PropKB\n",
    "    - Knowledge-based agents\n",
    "    - Inference in propositional knowledge base\n",
    "        - Truth table enumeration\n",
    "        - Proof by resolution\n",
    "        - Forward and backward chaining\n",
    "        - DPLL\n",
    "        - WalkSAT\n",
    "        - SATPlan\n",
    "    - FolKB\n",
    "    - Inference in first order knowledge base\n",
    "        - Unification\n",
    "        - Forward chaining algorithm\n",
    "        - Backward chaining algorithm"
   ]
  },
   "cell_type": "markdown",
   "metadata": {
    "collapsed": true
   },
Peter Norvig's avatar
Peter Norvig a validé
    "## Logical Sentences"
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
Peter Norvig's avatar
Peter Norvig a validé
    "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": {},
Peter Norvig's avatar
Peter Norvig a validé
   "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": [
Peter Norvig's avatar
Peter Norvig a validé
    "(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": {},
Peter Norvig's avatar
Peter Norvig a validé
   "outputs": [
    {
     "data": {
      "text/plain": [
       "(P & ~Q)"
      ]
     },
     "execution_count": 4,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
Peter Norvig's avatar
Peter Norvig a validé
    "P & ~Q"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
Peter Norvig's avatar
Peter Norvig a validé
    "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:"
Peter Norvig's avatar
Peter Norvig a validé
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "metadata": {},
Peter Norvig's avatar
Peter Norvig a validé
   "outputs": [
    {
     "data": {
      "text/plain": [
       "'&'"
      ]
     },
     "execution_count": 5,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "sentence = P & ~Q\n",
Peter Norvig's avatar
Peter Norvig a validé
    "\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": [
Peter Norvig's avatar
Peter Norvig a validé
    "sentence.args"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
Peter Norvig's avatar
Peter Norvig a validé
       "'P'"
      ]
     },
     "execution_count": 7,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
Peter Norvig's avatar
Peter Norvig a validé
    "P.op"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "metadata": {},
Peter Norvig's avatar
Peter Norvig a validé
   "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": [
Peter Norvig's avatar
Peter Norvig a validé
       "'P'"
      ]
     },
     "execution_count": 9,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
Peter Norvig's avatar
Peter Norvig a validé
    "Pxy = P(x, y)\n",
    "\n",
    "Pxy.op"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 10,
   "metadata": {},
Peter Norvig's avatar
Peter Norvig a validé
     "data": {
      "text/plain": [
       "(x, y)"
      ]
     },
     "execution_count": 10,
     "metadata": {},
     "output_type": "execute_result"
Peter Norvig's avatar
Peter Norvig a validé
    "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": {},
Peter Norvig's avatar
Peter Norvig a validé
     "data": {
      "text/plain": [
       "(((3 * f(x, y)) + (P(y) / 2)) + 1)"
      ]
     },
     "execution_count": 11,
     "metadata": {},
     "output_type": "execute_result"
Peter Norvig's avatar
Peter Norvig a validé
    "3 * f(x, y) + P(y) / 2 + 1"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Operators for Constructing Logical Sentences\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",
    "| Operation                | Book | Python Infix Input | Python Output | Python `Expr` Input\n",
Peter Norvig's avatar
Peter Norvig a validé
    "|--------------------------|----------------------|-------------------------|---|---|\n",
    "| Negation                 | ¬ P      | `~P`                       | `~P` | `Expr('~', P)`\n",
    "| And                      | P ∧ 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",
Peter Norvig's avatar
Peter Norvig a validé
    "| 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",
    "Here's an example of defining a sentence with an implication arrow:"
Peter Norvig's avatar
Peter Norvig a validé
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 12,
   "metadata": {},
Peter Norvig's avatar
Peter Norvig a validé
   "outputs": [
    {
     "data": {
      "text/plain": [
       "(~(P & Q) ==> (~P | ~Q))"
Peter Norvig's avatar
Peter Norvig a validé
      ]
     },
     "execution_count": 12,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "~(P & Q)  |'==>'|  (~P | ~Q)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
Peter Norvig's avatar
Peter Norvig a validé
    "## `expr`: a Shortcut for Constructing Sentences\n",
    "If the `|'==>'|` notation looks ugly to you, you can use the function `expr` instead:"
Peter Norvig's avatar
Peter Norvig a validé
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 13,
   "metadata": {},
Peter Norvig's avatar
Peter Norvig a validé
   "outputs": [
    {
     "data": {
      "text/plain": [
       "(~(P & Q) ==> (~P | ~Q))"
Peter Norvig's avatar
Peter Norvig a validé
      ]
     },
     "execution_count": 13,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "expr('~(P & Q)  ==>  (~P | ~Q)')"
Peter Norvig's avatar
Peter Norvig a validé
   ]
  },
  {
   "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:"
Peter Norvig's avatar
Peter Norvig a validé
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 14,
   "metadata": {},
Peter Norvig's avatar
Peter Norvig a validé
   "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": [
C.G.Vedant's avatar
C.G.Vedant a validé
    "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."
Peter Norvig's avatar
Peter Norvig a validé
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Propositional Knowledge Bases: `PropKB`\n",
Peter Norvig's avatar
Peter Norvig a validé
    "The class `PropKB` can be used to represent a knowledge base of propositional logic sentences.\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",
Peter Norvig's avatar
Peter Norvig a validé
    "\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",
Peter Norvig's avatar
Peter Norvig a validé
    "* `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."
   ]
  },
C.G.Vedant's avatar
C.G.Vedant a validé
  {
   "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": {},
C.G.Vedant's avatar
C.G.Vedant a validé
   "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": {},
C.G.Vedant's avatar
C.G.Vedant a validé
   "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": {},
C.G.Vedant's avatar
C.G.Vedant a validé
   "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": {},
C.G.Vedant's avatar
C.G.Vedant a validé
   "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": {},
C.G.Vedant's avatar
C.G.Vedant a validé
   "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": [
    "## Knowledge based agents"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "A knowledge-based agent is a simple generic agent that maintains and handles a knowledge base.\n",
    "The knowledge base may initially contain some background knowledge.\n",
    "<br>\n",
    "The purpose of a KB agent is to provide a level of abstraction over knowledge-base manipulation and is to be used as a base class for agents that work on a knowledge base.\n",
    "<br>\n",
    "Given a percept, the KB agent adds the percept to its knowledge base, asks the knowledge base for the best action, and tells the knowledge base that it has infact taken that action.\n",
    "<br>\n",
    "Our implementation of `KB-Agent` is encapsulated in a class `KB_AgentProgram` which inherits from the `KB` class.\n",
    "<br>\n",
    "Let's have a look."
   ]
  },
  {
   "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\">KB_AgentProgram</span><span class=\"p\">(</span><span class=\"n\">KB</span><span class=\"p\">):</span>\n",
       "    <span class=\"sd\">&quot;&quot;&quot;A generic logical knowledge-based agent program. [Figure 7.1]&quot;&quot;&quot;</span>\n",
       "    <span class=\"n\">steps</span> <span class=\"o\">=</span> <span class=\"n\">itertools</span><span class=\"o\">.</span><span class=\"n\">count</span><span class=\"p\">()</span>\n",
       "\n",
       "    <span class=\"k\">def</span> <span class=\"nf\">program</span><span class=\"p\">(</span><span class=\"n\">percept</span><span class=\"p\">):</span>\n",
       "        <span class=\"n\">t</span> <span class=\"o\">=</span> <span class=\"nb\">next</span><span class=\"p\">(</span><span class=\"n\">steps</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\">make_percept_sentence</span><span class=\"p\">(</span><span class=\"n\">percept</span><span class=\"p\">,</span> <span class=\"n\">t</span><span class=\"p\">))</span>\n",
       "        <span class=\"n\">action</span> <span class=\"o\">=</span> <span class=\"n\">KB</span><span class=\"o\">.</span><span class=\"n\">ask</span><span class=\"p\">(</span><span class=\"n\">make_action_query</span><span class=\"p\">(</span><span class=\"n\">t</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\">make_action_sentence</span><span class=\"p\">(</span><span class=\"n\">action</span><span class=\"p\">,</span> <span class=\"n\">t</span><span class=\"p\">))</span>\n",
       "        <span class=\"k\">return</span> <span class=\"n\">action</span>\n",
       "\n",
       "    <span class=\"k\">def</span> <span class=\"nf\">make_percept_sentence</span><span class=\"p\">(</span><span class=\"n\">percept</span><span class=\"p\">,</span> <span class=\"n\">t</span><span class=\"p\">):</span>\n",
       "        <span class=\"k\">return</span> <span class=\"n\">Expr</span><span class=\"p\">(</span><span class=\"s2\">&quot;Percept&quot;</span><span class=\"p\">)(</span><span class=\"n\">percept</span><span class=\"p\">,</span> <span class=\"n\">t</span><span class=\"p\">)</span>\n",
       "\n",
       "    <span class=\"k\">def</span> <span class=\"nf\">make_action_query</span><span class=\"p\">(</span><span class=\"n\">t</span><span class=\"p\">):</span>\n",
       "        <span class=\"k\">return</span> <span class=\"n\">expr</span><span class=\"p\">(</span><span class=\"s2\">&quot;ShouldDo(action, {})&quot;</span><span class=\"o\">.</span><span class=\"n\">format</span><span class=\"p\">(</span><span class=\"n\">t</span><span class=\"p\">))</span>\n",
       "\n",
       "    <span class=\"k\">def</span> <span class=\"nf\">make_action_sentence</span><span class=\"p\">(</span><span class=\"n\">action</span><span class=\"p\">,</span> <span class=\"n\">t</span><span class=\"p\">):</span>\n",
       "        <span class=\"k\">return</span> <span class=\"n\">Expr</span><span class=\"p\">(</span><span class=\"s2\">&quot;Did&quot;</span><span class=\"p\">)(</span><span class=\"n\">action</span><span class=\"p\">[</span><span class=\"n\">expr</span><span class=\"p\">(</span><span class=\"s1\">&#39;action&#39;</span><span class=\"p\">)],</span> <span class=\"n\">t</span><span class=\"p\">)</span>\n",
       "\n",
       "    <span class=\"k\">return</span> <span class=\"n\">program</span>\n",
       "</pre></div>\n",
       "</body>\n",
       "</html>\n"
      ],
      "text/plain": [
       "<IPython.core.display.HTML object>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "psource(KB_AgentProgram)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "The helper functions `make_percept_sentence`, `make_action_query` and `make_action_sentence` are all aptly named and as expected,\n",
    "`make_percept_sentence` makes first-order logic sentences about percepts we want our agent to receive,\n",
    "`make_action_query` asks the underlying `KB` about the action that should be taken and\n",
    "`make_action_sentence` tells the underlying `KB` about the action it has just taken."
   ]
  },
C.G.Vedant's avatar
C.G.Vedant a validé
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Inference in Propositional Knowledge Base\n",
C.G.Vedant's avatar
C.G.Vedant a validé
    "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": 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_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": 23,
   "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": [