From 4eb9cfd697ef5f59c96bed4b538752c93b894db5 Mon Sep 17 00:00:00 2001 From: AngryCracker Date: Wed, 7 Mar 2018 23:27:31 +0530 Subject: [PATCH 1/5] Added pl-fc-entails section --- logic.ipynb | 849 ++++++++++++++++++++++++++++++++++++++++++++++++---- 1 file changed, 784 insertions(+), 65 deletions(-) diff --git a/logic.ipynb b/logic.ipynb index 726a8d69d..9ee1b1c7c 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", + "Introducing this section, 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'))" ] }, { @@ -1510,7 +1975,7 @@ }, { "cell_type": "code", - "execution_count": 27, + "execution_count": 48, "metadata": { "collapsed": true }, @@ -1539,7 +2004,7 @@ }, { "cell_type": "code", - "execution_count": 28, + "execution_count": 49, "metadata": { "collapsed": true }, @@ -1560,7 +2025,7 @@ }, { "cell_type": "code", - "execution_count": 29, + "execution_count": 50, "metadata": { "collapsed": true }, @@ -1581,7 +2046,7 @@ }, { "cell_type": "code", - "execution_count": 30, + "execution_count": 51, "metadata": { "collapsed": true }, @@ -1605,7 +2070,7 @@ }, { "cell_type": "code", - "execution_count": 31, + "execution_count": 52, "metadata": { "collapsed": true }, @@ -1626,7 +2091,7 @@ }, { "cell_type": "code", - "execution_count": 32, + "execution_count": 53, "metadata": { "collapsed": true }, @@ -1646,7 +2111,7 @@ }, { "cell_type": "code", - "execution_count": 33, + "execution_count": 54, "metadata": { "collapsed": true }, @@ -1665,7 +2130,7 @@ }, { "cell_type": "code", - "execution_count": 34, + "execution_count": 55, "metadata": { "collapsed": true }, @@ -1692,7 +2157,7 @@ }, { "cell_type": "code", - "execution_count": 35, + "execution_count": 56, "metadata": {}, "outputs": [ { @@ -1701,7 +2166,7 @@ "{x: 3}" ] }, - "execution_count": 35, + "execution_count": 56, "metadata": {}, "output_type": "execute_result" } @@ -1712,7 +2177,7 @@ }, { "cell_type": "code", - "execution_count": 36, + "execution_count": 57, "metadata": {}, "outputs": [ { @@ -1721,7 +2186,7 @@ "{x: B}" ] }, - "execution_count": 36, + "execution_count": 57, "metadata": {}, "output_type": "execute_result" } @@ -1732,7 +2197,7 @@ }, { "cell_type": "code", - "execution_count": 37, + "execution_count": 58, "metadata": {}, "outputs": [ { @@ -1741,7 +2206,7 @@ "{x: Bella, y: Dobby}" ] }, - "execution_count": 37, + "execution_count": 58, "metadata": {}, "output_type": "execute_result" } @@ -1759,7 +2224,7 @@ }, { "cell_type": "code", - "execution_count": 38, + "execution_count": 59, "metadata": {}, "outputs": [ { @@ -1783,7 +2248,7 @@ }, { "cell_type": "code", - "execution_count": 39, + "execution_count": 60, "metadata": {}, "outputs": [ { @@ -1810,13 +2275,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)" ] }, { @@ -1828,7 +2425,7 @@ }, { "cell_type": "code", - "execution_count": 41, + "execution_count": 62, "metadata": {}, "outputs": [ { @@ -1853,7 +2450,7 @@ }, { "cell_type": "code", - "execution_count": 42, + "execution_count": 63, "metadata": {}, "outputs": [ { @@ -1895,7 +2492,7 @@ }, { "cell_type": "code", - "execution_count": 43, + "execution_count": 64, "metadata": { "collapsed": true }, @@ -1914,7 +2511,7 @@ }, { "cell_type": "code", - "execution_count": 44, + "execution_count": 65, "metadata": { "collapsed": true }, @@ -1932,7 +2529,7 @@ }, { "cell_type": "code", - "execution_count": 45, + "execution_count": 66, "metadata": { "collapsed": true }, @@ -1944,7 +2541,7 @@ }, { "cell_type": "code", - "execution_count": 46, + "execution_count": 67, "metadata": {}, "outputs": [ { @@ -1953,7 +2550,7 @@ "{v_5: x, x: Nono}" ] }, - "execution_count": 46, + "execution_count": 67, "metadata": {}, "output_type": "execute_result" } @@ -1980,7 +2577,7 @@ }, { "cell_type": "code", - "execution_count": 47, + "execution_count": 68, "metadata": {}, "outputs": [ { @@ -1989,7 +2586,7 @@ "(P ==> ~Q)" ] }, - "execution_count": 47, + "execution_count": 68, "metadata": {}, "output_type": "execute_result" } @@ -2007,7 +2604,7 @@ }, { "cell_type": "code", - "execution_count": 48, + "execution_count": 69, "metadata": {}, "outputs": [ { @@ -2016,7 +2613,7 @@ "(P ==> ~Q)" ] }, - "execution_count": 48, + "execution_count": 69, "metadata": {}, "output_type": "execute_result" } @@ -2034,7 +2631,7 @@ }, { "cell_type": "code", - "execution_count": 49, + "execution_count": 70, "metadata": {}, "outputs": [ { @@ -2043,7 +2640,7 @@ "PartialExpr('==>', P)" ] }, - "execution_count": 49, + "execution_count": 70, "metadata": {}, "output_type": "execute_result" } @@ -2063,7 +2660,7 @@ }, { "cell_type": "code", - "execution_count": 50, + "execution_count": 71, "metadata": {}, "outputs": [ { @@ -2072,7 +2669,7 @@ "(P ==> ~Q)" ] }, - "execution_count": 50, + "execution_count": 71, "metadata": {}, "output_type": "execute_result" } @@ -2102,7 +2699,7 @@ }, { "cell_type": "code", - "execution_count": 51, + "execution_count": 72, "metadata": {}, "outputs": [ { @@ -2111,7 +2708,7 @@ "(~(P & Q) ==> (~P | ~Q))" ] }, - "execution_count": 51, + "execution_count": 72, "metadata": {}, "output_type": "execute_result" } @@ -2129,7 +2726,7 @@ }, { "cell_type": "code", - "execution_count": 52, + "execution_count": 73, "metadata": {}, "outputs": [ { @@ -2138,7 +2735,7 @@ "(~(P & Q) ==> (~P | ~Q))" ] }, - "execution_count": 52, + "execution_count": 73, "metadata": {}, "output_type": "execute_result" } @@ -2157,7 +2754,7 @@ }, { "cell_type": "code", - "execution_count": 53, + "execution_count": 74, "metadata": {}, "outputs": [ { @@ -2166,7 +2763,7 @@ "(((P & Q) ==> P) | Q)" ] }, - "execution_count": 53, + "execution_count": 74, "metadata": {}, "output_type": "execute_result" } @@ -2184,7 +2781,7 @@ }, { "cell_type": "code", - "execution_count": 54, + "execution_count": 75, "metadata": {}, "outputs": [ { @@ -2193,7 +2790,7 @@ "((P & Q) ==> (P | Q))" ] }, - "execution_count": 54, + "execution_count": 75, "metadata": {}, "output_type": "execute_result" } @@ -2211,11 +2808,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)'))" From bc3910fc4461571694a2f81f40d99643e226b6ea Mon Sep 17 00:00:00 2001 From: AngryCracker Date: Wed, 7 Mar 2018 23:31:46 +0530 Subject: [PATCH 2/5] Updated README.md --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index c97db60f1..88b59c617 100644 --- a/README.md +++ b/README.md @@ -98,7 +98,7 @@ Here is a table of algorithms, the figure, name of the algorithm in the book and | 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 | Included | -| 7.15 | PL-FC-Entails? | `pl_fc_resolution` | [`logic.py`][logic] | Done | | +| 7.15 | PL-FC-Entails? | `pl_fc_resolution` | [`logic.py`][logic] | Done | Included | | 7.17 | DPLL-Satisfiable? | `dpll_satisfiable` | [`logic.py`][logic] | Done | | | 7.18 | WalkSAT | `WalkSAT` | [`logic.py`][logic] | Done | | | 7.20 | Hybrid-Wumpus-Agent | `HybridWumpusAgent` | | | | From 6b949efbf424702641dd6940f0ea29961275bd30 Mon Sep 17 00:00:00 2001 From: AngryCracker Date: Wed, 7 Mar 2018 23:37:12 +0530 Subject: [PATCH 3/5] Updated filename --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index 88b59c617..303a827d5 100644 --- a/README.md +++ b/README.md @@ -98,7 +98,7 @@ Here is a table of algorithms, the figure, name of the algorithm in the book and | 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 | Included | -| 7.15 | PL-FC-Entails? | `pl_fc_resolution` | [`logic.py`][logic] | Done | Included | +| 7.15 | PL-FC-Entails? | `pl_fc_entails` | [`logic.py`][logic] | Done | Included | | 7.17 | DPLL-Satisfiable? | `dpll_satisfiable` | [`logic.py`][logic] | Done | | | 7.18 | WalkSAT | `WalkSAT` | [`logic.py`][logic] | Done | | | 7.20 | Hybrid-Wumpus-Agent | `HybridWumpusAgent` | | | | From 78301d2ed6b6abb02cd4ad6cf95dfbe03975fa32 Mon Sep 17 00:00:00 2001 From: AngryCracker Date: Wed, 7 Mar 2018 23:45:29 +0530 Subject: [PATCH 4/5] Added tests for pl-fc-entails --- tests/test_logic.py | 8 ++++++++ 1 file changed, 8 insertions(+) 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')) From db06415fe4650bfc234fc6eea9f0be6ff1aca168 Mon Sep 17 00:00:00 2001 From: AngryCracker Date: Fri, 9 Mar 2018 03:56:28 +0530 Subject: [PATCH 5/5] Review fixes --- logic.ipynb | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/logic.ipynb b/logic.ipynb index 9ee1b1c7c..79e439ba0 100644 --- a/logic.ipynb +++ b/logic.ipynb @@ -1494,7 +1494,7 @@ "metadata": {}, "source": [ "### Forward and backward chaining\n", - "Introducing this section, we said we will look at two algorithms to check if a sentence is entailed by the `KB`, \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", @@ -1502,9 +1502,9 @@ "#### 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", + "A Horn clause with exactly one positive literal is called a *definite clause*.\n", "
\n", - "A horn clause might look like \n", + "A Horn clause might look like \n", "
\n", "$\\neg a\\lor\\neg b\\lor\\neg c\\lor\\neg d... \\lor z$\n", "
\n",