diff --git a/README.md b/README.md index 79c50c822..c97db60f1 100644 --- a/README.md +++ b/README.md @@ -97,7 +97,7 @@ Here is a table of algorithms, the figure, name of the algorithm in the book and | 7.7 | Propositional Logic Sentence | `Expr` | [`utils.py`][utils] | Done | Included | | 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.14 | Convert to CNF | `to_cnf` | [`logic.py`][logic] | Done | Included | | 7.15 | PL-FC-Entails? | `pl_fc_resolution` | [`logic.py`][logic] | Done | | | 7.17 | DPLL-Satisfiable? | `dpll_satisfiable` | [`logic.py`][logic] | Done | | | 7.18 | WalkSAT | `WalkSAT` | [`logic.py`][logic] | Done | | diff --git a/logic.ipynb b/logic.ipynb index 6716e8515..726a8d69d 100644 --- a/logic.ipynb +++ b/logic.ipynb @@ -1006,15 +1006,447 @@ "unit clauses such as $P$ and $\\neg P$ which is a contradiction as both $P$ and $\\neg P$ can't be True at the same time." ] }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "There is one catch however, the algorithm that implements proof by resolution cannot handle complex sentences. \n", + "Implications and bi-implications have to be simplified into simpler clauses. \n", + "We already know that *every sentence of a propositional logic is logically equivalent to a conjunction of clauses*.\n", + "We will use this fact to our advantage and simplify the input sentence into the **conjunctive normal form** (CNF) which is a conjunction of disjunctions of literals.\n", + "For eg:\n", + "
\n", + "$$(A\\lor B)\\land (\\neg B\\lor C\\lor\\neg D)\\land (D\\lor\\neg E)$$\n", + "This is equivalent to the POS (Product of sums) form in digital electronics.\n", + "
\n", + "Here's an outline of how the conversion is done:\n", + "1. Convert bi-implications to implications\n", + "
\n", + "$\\alpha\\iff\\beta$ can be written as $(\\alpha\\implies\\beta)\\land(\\beta\\implies\\alpha)$\n", + "
\n", + "This also applies to compound sentences\n", + "
\n", + "$\\alpha\\iff(\\beta\\lor\\gamma)$ can be written as $(\\alpha\\implies(\\beta\\lor\\gamma))\\land((\\beta\\lor\\gamma)\\implies\\alpha)$\n", + "
\n", + "2. Convert implications to their logical equivalents\n", + "
\n", + "$\\alpha\\implies\\beta$ can be written as $\\neg\\alpha\\lor\\beta$\n", + "
\n", + "3. Move negation inwards\n", + "
\n", + "CNF requires atomic literals. Hence, negation cannot appear on a compound statement.\n", + "De Morgan's laws will be helpful here.\n", + "
\n", + "$\\neg(\\alpha\\land\\beta)\\equiv(\\neg\\alpha\\lor\\neg\\beta)$\n", + "
\n", + "$\\neg(\\alpha\\lor\\beta)\\equiv(\\neg\\alpha\\land\\neg\\beta)$\n", + "
\n", + "4. Distribute disjunction over conjunction\n", + "
\n", + "Disjunction and conjunction are distributive over each other.\n", + "Now that we only have conjunctions, disjunctions and negations in our expression, \n", + "we will distribute disjunctions over conjunctions wherever possible as this will give us a sentence which is a conjunction of simpler clauses, \n", + "which is what we wanted in the first place.\n", + "
\n", + "We need a term of the form\n", + "
\n", + "$(\\alpha_{1}\\lor\\alpha_{2}\\lor\\alpha_{3}...)\\land(\\beta_{1}\\lor\\beta_{2}\\lor\\beta_{3}...)\\land(\\gamma_{1}\\lor\\gamma_{2}\\lor\\gamma_{3}...)\\land...$\n", + "
\n", + "
\n", + "The `to_cnf` function executes this conversion using helper subroutines." + ] + }, { "cell_type": "code", - "execution_count": 24, + "execution_count": 29, + "metadata": {}, + "outputs": [ + { + "data": { + "text/html": [ + "\n", + "\n", + "\n", + "\n", + " \n", + " \n", + " \n", + "\n", + "\n", + "

