add more material about propositional logic

Signed-off-by: Michael Leuschel <leuschel@uni-duesseldorf.de>

add more material about propositional logic
b496aad0 · Michael Leuschel · de95161a · b496aad0
Commit b496aad0 authored Oct 24, 2022 by Michael Leuschel
--- 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": [
+   "outputs": [],
-    {
-     "data": {
-      "text/plain": [
-       "\u001b[1;31m% The Prolog server was restarted"
-      ]
-     },
-     "metadata": {},
-     "output_type": "display_data"
-    }
-   ],
   "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",
+    "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`."
+    "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": []
  }

 %% Cell type:markdown id:9eb5530a tags:
 # Propositional Logic
 Syntax and Semantics Explained using a Prolog Implementation
 %% Cell type:markdown id:dba70591 tags:
 ## Well-Formed Formulas (WFF)
 All atomic propositions are WFF)
 If a und b are WFF then so are:
 - (¬ a)
 - (a ∧ b)
 - (a ∨ b)
 - (a ⇒ b)
 - (a ⟺ b)
 No other formulas are WFF.
 Comment: a, b are metavariablens outside the syntax of propositional logic.
 %% Cell type:markdown id:dd01f86a tags:
 Maybe this reminds you of formal grammars from a theoretical computer science lecture.
 And indeed, the above can be written as a grammar using a non-terminal symbol wff.
 In Prolog, grammars can actually be written using DCG notation, which we will see and understand much later in the course.
 Here we simply write the grammar in Prolog style and can then use it to check if a formula is a WFF:
 %% Cell type:code id:964ebd52 tags:
 ``` prolog
 :- set_prolog_flag(double_quotes, codes).
 wff --> "p". % atomic proposition
 wff --> "q". % atomic proposition
 wff --> "(¬",wff,")".
 wff --> "(", wff, "∧", wff, ")".
 wff --> "(", wff, "∨", wff, ")".
 wff --> "(", wff, "⇒", wff, ")".
 wff --> "(", wff, "⟺", wff, ")".
 ```
-%% Output
 %% Cell type:code id:fc6823ad tags:
 ``` prolog
 ?- wff("p","").
 ```
 %% Output
 %% Cell type:code id:152289b6 tags:
 ``` prolog
 ?- wff("(¬p)","").
 ```
 %% Output
 %% Cell type:code id:2c3dd1bf tags:
 ``` prolog
 ?- wff("(p∧(q∨(¬p)))","").
 %comment.
 ```
 %% Output
 %% Cell type:markdown id:38b0a282 tags:
 This grammar does not talk about whitespace and requires parentheses for every connective used.
 In practice, one typically uses operator precedences to avoid having to write too many parentheses:
 - negation binds strongest
 - then come conjunction and disjunction
 - then come implication and equivalence.
 So instead of
 - (((¬ p) ∧ (¬ q)) ⇒ ((¬ p) ∨ (¬ q)))
 we can write
 - ¬ p ∧ ¬ q ⇒ ¬ p ∨ ¬ q
 We will try not not mix conjunction/disjunction and implication/equivalence without parentheses.
 We will also not try to improve our Prolog parser here to accomodate these precedences.
 This is the subject of another course (on compiler construction).
 %% Cell type:markdown id:92b6dc2d tags:
 We will also see much later that Prolog allows one to annotate grammars with semantic values, here to generate
 a Prolog term representing the logical formal in the form of a syntax tree:
 %% Cell type:code id:78163b60 tags:
 ``` prolog
 :- set_prolog_flag(double_quotes, codes).
 wff(p) --> "p". % atomic proposition
 wff(q) --> "q". % atomic proposition
 wff(not(A)) --> "(¬",wff(A),")".
 wff(and(A,B)) --> "(", wff(A), "∧", wff(B), ")".
 wff(or(A,B)) --> "(", wff(A), "∨", wff(B), ")".
 wff(impl(A,B)) --> "(", wff(A), "⇒", wff(B), ")".
 wff(equiv(A,B)) --> "(", wff(A), "⟺", wff(B), ")".
 ```
 %% Cell type:code id:8ddb568d tags:
 ``` prolog
 ?- wff(Formula,"(¬p)","").
 ```
 %% Output
 %% Cell type:code id:075dc3b2 tags:
 ``` prolog
 ?- wff(Formula,"(¬(p∧q))","").
 ```
 %% Output
 %% Cell type:code id:338cb7dd tags:
 ``` prolog
 ?- wff(Formula,"(p∧(q∨(¬p)))","").
 ```
 %% Output
 %% Cell type:markdown id:f9005519 tags:
 The above Prolog term `and(p,or(q,not(p)))` represents the logical formula in tree form.
 We can display the tree as a dag (directed acyclic graph) using the following subsidiary code
 (in future the Jupyter kernel will probably have a dedicated command to show a term graphically):
 %% Cell type:code id:f6116612 tags:
 ``` prolog
 subtree(Term,Nr,SubTerm) :-
   Term =.. [_|ArgList], %obtain arguments of the term
   nth1(Nr,ArgList,SubTerm). % get sub-argument and its position number
 % recursive and transitive closure of subtree
 rec_subtree(Term,Sub) :- Term = Sub.
 rec_subtree(Term,Sub) :- subtree(Term,_,X), rec_subtree(X,Sub).
 subnode(Sub,[shape/S, label/F],Formula) :-
   rec_subtree(Formula,Sub), % any sub-formula Sub of Formula is a node in the graphical rendering
   functor(Sub,F,_), (atom(Sub) -> S=egg ; number(Sub) -> S=oval ; S=rect).
 ```
 %% Cell type:code id:d7e68593 tags:
 ``` prolog
 jupyter:print_table(subnode(Node,Dot,and(p,or(q,not(p)))))
 ```
 %% Output
    Node | Dot |
    :- | :- |
    and(p,or(q,not(p))) | [shape/rect,label/and] |
    p | [shape/egg,label/p] |
    or(q,not(p)) | [shape/rect,label/or] |
    q | [shape/egg,label/q] |
    not(p) | [shape/rect,label/not] |
    p | [shape/egg,label/p] |
 %% Cell type:code id:3646e3ee tags:
 ``` prolog
 jupyter:show_graph(subnode(_,_,and(p,or(q,not(p)))),subtree/3)
 ```
 %% Output
 %% Cell type:markdown id:11b3a8ad tags:
 Below we will study how one can assign a truth-value to logical formulas like the one above.
 ## Truth tables
