diff --git a/logic_programming/4_DPLL.ipynb b/logic_programming/4_DPLL.ipynb index 484cfc0f6bae6d4e2b2ed17ecb93a7c0fe6d71e7..60825dfd053fee73e71008cb60fa723110c76cf5 100644 --- a/logic_programming/4_DPLL.ipynb +++ b/logic_programming/4_DPLL.ipynb @@ -969,6 +969,7 @@ "source": [ "dpll(Clauses,[unit(Lit)|Stack]) :-\n", " select([Lit],Clauses,Clauses2), % unit clause found\n", + " !,\n", " set_literal(Lit,Clauses2,Clauses3),\n", " dpll(Clauses3,Stack).\n", "dpll([],Stack) :- !, Stack=[]. % SAT\n", @@ -1384,7 +1385,7 @@ { "data": { "text/plain": [ - "Solving problem 2 : Knights & Knaves (Proof by contradiction)\n", + "Solving problem 5 : schaltung_a1.pl\n", "UNSAT: no model exists" ] }, @@ -1402,7 +1403,7 @@ } ], "source": [ - "?-test(2)." + "?-test(5)." ] }, { @@ -1568,6 +1569,18 @@ "source": [ "show_term($Tree)" ] + }, + { + "cell_type": "code", + "execution_count": null, + "id": "94b3da71", + "metadata": { + "vscode": { + "languageId": "prolog" + } + }, + "outputs": [], + "source": [] } ], "metadata": { diff --git a/logic_programming/4_DPLL.pdf b/logic_programming/4_DPLL.pdf new file mode 100644 index 0000000000000000000000000000000000000000..3846ee3337d7d709fadfc4efbd854dbdba0107df Binary files /dev/null and b/logic_programming/4_DPLL.pdf differ diff --git a/logic_programming/5_SLD.pdf b/logic_programming/5_SLD.pdf new file mode 100644 index 0000000000000000000000000000000000000000..3239e62cb11e895a8fcc1c69c3b6da91042ae5fd Binary files /dev/null and b/logic_programming/5_SLD.pdf differ