diff --git a/logic_programming/3_PropositionalLogic.ipynb b/logic_programming/3_PropositionalLogic.ipynb
index c3a594f00359a9e1641575d7ffa27a2d41be0341..4caace5763452aebee66bc96320a75d3d1907dad 100644
--- a/logic_programming/3_PropositionalLogic.ipynb
+++ b/logic_programming/3_PropositionalLogic.ipynb
@@ -42,7 +42,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 34,
+   "execution_count": 2,
    "id": "964ebd52",
    "metadata": {
     "vscode": {
@@ -63,7 +63,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 35,
+   "execution_count": 3,
    "id": "fc6823ad",
    "metadata": {
     "vscode": {
@@ -87,7 +87,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 36,
+   "execution_count": 4,
    "id": "152289b6",
    "metadata": {
     "vscode": {
@@ -111,7 +111,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 37,
+   "execution_count": 5,
    "id": "2c3dd1bf",
    "metadata": {
     "vscode": {
@@ -166,7 +166,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 38,
+   "execution_count": 6,
    "id": "78163b60",
    "metadata": {
     "vscode": {
@@ -187,7 +187,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 39,
+   "execution_count": 7,
    "id": "8ddb568d",
    "metadata": {
     "vscode": {
@@ -211,7 +211,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 40,
+   "execution_count": 8,
    "id": "075dc3b2",
    "metadata": {
     "vscode": {
@@ -235,7 +235,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 41,
+   "execution_count": 9,
    "id": "338cb7dd",
    "metadata": {
     "vscode": {
@@ -269,7 +269,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 42,
+   "execution_count": 10,
    "id": "f6116612",
    "metadata": {
     "vscode": {
@@ -293,7 +293,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 43,
+   "execution_count": 11,
    "id": "d7e68593",
    "metadata": {
     "vscode": {
@@ -343,7 +343,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 44,
+   "execution_count": 12,
    "id": "3646e3ee",
    "metadata": {
     "vscode": {
@@ -403,7 +403,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 45,
+   "execution_count": 13,
    "id": "350b9756",
    "metadata": {
     "vscode": {
@@ -443,7 +443,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 46,
+   "execution_count": 14,
    "id": "3101448b",
    "metadata": {
     "vscode": {
@@ -467,7 +467,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 47,
+   "execution_count": 15,
    "id": "922004e9",
    "metadata": {
     "vscode": {
@@ -499,7 +499,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 48,
+   "execution_count": 16,
    "id": "54b57ff8",
    "metadata": {
     "vscode": {
@@ -558,7 +558,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 49,
+   "execution_count": 17,
    "id": "8f6d804b",
    "metadata": {
     "vscode": {
@@ -593,7 +593,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 50,
+   "execution_count": 18,
    "id": "175c00d0",
    "metadata": {
     "vscode": {
@@ -626,7 +626,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 51,
+   "execution_count": 19,
    "id": "eee17774",
    "metadata": {
     "vscode": {
@@ -659,7 +659,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 52,
+   "execution_count": 20,
    "id": "fec75f65",
    "metadata": {
     "vscode": {
@@ -692,7 +692,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 53,
+   "execution_count": 21,
    "id": "78473da0",
    "metadata": {
     "vscode": {
@@ -747,7 +747,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 54,
+   "execution_count": 22,
    "id": "2ee60c15",
    "metadata": {
     "vscode": {
@@ -765,7 +765,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 55,
+   "execution_count": 23,
    "id": "2b497dad",
    "metadata": {
     "vscode": {
@@ -810,7 +810,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 56,
+   "execution_count": 24,
    "id": "0fd23f05",
    "metadata": {
     "vscode": {
@@ -863,7 +863,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 57,
+   "execution_count": 25,
    "id": "23775624",
    "metadata": {
     "vscode": {
@@ -905,7 +905,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 58,
+   "execution_count": 26,
    "id": "7a6e29ed",
    "metadata": {
     "vscode": {
@@ -959,7 +959,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 59,
+   "execution_count": 27,
    "id": "6bd292f4",
    "metadata": {
     "vscode": {
@@ -1009,12 +1009,58 @@
    },
    "source": [
     "A formula which has at least one model is called <b>satisfiable</b>.\n",
+    "\n",
+    "We can use our code above to find models, by leaving the interpretation of propositions as Prolog variables\n",
+    "and by requiring the result to be `true`:"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 28,
+   "id": "ab15628a",
+   "metadata": {
+    "vscode": {
+     "languageId": "prolog"
+    }
+   },
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "\u001b[1mP = true,\n",
+       "Q = true"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    }
+   ],
+   "source": [
+    "?-value(and(p,or(q,not(p))), [p/P, q/Q],true)."
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "64baad25",
+   "metadata": {},
+   "source": [
+    "The above is not a very efficient way of finding models.\n",
+    "We return to this issue later.\n",
+    "A tool that determines whehter a propositional logic formula is satisfiable and computes possibles models is called a <b>SAT solver</b>."
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "8b2acc10",
+   "metadata": {},
+   "source": [
+    "\n",
     "Two formulas are called <b>equivalent</b> iff they have the same models:"
    ]
   },
   {
    "cell_type": "code",
-   "execution_count": 60,
+   "execution_count": 29,
    "id": "b912acd3",
    "metadata": {
     "vscode": {
@@ -1060,7 +1106,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 61,
+   "execution_count": 30,
    "id": "f4c9823d",
    "metadata": {
     "vscode": {
@@ -1106,13 +1152,369 @@
   },
   {
    "cell_type": "code",
-   "execution_count": null,
+   "execution_count": 33,
+   "id": "68a2a19c",
+   "metadata": {
+    "vscode": {
+     "languageId": "prolog"
+    }
+   },
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "P | Q | NotPandQ | PimpliesQ | \n",
+       ":- | :- | :- | :- | \n",
+       "true | true | true | true | \n",
+       "true | false | false | false | \n",
+       "false | true | true | true | \n",
+       "false | false | true | true | "
+      ],
+      "text/plain": [
+       "P | Q | NotPandQ | PimpliesQ | \n",
+       ":- | :- | :- | :- | \n",
+       "true | true | true | true | \n",
+       "true | false | false | false | \n",
+       "false | true | true | true | \n",
+       "false | false | true | true | "
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    },
+    {
+     "data": {
+      "text/plain": [
+       "\u001b[1mtrue"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    }
+   ],
+   "source": [
+    "jupyter:print_table((user:value(or(not(p),q), [p/P, q/Q],NotPandQ),user:value(implies(p,q), [p/P, q/Q],PimpliesQ)))"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "248d3d32",
+   "metadata": {},
+   "source": [
+    "A formula `B` is the logical consequence of `A` if all models of `A` are also models of `B`:"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 32,
    "id": "aaf46953",
    "metadata": {
     "vscode": {
      "languageId": "prolog"
     }
    },
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "P | Q | PandQ | PorQ | \n",
+       ":- | :- | :- | :- | \n",
+       "true | true | true | true | \n",
+       "true | false | false | true | \n",
+       "false | true | false | true | \n",
+       "false | false | false | false | "
+      ],
+      "text/plain": [
+       "P | Q | PandQ | PorQ | \n",
+       ":- | :- | :- | :- | \n",
+       "true | true | true | true | \n",
+       "true | false | false | true | \n",
+       "false | true | false | true | \n",
+       "false | false | false | false | "
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    },
+    {
+     "data": {
+      "text/plain": [
+       "\u001b[1mtrue"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    }
+   ],
+   "source": [
+    "jupyter:print_table((user:value(and(p,q), [p/P, q/Q],PandQ),user:value(or(p,q), [p/P, q/Q],PorQ)))"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "3e261892",
+   "metadata": {},
+   "source": [
+    "## Improving our Prolog program\n",
+    "\n",
+    "For convenience we now write some piece of Prolog code to find the atomic propositions used within a formula.\n",
+    "This obviates the need to write interpretation skeletons like `[p/P,q/Q]` ourselves."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 35,
+   "id": "da0a82b5",
+   "metadata": {
+    "vscode": {
+     "languageId": "prolog"
+    }
+   },
+   "outputs": [],
+   "source": [
+    "get_aps(Formula,SortedPropositions) :- findall(P, ap(Formula,P), Ps), sort(Ps,SortedPropositions).\n",
+    "% extract atomic propostions used by formula\n",
+    "ap(X,X) :- atomic(X).\n",
+    "ap(and(A,B),AP) :- ap(A,AP) ; ap(B,AP).\n",
+    "ap(or(A,B),AP) :- ap(A,AP) ; ap(B,AP).\n",
+    "ap(implies(A,B),AP) :- ap(A,AP) ; ap(B,AP).\n",
+    "ap(equiv(A,B),AP) :- ap(A,AP) ; ap(B,AP).\n",
+    "ap(not(A),AP) :- ap(A,AP)."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 36,
+   "id": "82980216",
+   "metadata": {
+    "vscode": {
+     "languageId": "prolog"
+    }
+   },
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "\u001b[1mPs = [p,q]"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    }
+   ],
+   "source": [
+    "?- get_aps(and(p,q),Ps)."
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "e4c2468b",
+   "metadata": {},
+   "source": [
+    "We can now write a more convenient predicate to find models for a formula:"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 39,
+   "id": "23cfb806",
+   "metadata": {
+    "vscode": {
+     "languageId": "prolog"
+    }
+   },
+   "outputs": [],
+   "source": [
+    "sat(Formula,Interpretation) :-\n",
+    "   get_aps(Formula,SPs),\n",
+    "   skel(SPs,Interpretation), % set up interpretation skeleton\n",
+    "   value(Formula,Interpretation,true).\n",
+    "\n",
+    "skel([],[]).\n",
+    "skel([AP|T],[AP/_|ST]) :- skel(T,ST). % we replace p by p/_ so that we have an unbound logical varible for every proposition\n",
+    "\n",
+    "unsat(Formula) :- \\+ sat(Formula,_). % a formula is unsatisfiable if we can find no model, \\+ is Prolog negation"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 38,
+   "id": "6338f6bf",
+   "metadata": {
+    "vscode": {
+     "languageId": "prolog"
+    }
+   },
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "\u001b[1mModel = [p/true,q/true]"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    }
+   ],
+   "source": [
+    "?- sat(and(p,or(q,not(p))),Model)."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 40,
+   "id": "266a4bd8",
+   "metadata": {
+    "vscode": {
+     "languageId": "prolog"
+    }
+   },
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "\u001b[1mtrue"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    }
+   ],
+   "source": [
+    "?- unsat(and(p,not(p)))."
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "9fb0715e",
+   "metadata": {},
+   "source": [
+    "## Proof by contradiction\n",
+    "\n",
+    "To prove that `B` is a logical consequence of `A` we can employ a <b>proof by contradiction</b>:\n",
+    "- assume that `B` is false and\n",
+    "- show that this leads to a contradiction."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 41,
+   "id": "6957d9f3",
+   "metadata": {
+    "vscode": {
+     "languageId": "prolog"
+    }
+   },
+   "outputs": [],
+   "source": [
+    "prove(A,B) :- /* prove that B follows from A */\n",
+    "   unsat(and(A,not(B)))."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 42,
+   "id": "f552a71e",
+   "metadata": {
+    "vscode": {
+     "languageId": "prolog"
+    }
+   },
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "\u001b[1mtrue"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    }
+   ],
+   "source": [
+    "?- prove(and(p,q),or(p,q))."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 43,
+   "id": "e7a2828d",
+   "metadata": {
+    "vscode": {
+     "languageId": "prolog"
+    }
+   },
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "\u001b[1;31mfalse"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    }
+   ],
+   "source": [
+    "?- prove(or(p,q),and(p,q))."
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "02395cde",
+   "metadata": {},
+   "source": [
+    "In case something is not a logical consequence we can use this code to find an explanation (aka counter example):"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 44,
+   "id": "26bab55b",
+   "metadata": {
+    "vscode": {
+     "languageId": "prolog"
+    }
+   },
+   "outputs": [],
+   "source": [
+    "disprove(A,B,CounterExample) :- /* show why B does not follow from A */\n",
+    "   sat(and(A,not(B)),CounterExample)."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 45,
+   "id": "fe5daeb4",
+   "metadata": {
+    "vscode": {
+     "languageId": "prolog"
+    }
+   },
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "\u001b[1mCounter = [p/true,q/false]"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    }
+   ],
+   "source": [
+    "?- disprove(or(p,q),and(p,q),Counter)."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "id": "3187bee7",
+   "metadata": {
+    "vscode": {
+     "languageId": "prolog"
+    }
+   },
    "outputs": [],
    "source": []
   }