-Every logical connective has a truth-table, indicating how it maps the truth of its arguments to its own truth value.
+Every logical connective has a truth table, indicating how it maps the truth of its arguments to its own truth value.
 For example, `and` maps inputs `true` and `false` to `false`.
+Below we encode the truth table for five connectives as Prolog facts and rules.
 %% Cell type:code id:350b9756 tags:
 ``` prolog
 not(true,false).
 not(false,true).
 and(true,V,V) :- truth_value(V).
-and(false,_,false).
+and(false,V,false) :- truth_value(V).
-or(true,_,true).
+or(true,V,true) :- truth_value(V).
 or(false,V,V) :- truth_value(V).
 implies(A,B,Res) :- not(A,NotA), or(NotA,B,Res).
 equiv(A,B,Res) :- implies(A,B,AiB), implies(B,A,BiA), and(AiB,BiA,Res).
 truth_value(true).
 truth_value(false).
 truth_table(A,B,NotA,AandB,AorB,AiB,AeB) :-
   truth_value(A), truth_value(B),
   not(A,NotA), and(A,B,AandB), or(A,B,AorB),
   implies(A,B,AiB), equiv(A,B,AeB).
 ```
+%% Cell type:markdown id:41cad0bc tags:
+We can now use the predicates `and/3`, ... to compute the truth value of the connectives for a particular input:
+%% Cell type:code id:3101448b tags:
+``` prolog
+?- and(true,false,X).
+```
+%% Output
+%% Cell type:code id:922004e9 tags:
+``` prolog
+?- or(true,false,X).
+```
+%% Output
+%% Cell type:markdown id:78c0eda3 tags:
+We can also display the whole truth table using a Jupyter command:
 %% Cell type:code id:54b57ff8 tags:
 ``` prolog
 jupyter:print_table(truth_table(A,B,NotA,AandB,AorB,AimpliesB,AequivB))
 ```
 %% Output
    A | B | NotA | AandB | AorB | AimpliesB | AequivB |
    :- | :- | :- | :- | :- | :- | :- |
    true | true | false | true | true | true | true |
    true | false | false | false | true | false | false |
    false | true | true | false | true | true | false |
    false | false | true | false | false | true | true |
+%% Cell type:markdown id:ce32b1d0 tags:
+An <b>interpretation</b> is an assignment of all relevant proposition to truth values (true or false).
+For example, given the formula `(p∧(q∨(¬p)))` an interpretation needs to assign a truth value to `p` and `q`.
+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`.
+For example, one of the four possible interpretations for the formula above is `[p/true, q/false]`.
+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 id:8f6d804b tags:
+``` prolog
+?- Interpetation=[p/true, q/false],  member(q/Q,Interpetation).
+```
+%% Output
+%% Cell type:markdown id:0d236e48 tags:
+Given an interpretation we can now compute the truth value for an entire formula in a recursive fashion.
+For propositions we look up the truth value in the interpretation (done using `member` below).
+For logical connectives we recursively compute the truth value of its arguments and then apply the truth tables we defined above.
 %% Cell type:code id:175c00d0 tags:
 ``` prolog
 value(X,Interpretation,Value) :-
