diff --git a/logic_programming/3_PropositionalLogic.ipynb b/logic_programming/3_PropositionalLogic.ipynb
index 4caace5763452aebee66bc96320a75d3d1907dad..0c42acec8cbc5ec89d6d61ab7f1b302ccd096575 100644
--- a/logic_programming/3_PropositionalLogic.ipynb
+++ b/logic_programming/3_PropositionalLogic.ipynb
@@ -1272,7 +1272,8 @@
    },
    "outputs": [],
    "source": [
-    "get_aps(Formula,SortedPropositions) :- findall(P, ap(Formula,P), Ps), sort(Ps,SortedPropositions).\n",
+    "get_aps(Formula,SortedPropositions) :- \n",
+    "    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",
@@ -1398,7 +1399,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 41,
+   "execution_count": 46,
    "id": "6957d9f3",
    "metadata": {
     "vscode": {
@@ -1408,7 +1409,9 @@
    "outputs": [],
    "source": [
     "prove(A,B) :- /* prove that B follows from A */\n",
-    "   unsat(and(A,not(B)))."
+    "   unsat(and(A,not(B))).\n",
+    "\n",
+    "equivalent(A,B) :- prove(A,B), prove(B,A)."
    ]
   },
   {
@@ -1435,6 +1438,30 @@
     "?- prove(and(p,q),or(p,q))."
    ]
   },
+  {
+   "cell_type": "code",
+   "execution_count": 48,
+   "id": "f8aca8b7",
+   "metadata": {
+    "vscode": {
+     "languageId": "prolog"
+    }
+   },
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "\u001b[1;31mfalse"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    }
+   ],
+   "source": [
+    "?- equivalent(and(p,q),or(p,q))."
+   ]
+  },
   {
    "cell_type": "code",
    "execution_count": 43,
@@ -1506,15 +1533,147 @@
     "?- disprove(or(p,q),and(p,q),Counter)."
    ]
   },
+  {
+   "cell_type": "markdown",
+   "id": "870939fa",
+   "metadata": {},
+   "source": [
+    "## Some Puzzles\n",
+    "\n",
+    "We can return to our Knights & Knave puzzle from the first lecture.\n",
+    "There is an island populated by only knights and knaves.\n",
+    "Knights always say the truth and knaves always lie.\n",
+    "We encounter three persons A,B,C on this island:\n",
+    "- 1. A says: “B is a knave oder C is a knave”\n",
+    "- 2. B says: “A is a knight”"
+   ]
+  },
   {
    "cell_type": "code",
-   "execution_count": null,
+   "execution_count": 50,
    "id": "3187bee7",
    "metadata": {
     "vscode": {
      "languageId": "prolog"
     }
    },
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "\u001b[1mI = [a/true,b/true,c/false]"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    }
+   ],
+   "source": [
+    "?- sat(and(equiv(a,or(not(b),not(c))),equiv(b,a)),I)."
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "575d68a0",
+   "metadata": {},
+   "source": [
+    "We can also prove that this is the only solution, i.e., our puzzle implies that A and B are knights and C is a knave:"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 52,
+   "id": "df153b0a",
+   "metadata": {
+    "vscode": {
+     "languageId": "prolog"
+    }
+   },
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "\u001b[1mtrue"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    }
+   ],
+   "source": [
+    "?- prove(and(equiv(a,or(not(b),not(c))),equiv(b,a)), and(a,and(b,not(c))))."
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "c0299ea9",
+   "metadata": {},
+   "source": [
+    "Let us now model another puzzle from Raymond Smullyan.\n",
+    "\n",
+    "- The King says: One note tells the truth and one does not\n",
+    "- Note on Door 1: This cell contains a princess and there is a tiger in the other cell\n",
+    "- Note on Door 2: One of the cells contains a princess and the other one contains a tiger.\n",
+    "\n"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 53,
+   "id": "4363c114",
+   "metadata": {
+    "vscode": {
+     "languageId": "prolog"
+    }
+   },
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "\u001b[1mI = [t1/true,t2/false,z1/false,z2/true]"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    }
+   ],
+   "source": [
+    "?- sat(and(equiv(z1,not(z2)),and(equiv(z1,and(not(t1),t2)),equiv(z2,equiv(t1,not(t2))))),I)."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 54,
+   "id": "0919b40c",
+   "metadata": {
+    "vscode": {
+     "languageId": "prolog"
+    }
+   },
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "\u001b[1;31mfalse"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    }
+   ],
+   "source": [
+    "jupyter:retry."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "id": "51d5630b",
+   "metadata": {
+    "vscode": {
+     "languageId": "prolog"
+    }
+   },
    "outputs": [],
    "source": []
   }