diff --git a/README.md b/README.md index d23cc6851..4142c4853 100644 --- a/README.md +++ b/README.md @@ -95,7 +95,7 @@ Here is a table of algorithms, the figure, name of the algorithm in the book and | 7 | KB | `KB` | [`logic.py`][logic] | Done | Included | | 7.1 | KB-Agent | `KB_Agent` | [`logic.py`][logic] | Done | | | 7.7 | Propositional Logic Sentence | `Expr` | [`utils.py`][utils] | Done | Included | -| 7.10 | TT-Entails | `tt_entails` | [`logic.py`][logic] | Done | | +| 7.10 | TT-Entails | `tt_entails` | [`logic.py`][logic] | Done | Included | | 7.12 | PL-Resolution | `pl_resolution` | [`logic.py`][logic] | Done | Included | | 7.14 | Convert to CNF | `to_cnf` | [`logic.py`][logic] | Done | | | 7.15 | PL-FC-Entails? | `pl_fc_resolution` | [`logic.py`][logic] | Done | | diff --git a/logic.ipynb b/logic.ipynb index 4ac164861..6716e8515 100644 --- a/logic.ipynb +++ b/logic.ipynb @@ -29,7 +29,8 @@ "outputs": [], "source": [ "from utils import *\n", - "from logic import *" + "from logic import *\n", + "from notebook import psource" ] }, { @@ -553,19 +554,394 @@ { "cell_type": "code", "execution_count": 21, - "metadata": { - "collapsed": true - }, - "outputs": [], + "metadata": {}, + "outputs": [ + { + "data": { + "text/html": [ + "\n", + "\n", + "\n", + "\n", + " \n", + " \n", + " \n", + "\n", + "\n", + "

\n", + "\n", + "
def tt_check_all(kb, alpha, symbols, model):\n",
+       "    """Auxiliary routine to implement tt_entails."""\n",
+       "    if not symbols:\n",
+       "        if pl_true(kb, model):\n",
+       "            result = pl_true(alpha, model)\n",
+       "            assert result in (True, False)\n",
+       "            return result\n",
+       "        else:\n",
+       "            return True\n",
+       "    else:\n",
+       "        P, rest = symbols[0], symbols[1:]\n",
+       "        return (tt_check_all(kb, alpha, rest, extend(model, P, True)) and\n",
+       "                tt_check_all(kb, alpha, rest, extend(model, P, False)))\n",
+       "
\n", + "\n", + "\n" + ], + "text/plain": [ + "" + ] + }, + "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", + "
\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", + "
\n", + "`result = pl_true(alpha, model)`.\n", + "
\n", + "
\n", + "In short, `tt_check_all` evaluates this logical expression for each `model`\n", + "
\n", + "`pl_true(kb, model) => pl_true(alpha, model)`\n", + "
\n", + "which is logically equivalent to\n", + "
\n", + "`pl_true(kb, model) & ~pl_true(alpha, model)` \n", + "
\n", + "that is, the knowledge base and the negation of the query are logically inconsistent.\n", + "
\n", + "
\n", + "`tt_entails()` just extracts the symbols from the query and calls `tt_check_all()` with the proper parameters.\n" + ] + }, + { + "cell_type": "code", + "execution_count": 22, + "metadata": {}, + "outputs": [ + { + "data": { + "text/html": [ + "\n", + "\n", + "\n", + "\n", + " \n", + " \n", + " \n", + "\n", + "\n", + "

\n", + "\n", + "
def tt_entails(kb, alpha):\n",
+       "    """Does kb entail the sentence alpha? Use truth tables. For propositional\n",
+       "    kb's and sentences. [Figure 7.10]. Note that the 'kb' should be an\n",
+       "    Expr which is a conjunction of clauses.\n",
+       "    >>> tt_entails(expr('P & Q'), expr('Q'))\n",
+       "    True\n",
+       "    """\n",
+       "    assert not variables(alpha)\n",
+       "    symbols = list(prop_symbols(kb & alpha))\n",
+       "    return tt_check_all(kb, alpha, symbols, {})\n",
+       "
\n", + "\n", + "\n" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + } + ], + "source": [ + "psource(tt_entails)" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Keep in mind that for two symbols P and Q, P => Q is false only when P is `True` and Q is `False`.\n", + "Example usage of `tt_entails()`:" + ] + }, + { + "cell_type": "code", + "execution_count": 23, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "True" + ] + }, + "execution_count": 23, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "tt_entails(P & Q, Q)" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "P & Q is True only when both P and Q are True. Hence, (P & Q) => Q is True" + ] + }, + { + "cell_type": "code", + "execution_count": 24, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "False" + ] + }, + "execution_count": 24, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "tt_entails(P | Q, Q)" + ] + }, + { + "cell_type": "code", + "execution_count": 25, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "False" + ] + }, + "execution_count": 25, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "tt_entails(P | Q, P)" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "If we know that P | Q is true, we cannot infer the truth values of P and Q. \n", + "Hence (P | Q) => Q is False and so is (P | Q) => P." + ] + }, + { + "cell_type": "code", + "execution_count": 26, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "True" + ] + }, + "execution_count": 26, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "(A, B, C, D, E, F, G) = symbols('A, B, C, D, E, F, G')\n", + "tt_entails(A & (B | C) & D & E & ~(F | G), A & D & E & ~F & ~G)" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, "source": [ - "%psource tt_check_all" + "We can see that for the KB to be true, A, D, E have to be True and F and G have to be False.\n", + "Nothing can be said about B or C." ] }, { "cell_type": "markdown", "metadata": {}, "source": [ - "Note that `tt_entails()` takes an `Expr` which is a conjunction of clauses as the input instead of the `KB` itself. You can use the `ask_if_true()` method of `PropKB` which does all the required conversions. Let's check what `wumpus_kb` tells us about $P_{1, 1}$." + "Coming back to our problem, note that `tt_entails()` takes an `Expr` which is a conjunction of clauses as the input instead of the `KB` itself. \n", + "You can use the `ask_if_true()` method of `PropKB` which does all the required conversions. \n", + "Let's check what `wumpus_kb` tells us about $P_{1, 1}$." ] }, {