-   atomic(X), % we could also use: proposition(X),
+   atomic(X), % we have a proposition
   member(X/Value,Interpretation).
 value(and(A,B),I,Val) :- value(A,I,VA), value(B,I,VB),
   and(VA,VB,Val).
 value(or(A,B),I,Val) :- value(A,I,VA), value(B,I,VB),
   or(VA,VB,Val).
 value(not(A),I,Val) :- value(A,I,VA),
   not(VA,Val).
 value(implies(A,B),I,Val) :- value(or(not(A),B),I,Val).
 value(equiv(A,B),I,Val) :-
   value(and(implies(A,B),implies(B,A)),I,Val).
 ```
+%% Cell type:markdown id:aa50ec0e tags:
+Using the above we can compute the truth value of `(p∧(q∨(¬p)))` for the interpretation `[p/true, q/false]`:
 %% Cell type:code id:eee17774 tags:
 ``` prolog
 ?- value(and(p,or(q,not(p))), [p/true, q/false],Res).
 ```
 %% Output
+%% Cell type:markdown id:4387b4a2 tags:
+The truth value of `(p∧(q∨(¬p)))` for the interpretation `[p/true, q/true]` is true.
+In this case the interpretation is called a <b>model</b> of the formula.
+%% Cell type:code id:fec75f65 tags:
+``` prolog
+?- value(and(p,or(q,not(p))), [p/true, q/true],Res).
+```
+%% Output
+%% Cell type:markdown id:3aa46665 tags:
+We can also compute the truth table of the entire formula, by trying out all possible interpretations.
+Below we leave P and Q as Prolog variable which is instantiated by the code above:
 %% Cell type:code id:78473da0 tags:
 ``` prolog
 jupyter:print_table(value(and(p,or(q,not(p))), [p/P, q/Q],Res))
 ```
 %% Output
    P | Q | Res |
    :- | :- | :- |
    true | true | true |
    true | false | false |
    false | true | false |
    false | false | false |
+%% Cell type:markdown id:5b4ee42b tags:
+Below we visualise graphically this computation, by displaying the syntax tree of a logical formula
+as a dag and by colouring the nodes using the `value` predicate:
 %% Cell type:code id:2ee60c15 tags:
 ``` prolog
 subnode_val(Sub,[shape/S, label/F, style/filled, fillcolor/C],Formula,Interpretation) :-
   rec_subtree(Formula,Sub), % any sub-formula Sub of Formula is a node in the graphical rendering
   functor(Sub,F,_), (atom(Sub) -> S=egg ; number(Sub) -> S=oval ; S=rect),
   (value(Sub,Interpretation,true) -> C=olive ; C=sienna1).
 ```
 %% Cell type:code id:2b497dad tags:
 ``` prolog
 jupyter:show_graph(subnode_val(_,_,and(p,or(q,not(p))),[p/true,q/false]),subtree/3)
 ```
 %% Output
 %% Cell type:code id:0fd23f05 tags:
 ``` prolog
 jupyter:show_graph(subnode_val(_,_,and(p,or(q,not(p))),[p/true,q/true]),subtree/3)
 ```
 %% Output
+%% Cell type:markdown id:013fda69 tags:
+A formula for which all interpretations are models is called a <b>tautology</b>:
 %% Cell type:code id:23775624 tags:
 ``` prolog
-?- use_module(library(clpfd)).
+jupyter:print_table(value(or(p,not(p)), [p/P],Res))
 ```
 %% Output
+    P | Res |
+    :- | :- |
+    true | true |
+    false | true |
 %% Cell type:code id:7a6e29ed tags:
 ``` prolog
+jupyter:print_table(value(or(p,or(q,not(q))), [p/P, q/Q],Res))
+```
+%% Output
+    P | Q | Res |
+    :- | :- | :- |
+    true | true | true |
+    false | true | true |
+    true | false | true |
+    false | false | true |
+%% Cell type:markdown id:9ff1936a tags:
+A formula which has no models is called a <b>contradiction</b>:
+%% Cell type:code id:6bd292f4 tags:
+``` prolog
+jupyter:print_table(value(and(p,not(p)), [p/P],Res))
+```
+%% Output
+    P | Res |
+    :- | :- |
+    true | false |
+    false | false |
+%% Cell type:markdown id:fc920c04 tags:
+A formula which has at least one model is called <b>satisfiable</b>.
+Two formulas are called <b>equivalent</b> iff they have the same models:
+%% Cell type:code id:b912acd3 tags:
+``` prolog
+jupyter:print_table(value(or(not(p),q), [p/P, q/Q],Res))
+```
+%% Output
+    P | Q | Res |
+    :- | :- | :- |
+    true | true | true |
+    true | false | false |
+    false | true | true |
+    false | false | true |
+%% Cell type:code id:f4c9823d tags:
+``` prolog
+jupyter:print_table(value(implies(p,q), [p/P, q/Q],Res))
+```
+%% Output
+    P | Q | Res |
+    :- | :- | :- |
+    true | true | true |
+    true | false | false |
+    false | true | true |
+    false | false | true |
+%% Cell type:code id:aaf46953 tags:
+``` prolog
 ```