diff --git a/logic.ipynb b/logic.ipynb index 0cd6cbc1f..92b8f51ed 100644 --- a/logic.ipynb +++ b/logic.ipynb @@ -946,7 +946,7 @@ }, { "cell_type": "code", - "execution_count": 22, + "execution_count": 27, "metadata": {}, "outputs": [ { @@ -955,7 +955,7 @@ "(True, False)" ] }, - "execution_count": 22, + "execution_count": 27, "metadata": {}, "output_type": "execute_result" } @@ -973,7 +973,7 @@ }, { "cell_type": "code", - "execution_count": 23, + "execution_count": 28, "metadata": {}, "outputs": [ { @@ -982,7 +982,7 @@ "(False, False)" ] }, - "execution_count": 23, + "execution_count": 28, "metadata": {}, "output_type": "execute_result" } @@ -1438,55 +1438,520 @@ "\n" ], "text/plain": [ - "" + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + } + ], + "source": [ + "psource(pl_resolution)" + ] + }, + { + "cell_type": "code", + "execution_count": 38, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "(True, False)" + ] + }, + "execution_count": 38, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "pl_resolution(wumpus_kb, ~P11), pl_resolution(wumpus_kb, P11)" + ] + }, + { + "cell_type": "code", + "execution_count": 39, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "(False, False)" + ] + }, + "execution_count": 39, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "pl_resolution(wumpus_kb, ~P22), pl_resolution(wumpus_kb, P22)" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "### Forward and backward chaining\n", + "Previously, we said we will look at two algorithms to check if a sentence is entailed by the `KB`, \n", + "but here's a third one. \n", + "The difference here is that our goal now is to determine if a knowledge base of definite clauses entails a single proposition symbol *q* - the query.\n", + "There is a catch however, the knowledge base can only contain **Horn clauses**.\n", + "
\n", + "#### Horn Clauses\n", + "Horn clauses can be defined as a *disjunction* of *literals* with **at most** one positive literal. \n", + "
\n", + "A Horn clause with exactly one positive literal is called a *definite clause*.\n", + "
\n", + "A Horn clause might look like \n", + "
\n", + "$\\neg a\\lor\\neg b\\lor\\neg c\\lor\\neg d... \\lor z$\n", + "
\n", + "This, coincidentally, is also a definite clause.\n", + "
\n", + "Using De Morgan's laws, the example above can be simplified to \n", + "
\n", + "$a\\land b\\land c\\land d ... \\implies z$\n", + "
\n", + "This seems like a logical representation of how humans process known data and facts. \n", + "Assuming percepts `a`, `b`, `c`, `d` ... to be true simultaneously, we can infer `z` to also be true at that point in time. \n", + "There are some interesting aspects of Horn clauses that make algorithmic inference or *resolution* easier.\n", + "- Definite clauses can be written as implications:\n", + "
\n", + "The most important simplification a definite clause provides is that it can be written as an implication.\n", + "The premise (or the knowledge that leads to the implication) is a conjunction of positive literals.\n", + "The conclusion (the implied statement) is also a positive literal.\n", + "The sentence thus becomes easier to understand.\n", + "The premise and the conclusion are conventionally called the *body* and the *head* respectively.\n", + "A single positive literal is called a *fact*.\n", + "- Forward chaining and backward chaining can be used for inference from Horn clauses:\n", + "
\n", + "Forward chaining is semantically identical to `AND-OR-Graph-Search` from the chapter on search algorithms.\n", + "Implementational details will be explained shortly.\n", + "- Deciding entailment with Horn clauses is linear in size of the knowledge base:\n", + "
\n", + "Surprisingly, the forward and backward chaining algorithms traverse each element of the knowledge base at most once, greatly simplifying the problem.\n", + "
\n", + "
\n", + "The function `pl_fc_entails` implements forward chaining to see if a knowledge base `KB` entails a symbol `q`.\n", + "
\n", + "Before we proceed further, note that `pl_fc_entails` doesn't use an ordinary `KB` instance. \n", + "The knowledge base here is an instance of the `PropDefiniteKB` class, derived from the `PropKB` class, \n", + "but modified to store definite clauses.\n", + "
\n", + "The main point of difference arises in the inclusion of a helper method to `PropDefiniteKB` that returns a list of clauses in KB that have a given symbol `p` in their premise." + ] + }, + { + "cell_type": "code", + "execution_count": 40, + "metadata": {}, + "outputs": [ + { + "data": { + "text/html": [ + "\n", + "\n", + "\n", + "\n", + " \n", + " \n", + " \n", + "\n", + "\n", + "

