{"nbformat":4,"nbformat_minor":0,"metadata":{"kernelspec":{"display_name":"Python 3","language":"python","name":"python3"},"language_info":{"codemirror_mode":{"name":"ipython","version":3},"file_extension":".py","mimetype":"text/x-python","name":"python","nbconvert_exporter":"python","pygments_lexer":"ipython3","version":"3.6.1"},"colab":{"name":"PB016_lab9.ipynb","provenance":[],"collapsed_sections":[]}},"cells":[{"cell_type":"markdown","metadata":{"id":"2F0wRc29TBuw"},"source":["# PB016: Artificial intelligence I, labs 9 - Introduction to resolution\n","\n","This week's topic is introduction to resolution. We'll focus namely on:\n","\n","1. __Resolution in propositional logic__\n","2. __Normal forms in predicate logic__"]},{"cell_type":"markdown","metadata":{"id":"BqFo2ZesTBuy"},"source":["---\n","\n","## 1. Resolution in propositional logic\n","\n","- Technique for proving the satisfiability of formulas in propositional logic.\n","- Used mainly for automatic reasoning and logic programming."]},{"cell_type":"markdown","metadata":{"id":"b43_luoWTBuz"},"source":["### __Exercise 1.1__\n","\n","Using resolution, show that the following entailment holds:\n","- ${\\neg p \\vee q, \\neg r \\Rightarrow \\neg q} \\models p \\Rightarrow r$\n","\n","### __Solution__"]},{"cell_type":"markdown","metadata":{"id":"ymTQM0h_bV7H"},"source":["_TODO - complete by editing this cell_"]},{"cell_type":"markdown","metadata":{"id":"eS0Jy34nTBu5"},"source":["### __Exercise 1.2__\n","\n","Refute the following set of formulas using general resolution:\n","- $( A \\vee B) \\wedge (\\neg{B} \\vee \\neg{C}) \\wedge (\\neg{A} \\vee D) \\wedge (\\neg{D}) \\wedge (C \\vee D)$\t  \n","\n","### __Solution__\n","\n","Note:\n","- Use the predefined node and edge templates in the cell below to draw the resolution tree here and in the other exercises (in the [DOT syntax](https://en.wikipedia.org/wiki/DOT_%28graph_description_language%29)).\n","- To keep things simple, use simply \"!\" or \"NOT\" for negation in the set notation of clauses. For the endpoint of the resolution use an empty box or \"NILL\"."]},{"cell_type":"code","metadata":{"id":"g0BVIAjhg3gT"},"source":["# pre-defined imports\n","import graphviz\n","from IPython.display import display\n","\n","# TODO - complete the specific shape of the resolution tree according to the following node and edge templates\n","tree = \"\"\"\n","digraph tree {\n","  1 [label=\"{A}\" shape=\"plain\"];\n","  2 [label=\"{!A}\" shape=\"plain\"];\n","  99 [label=\"\" shape=\"box\"];\n","\n","  1 -> 99;\n","  2 -> 99;\n","}\n","\"\"\"\n","\n","# pre-defined output\n","display(graphviz.Source(tree))"],"execution_count":null,"outputs":[]},{"cell_type":"markdown","metadata":{"id":"e29RAf62TBu-"},"source":["### __Exercise 1.3__\n","\n","Use linear resolution to show that the following formula is unsatisfiable (create at least two different proofs):\n","-  $S = (\\neg{A} \\vee \\neg{B} \\vee C) \\wedge (A \\vee B) \\wedge (A \\vee \\neg{C}) \\wedge (\\neg{A} \\vee B) \\wedge (A \\vee \\neg{B}) \\wedge (\\neg{A} \\vee \\neg{C}) \\wedge (A \\vee C) $\n","\n","Note: Linear resolution is a sequence $<C_0, B_0>, \\dots, <C_n, B_n>$, where:\n","- $C_0 \\in S \\wedge (B_i \\in S \\vee B_i = C_j, j < i)$\n","- $C_{i+1}$ is a resolvent of $C_i$ and $B_i$\n","- $C_{n+1} = []$ \n","\n","### __Solution__"]},{"cell_type":"code","metadata":{"id":"gTSfhtTqiMlY"},"source":["# pre-defined imports\n","import graphviz\n","from IPython.display import display\n","\n","# TODO - complete the specific shape of the resolution tree according to the following node and edge templates\n","tree = \"\"\"\n","digraph tree {\n","  1 [label=\"{A}\" shape=\"plain\"];\n","  2 [label=\"{!A}\" shape=\"plain\"];\n","  99 [label=\"\" shape=\"box\"];\n","\n","  1 -> 99;\n","  2 -> 99;\n","}\n","\"\"\"\n","\n","# pre-defined output\n","display(graphviz.Source(tree))"],"execution_count":null,"outputs":[]},{"cell_type":"markdown","metadata":{"id":"r8a6Cb82TBvC"},"source":["### __Exercise 1.4__\n","\n","Use LI resolution to show that the following formula is unsatisfiable:\n","- $S =  (q\\vee\\neg{p}\\vee\\neg{r}\\vee\\neg{s}) \\wedge (p\\vee\\neg{r}\\vee\\neg{s}) \\wedge (s\\vee\\neg{r}) \\wedge (r) \\wedge (\\neg{p}\\vee\\neg{q})$\n","\n","Note: LI (linear input) resolution $S = P \\cup \\{ G \\}$ is a sequence $<G_0, C_0>, \\dots, <G_n, C_n>$, where:\n","- $G_0 = G \\wedge \\forall i: C_i \\in P$  (thus $\\forall i: G_i$ only contains negative literals)\n","- $G_{i+1}$ is a resolvent of $G_i$ and $C_i$\n","- $G_{n+1} = []$ \n","\n","### __Solution__"]},{"cell_type":"markdown","metadata":{"id":"PIjaEK7Gio1H"},"source":["The formula in the set notation: _TODO_"]},{"cell_type":"code","metadata":{"id":"9nBnL74-ixyv"},"source":["# pre-defined imports\n","import graphviz\n","from IPython.display import display\n","\n","# TODO - complete the specific shape of the resolution tree according to the following node and edge templates\n","tree = \"\"\"\n","digraph tree {\n","  1 [label=\"{A}\" shape=\"plain\"];\n","  2 [label=\"{!A}\" shape=\"plain\"];\n","  99 [label=\"\" shape=\"box\"];\n","\n","  1 -> 99;\n","  2 -> 99;\n","}\n","\"\"\"\n","\n","# pre-defined output\n","display(graphviz.Source(tree))"],"execution_count":null,"outputs":[]},{"cell_type":"markdown","metadata":{"id":"xxzpPaU9TBvH"},"source":["### __Exercise 1.5__\n","\n","Use LD resolution to show that the following set of clauses is unsatisfiable:\n","- $S = \\{\\{\\neg s,q,\\neg t\\}, \\{\\neg s,\\neg r,p\\}, \\{\\neg t,s\\}, \\{\\neg p,\\neg q,\\neg r\\}, \\{r\\}, \\{t\\}\\}$\n","\n","Note: LD (linear input resolution for ordered clauses) is similar to linear resolution (LI), but clauses are ordered lists (duplicate literals cannot be automatically eliminated!).\n","\n","Resolvent for $[\\neg A_1, \\dots, \\neg A_n]$ and $[B_0, \\neg B_1, \\dots, \\neg B_n]$ for $A_i = \\neg B_0$ is $[\\neg A_1, \\dots, \\neg A_{i-1}, \\neg B_1, \\dots, \\neg B_n, \\neg A_{i+1}, \\dots, \\neg A_n]$\n","\n","### __Solution__"]},{"cell_type":"markdown","metadata":{"id":"8TRCTkAKi6xt"},"source":["_TODO_ - conversion of the set of clauses, identification of the target clause"]},{"cell_type":"code","metadata":{"id":"3zj0QiJnjM5u"},"source":["# pre-defined imports\n","import graphviz\n","from IPython.display import display\n","\n","# TODO - complete the specific shape of the resolution tree according to the following node and edge templates\n","tree = \"\"\"\n","digraph tree {\n","  1 [label=\"{A}\" shape=\"plain\"];\n","  2 [label=\"{!A}\" shape=\"plain\"];\n","  99 [label=\"\" shape=\"box\"];\n","\n","  1 -> 99;\n","  2 -> 99;\n","}\n","\"\"\"\n","\n","# pre-defined output\n","display(graphviz.Source(tree))"],"execution_count":null,"outputs":[]},{"cell_type":"markdown","metadata":{"id":"B9TGUgWUTBvL"},"source":["### __Exercise 1.6__\n","\n","Use SLD resolution to show that the following set of ordered clauses is unsatisfiable:\n","- $S = \\{[q,\\neg s,\\neg t], [p,\\neg s,\\neg r], [s,\\neg t], [r], [t]\\} \\cup \\{[\\neg p,\\neg q,\\neg r]\\}$\n","\n","Note: SLD (Linear Input resolutions for ordered clauses with a selection rule):\n","- in the $i$-th step one resolves on the literal $ R(G_i) = A_i $;\n","- used in Prolog ($ R $ always selects the leftmost position).\n","\n","### __Solution__"]},{"cell_type":"code","metadata":{"id":"24GAsJJJjXeN"},"source":["# pre-defined imports\n","import graphviz\n","from IPython.display import display\n","\n","# TODO - complete the specific shape of the resolution tree according to the following node and edge templates\n","tree = \"\"\"\n","digraph tree {\n","  1 [label=\"{A}\" shape=\"plain\"];\n","  2 [label=\"{!A}\" shape=\"plain\"];\n","  99 [label=\"\" shape=\"box\"];\n","\n","  1 -> 99;\n","  2 -> 99;\n","}\n","\"\"\"\n","\n","# pre-defined output\n","display(graphviz.Source(tree))"],"execution_count":null,"outputs":[]},{"cell_type":"markdown","metadata":{"id":"YkraX9n4TBvP"},"source":["---\n","\n","## 2. Normal forms in predicate logic\n","\n","- We will focus in particular on:\n","  - [prenex normal form](https://en.wikipedia.org/wiki/Prenex_normal_form) - a formula consisting of two parts:\n","    - a prefix containing only quantifiers and bound variables;\n","    - formula body without quantifiers.\n","  - [Skolem's normal form](https://en.wikipedia.org/wiki/Skolem_normal_form) - a formula in the prenex normal form containing only universal quantifiers.\n","- Similarky to propositional logic, normal forms are suitable for algorithmic proving of satisfiability of formulas in PL1 (e.g., using SLD resolution for PL1, which we will deal with in the next labs)."]},{"cell_type":"markdown","metadata":{"id":"CaK5bLkETBvQ"},"source":["### __Exercise 2.1__\n","\n","Convert to normal prenex form and perform Scolemization:\n","- $\\exists z (\\forall y (\\exists x P(x,y) \\Rightarrow Q(y,z)) \\wedge \\exists y (\\forall x R(x,y) \\vee Q(z,y)))$\n","\n","### __Solution__"]},{"cell_type":"markdown","metadata":{"id":"NKnKXT2yQKR_"},"source":["_TODO - complete by editing this cell_"]},{"cell_type":"markdown","metadata":{"id":"I9WZ_qMkTBvU"},"source":["### __Exercise 2.2__\n","\n","Convert to normal prenex form and perform Scolemization:\n","- $\\forall y \\exists x R(x,y) \\Leftrightarrow \\forall x \\forall y P(x,y) $\n","\n","### __Solution__"]},{"cell_type":"markdown","metadata":{"id":"Erq3EdPxQM_g"},"source":["_TODO - complete by editing this cell_"]},{"cell_type":"markdown","metadata":{"id":"JT08lxOWTBvZ"},"source":["### __Exercise 2.3__\n","\n","Convert to normal prenex form and perform Scolemization:\n","- $(\\forall x \\exists y Q(x,y) \\vee \\exists x \\forall y P(x,y)) \\wedge \\neg \\exists x \\exists y P(x,y) $\n","\n","### __Solution__"]},{"cell_type":"markdown","metadata":{"id":"bIi7rEWYQkNA"},"source":["_TODO - complete by editing this cell_"]},{"cell_type":"markdown","metadata":{"id":"uC1MtxUKTBvd"},"source":["### __Exercise 2.4__\n","\n","Convert to normal prenex form and perform Scolemization:\n","- $\\neg (\\forall x \\exists y P(x,y) \\Rightarrow \\exists x \\exists y R(x,y)) \\wedge \\forall x (\\neg \\exists y Q(x,y)) $\n","\n","### __Solution__"]},{"cell_type":"markdown","metadata":{"id":"TWKQW0vLQm7g"},"source":["_TODO - complete by editing this cell_"]}]}