From b496aad0086b0b41f36d3b2f06523d1ed1d5dd55 Mon Sep 17 00:00:00 2001
From: Michael Leuschel <leuschel@uni-duesseldorf.de>
Date: Mon, 24 Oct 2022 18:59:34 +0200
Subject: [PATCH] add more material about propositional logic

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

diff --git a/logic_programming/3_PropositionalLogic.ipynb b/logic_programming/3_PropositionalLogic.ipynb
index 8d09732..c3a594f 100644
--- a/logic_programming/3_PropositionalLogic.ipynb
+++ b/logic_programming/3_PropositionalLogic.ipynb
@@ -42,24 +42,14 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 11,
+   "execution_count": 34,
    "id": "964ebd52",
    "metadata": {
     "vscode": {
      "languageId": "prolog"
     }
    },
-   "outputs": [
-    {
-     "data": {
-      "text/plain": [
-       "\u001b[1;31m% The Prolog server was restarted"
-      ]
-     },
-     "metadata": {},
-     "output_type": "display_data"
-    }
-   ],
+   "outputs": [],
    "source": [
     " :- set_prolog_flag(double_quotes, codes).\n",
     "wff --> \"p\". % atomic proposition\n",
@@ -73,7 +63,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 12,
+   "execution_count": 35,
    "id": "fc6823ad",
    "metadata": {
     "vscode": {
@@ -97,7 +87,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 13,
+   "execution_count": 36,
    "id": "152289b6",
    "metadata": {
     "vscode": {
@@ -121,7 +111,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 14,
+   "execution_count": 37,
    "id": "2c3dd1bf",
    "metadata": {
     "vscode": {
@@ -176,7 +166,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 15,
+   "execution_count": 38,
    "id": "78163b60",
    "metadata": {
     "vscode": {
@@ -197,7 +187,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 16,
+   "execution_count": 39,
    "id": "8ddb568d",
    "metadata": {
     "vscode": {
@@ -221,7 +211,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 17,
+   "execution_count": 40,
    "id": "075dc3b2",
    "metadata": {
     "vscode": {
@@ -245,7 +235,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 18,
+   "execution_count": 41,
    "id": "338cb7dd",
    "metadata": {
     "vscode": {
@@ -279,7 +269,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 19,
+   "execution_count": 42,
    "id": "f6116612",
    "metadata": {
     "vscode": {
@@ -303,7 +293,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 20,
+   "execution_count": 43,
    "id": "d7e68593",
    "metadata": {
     "vscode": {
@@ -353,7 +343,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 21,
+   "execution_count": 44,
    "id": "3646e3ee",
    "metadata": {
     "vscode": {
@@ -405,13 +395,15 @@
     "\n",
     "## Truth tables\n",
     "\n",
-    "Every logical connective has a truth-table, indicating how it maps the truth of its arguments to its own truth value.\n",
-    "For example, `and` maps inputs `true` and `false` to `false`."
+    "Every logical connective has a truth table, indicating how it maps the truth of its arguments to its own truth value.\n",
+    "For example, `and` maps inputs `true` and `false` to `false`.\n",
+    "\n",
+    "Below we encode the truth table for five connectives as Prolog facts and rules."
    ]
   },
   {
    "cell_type": "code",
-   "execution_count": 22,
+   "execution_count": 45,
    "id": "350b9756",
    "metadata": {
     "vscode": {
@@ -424,9 +416,9 @@
     "not(false,true).\n",
     "\n",
     "and(true,V,V) :- truth_value(V).\n",
-    "and(false,_,false).\n",
+    "and(false,V,false) :- truth_value(V).\n",
     "\n",
-    "or(true,_,true).\n",
+    "or(true,V,true) :- truth_value(V).\n",
     "or(false,V,V) :- truth_value(V).\n",
     "\n",
     "implies(A,B,Res) :- not(A,NotA), or(NotA,B,Res).\n",
@@ -441,9 +433,73 @@
     "   implies(A,B,AiB), equiv(A,B,AeB)."
    ]
   },
+  {
+   "cell_type": "markdown",
+   "id": "41cad0bc",
+   "metadata": {},
+   "source": [
+    "We can now use the predicates `and/3`, ... to compute the truth value of the connectives for a particular input:"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 46,
+   "id": "3101448b",
+   "metadata": {
+    "vscode": {
+     "languageId": "prolog"
+    }
+   },
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "\u001b[1mX = false"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    }
+   ],
+   "source": [
+    "?- and(true,false,X)."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 47,
+   "id": "922004e9",
+   "metadata": {
+    "vscode": {
+     "languageId": "prolog"
+    }
+   },
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "\u001b[1mX = true"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    }
+   ],
+   "source": [
+    "?- or(true,false,X)."
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "78c0eda3",
+   "metadata": {},
+   "source": [
+    "We can also display the whole truth table using a Jupyter command:"
+   ]
+  },
   {
    "cell_type": "code",
-   "execution_count": 23,
+   "execution_count": 48,
    "id": "54b57ff8",
    "metadata": {
     "vscode": {
@@ -487,9 +543,57 @@
     "jupyter:print_table(truth_table(A,B,NotA,AandB,AorB,AimpliesB,AequivB))"
    ]
   },
+  {
+   "cell_type": "markdown",
+   "id": "ce32b1d0",
+   "metadata": {},
+   "source": [
+    "An <b>interpretation</b> is an assignment of all relevant proposition to truth values (true or false).\n",
+    "For example, given the formula `(p∧(q∨(¬p)))` an interpretation needs to assign a truth value to `p` and `q`.\n",
+    "In the Prolog code below we will represent an interpretation as a list of bindings, each binding is a term of the form `Proposition/TruthValue`.\n",
+    "For example, one of the four possible interpretations for the formula above is `[p/true, q/false]`.\n",
+    "\n",
+    "Using the built-in `member/2` predicate we can inspect an interpretation in Prolog. For example, here we retrieve the truth value of `q`:"
+   ]
+  },
   {
    "cell_type": "code",
-   "execution_count": 24,
+   "execution_count": 49,
+   "id": "8f6d804b",
+   "metadata": {
+    "vscode": {
+     "languageId": "prolog"
+    }
+   },
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "\u001b[1mInterpetation = [p/true,q/false],\n",
+       "Q = false"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    }
+   ],
+   "source": [
+    "?- Interpetation=[p/true, q/false],  member(q/Q,Interpetation)."
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "0d236e48",
+   "metadata": {},
+   "source": [
+    "Given an interpretation we can now compute the truth value for an entire formula in a recursive fashion.\n",
+    "For propositions we look up the truth value in the interpretation (done using `member` below).\n",
+    "For logical connectives we recursively compute the truth value of its arguments and then apply the truth tables we defined above."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 50,
    "id": "175c00d0",
    "metadata": {
     "vscode": {
@@ -499,7 +603,7 @@
    "outputs": [],
    "source": [
     "value(X,Interpretation,Value) :- \n",
-    "   atomic(X), % we could also use: proposition(X),\n",
+    "   atomic(X), % we have a proposition\n",
     "   member(X/Value,Interpretation).\n",
     "value(and(A,B),I,Val) :- value(A,I,VA), value(B,I,VB),\n",
     "   and(VA,VB,Val).\n",
@@ -512,9 +616,17 @@
     "   value(and(implies(A,B),implies(B,A)),I,Val).\n"
    ]
   },
+  {
+   "cell_type": "markdown",
+   "id": "aa50ec0e",
+   "metadata": {},
+   "source": [
+    "Using the above we can compute the truth value of `(p∧(q∨(¬p)))` for the interpretation `[p/true, q/false]`:"
+   ]
+  },
   {
    "cell_type": "code",
-   "execution_count": 25,
+   "execution_count": 51,
    "id": "eee17774",
    "metadata": {
     "vscode": {
@@ -536,9 +648,51 @@
     "?- value(and(p,or(q,not(p))), [p/true, q/false],Res)."
    ]
   },
+  {
+   "cell_type": "markdown",
+   "id": "4387b4a2",
+   "metadata": {},
+   "source": [
+    "The truth value of `(p∧(q∨(¬p)))` for the interpretation `[p/true, q/true]` is true.\n",
+    "In this case the interpretation is called a <b>model</b> of the formula."
+   ]
+  },
   {
    "cell_type": "code",
-   "execution_count": 26,
+   "execution_count": 52,
+   "id": "fec75f65",
+   "metadata": {
+    "vscode": {
+     "languageId": "prolog"
+    }
+   },
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "\u001b[1mRes = true"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    }
+   ],
+   "source": [
+    "?- value(and(p,or(q,not(p))), [p/true, q/true],Res)."
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "3aa46665",
+   "metadata": {},
+   "source": [
+    "We can also compute the truth table of the entire formula, by trying out all possible interpretations.\n",
+    "Below we leave P and Q as Prolog variable which is instantiated by the code above:"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 53,
    "id": "78473da0",
    "metadata": {
     "vscode": {
@@ -582,9 +736,18 @@
     "jupyter:print_table(value(and(p,or(q,not(p))), [p/P, q/Q],Res))"
    ]
   },
+  {
+   "cell_type": "markdown",
+   "id": "5b4ee42b",
+   "metadata": {},
+   "source": [
+    "Below we visualise graphically this computation, by displaying the syntax tree of a logical formula\n",
+    "as a dag and by colouring the nodes using the `value` predicate:"
+   ]
+  },
   {
    "cell_type": "code",
-   "execution_count": 27,
+   "execution_count": 54,
    "id": "2ee60c15",
    "metadata": {
     "vscode": {
@@ -602,7 +765,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 28,
+   "execution_count": 55,
    "id": "2b497dad",
    "metadata": {
     "vscode": {
@@ -647,7 +810,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 29,
+   "execution_count": 56,
    "id": "0fd23f05",
    "metadata": {
     "vscode": {
@@ -690,9 +853,17 @@
     "jupyter:show_graph(subnode_val(_,_,and(p,or(q,not(p))),[p/true,q/true]),subtree/3)"
    ]
   },
+  {
+   "cell_type": "markdown",
+   "id": "013fda69",
+   "metadata": {},
+   "source": [
+    "A formula for which all interpretations are models is called a <b>tautology</b>:"
+   ]
+  },
   {
    "cell_type": "code",
-   "execution_count": 30,
+   "execution_count": 57,
    "id": "23775624",
    "metadata": {
     "vscode": {
@@ -700,6 +871,24 @@
     }
    },
    "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "P | Res | \n",
+       ":- | :- | \n",
+       "true | true | \n",
+       "false | true | "
+      ],
+      "text/plain": [
+       "P | Res | \n",
+       ":- | :- | \n",
+       "true | true | \n",
+       "false | true | "
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    },
     {
      "data": {
       "text/plain": [
@@ -711,18 +900,219 @@
     }
    ],
    "source": [
-    "?- use_module(library(clpfd))."
+    "jupyter:print_table(value(or(p,not(p)), [p/P],Res))"
    ]
   },
   {
    "cell_type": "code",
-   "execution_count": null,
+   "execution_count": 58,
    "id": "7a6e29ed",
    "metadata": {
     "vscode": {
      "languageId": "prolog"
     }
    },
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "P | Q | Res | \n",
+       ":- | :- | :- | \n",
+       "true | true | true | \n",
+       "false | true | true | \n",
+       "true | false | true | \n",
+       "false | false | true | "
+      ],
+      "text/plain": [
+       "P | Q | Res | \n",
+       ":- | :- | :- | \n",
+       "true | true | true | \n",
+       "false | true | true | \n",
+       "true | false | true | \n",
+       "false | false | true | "
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    },
+    {
+     "data": {
+      "text/plain": [
+       "\u001b[1mtrue"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    }
+   ],
+   "source": [
+    "jupyter:print_table(value(or(p,or(q,not(q))), [p/P, q/Q],Res))"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "9ff1936a",
+   "metadata": {},
+   "source": [
+    "A formula which has no models is called a <b>contradiction</b>:"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 59,
+   "id": "6bd292f4",
+   "metadata": {
+    "vscode": {
+     "languageId": "prolog"
+    }
+   },
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "P | Res | \n",
+       ":- | :- | \n",
+       "true | false | \n",
+       "false | false | "
+      ],
+      "text/plain": [
+       "P | Res | \n",
+       ":- | :- | \n",
+       "true | false | \n",
+       "false | false | "
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    },
+    {
+     "data": {
+      "text/plain": [
+       "\u001b[1mtrue"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    }
+   ],
+   "source": [
+    "jupyter:print_table(value(and(p,not(p)), [p/P],Res))"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "fc920c04",
+   "metadata": {
+    "vscode": {
+     "languageId": "prolog"
+    }
+   },
+   "source": [
+    "A formula which has at least one model is called <b>satisfiable</b>.\n",
+    "Two formulas are called <b>equivalent</b> iff they have the same models:"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 60,
+   "id": "b912acd3",
+   "metadata": {
+    "vscode": {
+     "languageId": "prolog"
+    }
+   },
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "P | Q | Res | \n",
+       ":- | :- | :- | \n",
+       "true | true | true | \n",
+       "true | false | false | \n",
+       "false | true | true | \n",
+       "false | false | true | "
+      ],
+      "text/plain": [
+       "P | Q | Res | \n",
+       ":- | :- | :- | \n",
+       "true | true | true | \n",
+       "true | false | false | \n",
+       "false | true | true | \n",
+       "false | false | true | "
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    },
+    {
+     "data": {
+      "text/plain": [
+       "\u001b[1mtrue"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    }
+   ],
+   "source": [
+    "jupyter:print_table(value(or(not(p),q), [p/P, q/Q],Res))"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 61,
+   "id": "f4c9823d",
+   "metadata": {
+    "vscode": {
+     "languageId": "prolog"
+    }
+   },
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "P | Q | Res | \n",
+       ":- | :- | :- | \n",
+       "true | true | true | \n",
+       "true | false | false | \n",
+       "false | true | true | \n",
+       "false | false | true | "
+      ],
+      "text/plain": [
+       "P | Q | Res | \n",
+       ":- | :- | :- | \n",
+       "true | true | true | \n",
+       "true | false | false | \n",
+       "false | true | true | \n",
+       "false | false | true | "
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    },
+    {
+     "data": {
+      "text/plain": [
+       "\u001b[1mtrue"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    }
+   ],
+   "source": [
+    "jupyter:print_table(value(implies(p,q), [p/P, q/Q],Res))"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "id": "aaf46953",
+   "metadata": {
+    "vscode": {
+     "languageId": "prolog"
+    }
+   },
    "outputs": [],
    "source": []
   }
-- 
GitLab