\n", + "\n", + "
    def clauses_with_premise(self, p):\n",
+       "        """Return a list of the clauses in KB that have p in their premise.\n",
+       "        This could be cached away for O(1) speed, but we'll recompute it."""\n",
+       "        return [c for c in self.clauses\n",
+       "                if c.op == '==>' and p in conjuncts(c.args[0])]\n",
+       "
\n", + "\n", + "\n" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + } + ], + "source": [ + "psource(PropDefiniteKB.clauses_with_premise)" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Let's now have a look at the `pl_fc_entails` algorithm." + ] + }, + { + "cell_type": "code", + "execution_count": 41, + "metadata": {}, + "outputs": [ + { + "data": { + "text/html": [ + "\n", + "\n", + "\n", + "\n", + " \n", + " \n", + " \n", + "\n", + "\n", + "

\n", + "\n", + "
def pl_fc_entails(KB, q):\n",
+       "    """Use forward chaining to see if a PropDefiniteKB entails symbol q.\n",
+       "    [Figure 7.15]\n",
+       "    >>> pl_fc_entails(horn_clauses_KB, expr('Q'))\n",
+       "    True\n",
+       "    """\n",
+       "    count = {c: len(conjuncts(c.args[0]))\n",
+       "             for c in KB.clauses\n",
+       "             if c.op == '==>'}\n",
+       "    inferred = defaultdict(bool)\n",
+       "    agenda = [s for s in KB.clauses if is_prop_symbol(s.op)]\n",
+       "    while agenda:\n",
+       "        p = agenda.pop()\n",
+       "        if p == q:\n",
+       "            return True\n",
+       "        if not inferred[p]:\n",
+       "            inferred[p] = True\n",
+       "            for c in KB.clauses_with_premise(p):\n",
+       "                count[c] -= 1\n",
+       "                if count[c] == 0:\n",
+       "                    agenda.append(c.args[1])\n",
+       "    return False\n",
+       "
\n", + "\n", + "\n" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + } + ], + "source": [ + "psource(pl_fc_entails)" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "The function accepts a knowledge base `KB` (an instance of `PropDefiniteKB`) and a query `q` as inputs.\n", + "
\n", + "
\n", + "`count` initially stores the number of symbols in the premise of each sentence in the knowledge base.\n", + "
\n", + "The `conjuncts` helper function separates a given sentence at conjunctions.\n", + "
\n", + "`inferred` is initialized as a *boolean* defaultdict. \n", + "This will be used later to check if we have inferred all premises of each clause of the agenda.\n", + "
\n", + "`agenda` initially stores a list of clauses that the knowledge base knows to be true.\n", + "The `is_prop_symbol` helper function checks if the given symbol is a valid propositional logic symbol.\n", + "
\n", + "
\n", + "We now iterate through `agenda`, popping a symbol `p` on each iteration.\n", + "If the query `q` is the same as `p`, we know that entailment holds.\n", + "
\n", + "The agenda is processed, reducing `count` by one for each implication with a premise `p`.\n", + "A conclusion is added to the agenda when `count` reaches zero. This means we know all the premises of that particular implication to be true.\n", + "
\n", + "`clauses_with_premise` is a helpful method of the `PropKB` class.\n", + "It returns a list of clauses in the knowledge base that have `p` in their premise.\n", + "
\n", + "
\n", + "Now that we have an idea of how this function works, let's see a few examples of its usage, but we first need to define our knowledge base. We assume we know the following clauses to be true." + ] + }, + { + "cell_type": "code", + "execution_count": 42, + "metadata": { + "collapsed": true + }, + "outputs": [], + "source": [ + "clauses = ['(B & F)==>E', \n", + " '(A & E & F)==>G', \n", + " '(B & C)==>F', \n", + " '(A & B)==>D', \n", + " '(E & F)==>H', \n", + " '(H & I)==>J',\n", + " 'A', \n", + " 'B', \n", + " 'C']" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "We will now `tell` this information to our knowledge base." + ] + }, + { + "cell_type": "code", + "execution_count": 43, + "metadata": { + "collapsed": true + }, + "outputs": [], + "source": [ + "definite_clauses_KB = PropDefiniteKB()\n", + "for clause in clauses:\n", + " definite_clauses_KB.tell(expr(clause))" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "We can now check if our knowledge base entails the following queries." + ] + }, + { + "cell_type": "code", + "execution_count": 44, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "True" ] }, + "execution_count": 44, "metadata": {}, - "output_type": "display_data" + "output_type": "execute_result" } ], "source": [ - "psource(pl_resolution)" + "pl_fc_entails(definite_clauses_KB, expr('G'))" ] }, { "cell_type": "code", - "execution_count": 25, + "execution_count": 45, "metadata": {}, "outputs": [ { "data": { "text/plain": [ - "(True, False)" + "True" ] }, - "execution_count": 25, + "execution_count": 45, "metadata": {}, "output_type": "execute_result" } ], "source": [ - "pl_resolution(wumpus_kb, ~P11), pl_resolution(wumpus_kb, P11)" + "pl_fc_entails(definite_clauses_KB, expr('H'))" ] }, { "cell_type": "code", - "execution_count": 26, + "execution_count": 46, "metadata": {}, "outputs": [ { "data": { "text/plain": [ - "(False, False)" + "False" ] }, - "execution_count": 26, + "execution_count": 46, "metadata": {}, "output_type": "execute_result" } ], "source": [ - "pl_resolution(wumpus_kb, ~P22), pl_resolution(wumpus_kb, P22)" + "pl_fc_entails(definite_clauses_KB, expr('I'))" + ] + }, + { + "cell_type": "code", + "execution_count": 47, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "False" + ] + }, + "execution_count": 47, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "pl_fc_entails(definite_clauses_KB, expr('J'))" ] }, { @@ -2357,7 +2822,7 @@ }, { "cell_type": "code", - "execution_count": 27, + "execution_count": 48, "metadata": { "collapsed": true }, @@ -2386,7 +2851,7 @@ }, { "cell_type": "code", - "execution_count": 28, + "execution_count": 49, "metadata": { "collapsed": true }, @@ -2407,7 +2872,7 @@ }, { "cell_type": "code", - "execution_count": 29, + "execution_count": 50, "metadata": { "collapsed": true }, @@ -2428,7 +2893,7 @@ }, { "cell_type": "code", - "execution_count": 30, + "execution_count": 51, "metadata": { "collapsed": true }, @@ -2452,7 +2917,7 @@ }, { "cell_type": "code", - "execution_count": 31, + "execution_count": 52, "metadata": { "collapsed": true }, @@ -2473,7 +2938,7 @@ }, { "cell_type": "code", - "execution_count": 32, + "execution_count": 53, "metadata": { "collapsed": true }, @@ -2493,7 +2958,7 @@ }, { "cell_type": "code", - "execution_count": 33, + "execution_count": 54, "metadata": { "collapsed": true }, @@ -2512,7 +2977,7 @@ }, { "cell_type": "code", - "execution_count": 34, + "execution_count": 55, "metadata": { "collapsed": true }, @@ -2539,7 +3004,7 @@ }, { "cell_type": "code", - "execution_count": 35, + "execution_count": 56, "metadata": {}, "outputs": [ { @@ -2548,7 +3013,7 @@ "{x: 3}" ] }, - "execution_count": 35, + "execution_count": 56, "metadata": {}, "output_type": "execute_result" } @@ -2559,7 +3024,7 @@ }, { "cell_type": "code", - "execution_count": 36, + "execution_count": 57, "metadata": {}, "outputs": [ { @@ -2568,7 +3033,7 @@ "{x: B}" ] }, - "execution_count": 36, + "execution_count": 57, "metadata": {}, "output_type": "execute_result" } @@ -2579,7 +3044,7 @@ }, { "cell_type": "code", - "execution_count": 37, + "execution_count": 58, "metadata": {}, "outputs": [ { @@ -2588,7 +3053,7 @@ "{x: Bella, y: Dobby}" ] }, - "execution_count": 37, + "execution_count": 58, "metadata": {}, "output_type": "execute_result" } @@ -2606,7 +3071,7 @@ }, { "cell_type": "code", - "execution_count": 38, + "execution_count": 59, "metadata": {}, "outputs": [ { @@ -2630,7 +3095,7 @@ }, { "cell_type": "code", - "execution_count": 39, + "execution_count": 60, "metadata": {}, "outputs": [ { @@ -2657,13 +3122,145 @@ }, { "cell_type": "code", - "execution_count": 40, - "metadata": { - "collapsed": true - }, - "outputs": [], + "execution_count": 61, + "metadata": {}, + "outputs": [ + { + "data": { + "text/html": [ + "\n", + "\n", + "\n", + "\n", + " \n", + " \n", + " \n", + "\n", + "\n", + "

\n", + "\n", + "
def fol_fc_ask(KB, alpha):\n",
+       "    """A simple forward-chaining algorithm. [Figure 9.3]"""\n",
+       "    # TODO: Improve efficiency\n",
+       "    kb_consts = list({c for clause in KB.clauses for c in constant_symbols(clause)})\n",
+       "    def enum_subst(p):\n",
+       "        query_vars = list({v for clause in p for v in variables(clause)})\n",
+       "        for assignment_list in itertools.product(kb_consts, repeat=len(query_vars)):\n",
+       "            theta = {x: y for x, y in zip(query_vars, assignment_list)}\n",
+       "            yield theta\n",
+       "\n",
+       "    # check if we can answer without new inferences\n",
+       "    for q in KB.clauses:\n",
+       "        phi = unify(q, alpha, {})\n",
+       "        if phi is not None:\n",
+       "            yield phi\n",
+       "\n",
+       "    while True:\n",
+       "        new = []\n",
+       "        for rule in KB.clauses:\n",
+       "            p, q = parse_definite_clause(rule)\n",
+       "            for theta in enum_subst(p):\n",
+       "                if set(subst(theta, p)).issubset(set(KB.clauses)):\n",
+       "                    q_ = subst(theta, q)\n",
+       "                    if all([unify(x, q_, {}) is None for x in KB.clauses + new]):\n",
+       "                        new.append(q_)\n",
+       "                        phi = unify(q_, alpha, {})\n",
+       "                        if phi is not None:\n",
+       "                            yield phi\n",
+       "        if not new:\n",
+       "            break\n",
+       "        for clause in new:\n",
+       "            KB.tell(clause)\n",
+       "    return None\n",
+       "
\n", + "\n", + "\n" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + } + ], "source": [ - "%psource fol_fc_ask" + "psource(fol_fc_ask)" ] }, { @@ -2675,7 +3272,7 @@ }, { "cell_type": "code", - "execution_count": 41, + "execution_count": 62, "metadata": {}, "outputs": [ { @@ -2700,7 +3297,7 @@ }, { "cell_type": "code", - "execution_count": 42, + "execution_count": 63, "metadata": {}, "outputs": [ { @@ -2742,7 +3339,7 @@ }, { "cell_type": "code", - "execution_count": 43, + "execution_count": 64, "metadata": { "collapsed": true }, @@ -2761,7 +3358,7 @@ }, { "cell_type": "code", - "execution_count": 44, + "execution_count": 65, "metadata": { "collapsed": true }, @@ -2779,7 +3376,7 @@ }, { "cell_type": "code", - "execution_count": 45, + "execution_count": 66, "metadata": { "collapsed": true }, @@ -2791,7 +3388,7 @@ }, { "cell_type": "code", - "execution_count": 46, + "execution_count": 67, "metadata": {}, "outputs": [ { @@ -2800,7 +3397,7 @@ "{v_5: x, x: Nono}" ] }, - "execution_count": 46, + "execution_count": 67, "metadata": {}, "output_type": "execute_result" } @@ -2827,7 +3424,7 @@ }, { "cell_type": "code", - "execution_count": 47, + "execution_count": 68, "metadata": {}, "outputs": [ { @@ -2836,7 +3433,7 @@ "(P ==> ~Q)" ] }, - "execution_count": 47, + "execution_count": 68, "metadata": {}, "output_type": "execute_result" } @@ -2854,7 +3451,7 @@ }, { "cell_type": "code", - "execution_count": 48, + "execution_count": 69, "metadata": {}, "outputs": [ { @@ -2863,7 +3460,7 @@ "(P ==> ~Q)" ] }, - "execution_count": 48, + "execution_count": 69, "metadata": {}, "output_type": "execute_result" } @@ -2881,7 +3478,7 @@ }, { "cell_type": "code", - "execution_count": 49, + "execution_count": 70, "metadata": {}, "outputs": [ { @@ -2890,7 +3487,7 @@ "PartialExpr('==>', P)" ] }, - "execution_count": 49, + "execution_count": 70, "metadata": {}, "output_type": "execute_result" } @@ -2910,7 +3507,7 @@ }, { "cell_type": "code", - "execution_count": 50, + "execution_count": 71, "metadata": {}, "outputs": [ { @@ -2919,7 +3516,7 @@ "(P ==> ~Q)" ] }, - "execution_count": 50, + "execution_count": 71, "metadata": {}, "output_type": "execute_result" } @@ -2949,7 +3546,7 @@ }, { "cell_type": "code", - "execution_count": 51, + "execution_count": 72, "metadata": {}, "outputs": [ { @@ -2958,7 +3555,7 @@ "(~(P & Q) ==> (~P | ~Q))" ] }, - "execution_count": 51, + "execution_count": 72, "metadata": {}, "output_type": "execute_result" } @@ -2976,7 +3573,7 @@ }, { "cell_type": "code", - "execution_count": 52, + "execution_count": 73, "metadata": {}, "outputs": [ { @@ -2985,7 +3582,7 @@ "(~(P & Q) ==> (~P | ~Q))" ] }, - "execution_count": 52, + "execution_count": 73, "metadata": {}, "output_type": "execute_result" } @@ -3004,7 +3601,7 @@ }, { "cell_type": "code", - "execution_count": 53, + "execution_count": 74, "metadata": {}, "outputs": [ { @@ -3013,7 +3610,7 @@ "(((P & Q) ==> P) | Q)" ] }, - "execution_count": 53, + "execution_count": 74, "metadata": {}, "output_type": "execute_result" } @@ -3031,7 +3628,7 @@ }, { "cell_type": "code", - "execution_count": 54, + "execution_count": 75, "metadata": {}, "outputs": [ { @@ -3040,7 +3637,7 @@ "((P & Q) ==> (P | Q))" ] }, - "execution_count": 54, + "execution_count": 75, "metadata": {}, "output_type": "execute_result" } @@ -3058,11 +3655,133 @@ }, { "cell_type": "code", - "execution_count": null, - "metadata": { - "collapsed": true - }, - "outputs": [], + "execution_count": 76, + "metadata": {}, + "outputs": [ + { + "data": { + "text/html": [ + "\n", + "\n", + "
\n", + "\n", + "
\n", + "\n", + "\n" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, + { + "data": { + "text/html": [ + "" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + } + ], "source": [ "from notebook import Canvas_fol_bc_ask\n", "canvas_bc_ask = Canvas_fol_bc_ask('canvas_bc_ask', crime_kb, expr('Criminal(x)'))" diff --git a/tests/test_logic.py b/tests/test_logic.py index 86bcc9ed6..6da2eb320 100644 --- a/tests/test_logic.py +++ b/tests/test_logic.py @@ -2,6 +2,10 @@ from logic import * from utils import expr_handle_infix_ops, count, Symbol +definite_clauses_KB = PropDefiniteKB() +for clause in ['(B & F)==>E', '(A & E & F)==>G', '(B & C)==>F', '(A & B)==>D', '(E & F)==>H', '(H & I)==>J', 'A', 'B', 'C']: + definite_clauses_KB.tell(expr(clause)) + def test_is_symbol(): assert is_symbol('x') @@ -154,6 +158,10 @@ def test_unify(): def test_pl_fc_entails(): assert pl_fc_entails(horn_clauses_KB, expr('Q')) + assert pl_fc_entails(definite_clauses_KB, expr('G')) + assert pl_fc_entails(definite_clauses_KB, expr('H')) + assert not pl_fc_entails(definite_clauses_KB, expr('I')) + assert not pl_fc_entails(definite_clauses_KB, expr('J')) assert not pl_fc_entails(horn_clauses_KB, expr('SomethingSilly'))