From d661ab899e25a8716277797cf01587e20b861188 Mon Sep 17 00:00:00 2001
From: Michael Leuschel <leuschel@uni-duesseldorf.de>
Date: Tue, 25 Oct 2022 11:25:12 +0200
Subject: [PATCH] add $Var feature usage

Signed-off-by: Michael Leuschel <leuschel@uni-duesseldorf.de>
---
 logic_programming/3_PropositionalLogic.ipynb | 57 ++++++++++++++++----
 1 file changed, 47 insertions(+), 10 deletions(-)

diff --git a/logic_programming/3_PropositionalLogic.ipynb b/logic_programming/3_PropositionalLogic.ipynb
index 75d3037..f81f348 100644
--- a/logic_programming/3_PropositionalLogic.ipynb
+++ b/logic_programming/3_PropositionalLogic.ipynb
@@ -25,6 +25,8 @@
     "- (a ⟺ b)\n",
     "No other formulas are WFF.\n",
     "\n",
+    "Note in the slides we use the single arrow `→` instead of the double arrow `⇒` for implication.\n",
+    "\n",
     "Comment: a, b are metavariablens outside the syntax of propositional logic.\n"
    ]
   },
@@ -166,7 +168,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 6,
+   "execution_count": 64,
    "id": "78163b60",
    "metadata": {
     "vscode": {
@@ -182,13 +184,15 @@
     "wff(and(A,B)) --> \"(\", wff(A), \"∧\", wff(B), \")\".\n",
     "wff(or(A,B)) --> \"(\", wff(A), \"∨\", wff(B), \")\".\n",
     "wff(impl(A,B)) --> \"(\", wff(A), \"⇒\", wff(B), \")\".\n",
-    "wff(equiv(A,B)) --> \"(\", wff(A), \"⟺\", wff(B), \")\"."
+    "wff(equiv(A,B)) --> \"(\", wff(A), \"⟺\", wff(B), \")\".\n",
+    "\n",
+    "parse_wff(String,Formula) :- wff(Formula,String,\"\")."
    ]
   },
   {
    "cell_type": "code",
-   "execution_count": 7,
-   "id": "8ddb568d",
+   "execution_count": 65,
+   "id": "6b9c3364",
    "metadata": {
     "vscode": {
      "languageId": "prolog"
@@ -206,12 +210,12 @@
     }
    ],
    "source": [
-    "?- wff(Formula,\"(¬p)\",\"\")."
+    "?- parse_wff(\"(¬p)\",Formula)."
    ]
   },
   {
    "cell_type": "code",
-   "execution_count": 8,
+   "execution_count": 66,
    "id": "075dc3b2",
    "metadata": {
     "vscode": {
@@ -230,12 +234,12 @@
     }
    ],
    "source": [
-    "?- wff(Formula,\"(¬(p∧q))\",\"\")."
+    "?- parse_wff(\"(¬(p∧q))\",Formula)."
    ]
   },
   {
    "cell_type": "code",
-   "execution_count": 9,
+   "execution_count": 67,
    "id": "338cb7dd",
    "metadata": {
     "vscode": {
@@ -254,7 +258,7 @@
     }
    ],
    "source": [
-    "?- wff(Formula,\"(p∧(q∨(¬p)))\",\"\")."
+    "?- parse_wff(\"(p∧(q∨(¬p)))\",Formula)."
    ]
   },
   {
@@ -648,6 +652,39 @@
     "?- value(and(p,or(q,not(p))), [p/true, q/false],Res)."
    ]
   },
+  {
+   "cell_type": "markdown",
+   "id": "f3c2de52",
+   "metadata": {},
+   "source": [
+    "We can also use our parser instead of writing the logical formulas as Prolog terms:"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 68,
+   "id": "575fc20f",
+   "metadata": {
+    "vscode": {
+     "languageId": "prolog"
+    }
+   },
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "\u001b[1mFormula = and(p,or(q,not(p))),\n",
+       "Res = false"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    }
+   ],
+   "source": [
+    "?- parse_wff(\"(p∧(q∨(¬p)))\",Formula), value(Formula, [p/true,q/false],Res)."
+   ]
+  },
   {
    "cell_type": "markdown",
    "id": "4387b4a2",
@@ -1890,7 +1927,7 @@
   {
    "cell_type": "code",
    "execution_count": null,
-   "id": "79db3ffb",
+   "id": "0fd61d87",
    "metadata": {
     "vscode": {
      "languageId": "prolog"
-- 
GitLab