\n", + "\n", + "
def to_cnf(s):\n",
+       "    """Convert a propositional logical sentence to conjunctive normal form.\n",
+       "    That is, to the form ((A | ~B | ...) & (B | C | ...) & ...) [p. 253]\n",
+       "    >>> to_cnf('~(B | C)')\n",
+       "    (~B & ~C)\n",
+       "    """\n",
+       "    s = expr(s)\n",
+       "    if isinstance(s, str):\n",
+       "        s = expr(s)\n",
+       "    s = eliminate_implications(s)  # Steps 1, 2 from p. 253\n",
+       "    s = move_not_inwards(s)  # Step 3\n",
+       "    return distribute_and_over_or(s)  # Step 4\n",
+       "
\n", + "\n", + "\n" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + } + ], + "source": [ + "psource(to_cnf)" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "`to_cnf` calls three subroutines.\n", + "
\n", + "`eliminate_implications` converts bi-implications and implications to their logical equivalents.\n", + "
\n", + "`move_not_inwards` removes negations from compound statements and moves them inwards using De Morgan's laws.\n", + "
\n", + "`distribute_and_over_or` distributes disjunctions over conjunctions.\n", + "
\n", + "Run the cells below for implementation details.\n" + ] + }, + { + "cell_type": "code", + "execution_count": 30, + "metadata": { + "collapsed": true + }, + "outputs": [], + "source": [ + "%psource eliminate_implications" + ] + }, + { + "cell_type": "code", + "execution_count": 31, + "metadata": { + "collapsed": true + }, + "outputs": [], + "source": [ + "%psource move_not_inwards" + ] + }, + { + "cell_type": "code", + "execution_count": 32, "metadata": { "collapsed": true }, "outputs": [], "source": [ - "%psource pl_resolution" + "%psource distribute_and_over_or" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Let's convert some sentences to see how it works\n" + ] + }, + { + "cell_type": "code", + "execution_count": 33, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "((A | ~B) & (B | ~A))" + ] + }, + "execution_count": 33, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "A, B, C, D = expr('A, B, C, D')\n", + "to_cnf(A |'<=>'| B)" + ] + }, + { + "cell_type": "code", + "execution_count": 34, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "((A | ~B | ~C) & (B | ~A) & (C | ~A))" + ] + }, + "execution_count": 34, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "to_cnf(A |'<=>'| (B & C))" + ] + }, + { + "cell_type": "code", + "execution_count": 35, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "(A & (C | B) & (D | B))" + ] + }, + "execution_count": 35, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "to_cnf(A & (B | (C & D)))" + ] + }, + { + "cell_type": "code", + "execution_count": 36, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "((B | ~A | C | ~D) & (A | ~A | C | ~D) & (B | ~B | C | ~D) & (A | ~B | C | ~D))" + ] + }, + "execution_count": 36, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "to_cnf((A |'<=>'| ~B) |'==>'| (C | ~D))" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Coming back to our resolution problem, we can see how the `to_cnf` function is utilized here" + ] + }, + { + "cell_type": "code", + "execution_count": 37, + "metadata": {}, + "outputs": [ + { + "data": { + "text/html": [ + "\n", + "\n", + "\n", + "\n", + " \n", + " \n", + " \n", + "\n", + "\n", + "

\n", + "\n", + "
def pl_resolution(KB, alpha):\n",
+       "    """Propositional-logic resolution: say if alpha follows from KB. [Figure 7.12]"""\n",
+       "    clauses = KB.clauses + conjuncts(to_cnf(~alpha))\n",
+       "    new = set()\n",
+       "    while True:\n",
+       "        n = len(clauses)\n",
+       "        pairs = [(clauses[i], clauses[j])\n",
+       "                 for i in range(n) for j in range(i+1, n)]\n",
+       "        for (ci, cj) in pairs:\n",
+       "            resolvents = pl_resolve(ci, cj)\n",
+       "            if False in resolvents:\n",
+       "                return True\n",
+       "            new = new.union(set(resolvents))\n",
+       "        if new.issubset(set(clauses)):\n",
+       "            return False\n",
+       "        for c in new:\n",
+       "            if c not in clauses:\n",
+       "                clauses.append(c)\n",
+       "
\n", + "\n", + "\n" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + } + ], + "source": [ + "psource(pl_resolution)" ] }, {