First version of Prolog lecture 3

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

logic_programming/3_PropositionalLogic.ipynb

+{
+ "cells": [
+  {
+   "cell_type": "markdown",
+   "id": "9eb5530a",
+   "metadata": {},
+   "source": [
+    "# Propositional Logic\n",
+    "Syntax and Semantics Explained using a Prolog Implementation"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "dba70591",
+   "metadata": {},
+   "source": [
+    "## Well-Formed Formulas (WFF)\n",
+    "\n",
+    "All atomic propositions are WFF)\n",
+    "If a und b are WFF then so are:\n",
+    "- (¬ a)\n",
+    "- (a ∧ b)\n",
+    "- (a ∨ b)\n",
+    "- (a ⇒ b)\n",
+    "- (a ⟺ b)\n",
+    "No other formulas are WFF.\n",
+    "\n",
+    "Comment: a, b are metavariablens outside the syntax of propositional logic.\n"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "dd01f86a",
+   "metadata": {},
+   "source": [
+    "Maybe this reminds you of formal grammars from a theoretical computer science lecture.\n",
+    "And indeed, the above can be written as a grammar using a non-terminal symbol wff.\n",
+    "\n",
+    "In Prolog, grammars can actually be written using DCG notation, which we will see and understand much later in the course.\n",
+    "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",
+   "execution_count": 23,
+   "id": "964ebd52",
+   "metadata": {
+    "vscode": {
+     "languageId": "prolog"
+    }
+   },
+   "outputs": [
+    {
+     "data": {
+      "text/html": [
+       "\n",
+       "            <style>\n",
+       "            details  {\n",
+       "              font-family: Menlo, Consolas, 'DejaVu Sans Mono', monospace; font-size: 13px;\n",
+       "            }\n",
+       "\n",
+       "            details > summary {\n",
+       "              cursor: pointer;\n",
+       "            }\n",
+       "            </style>\n",
+       "            <details><summary>Previously defined clauses of user:wff/2 were retracted (click to expand)</summary><pre>:- dynamic wff/2.\n",
+       "\n",
+       "wff(A, B) :-\n",
+       "    A=[112|B].\n",
+       "wff(A, B) :-\n",
+       "    A=[113|B].\n",
+       "wff(A, B) :-\n",
+       "    A=[40, 172|C],\n",
+       "    wff(C, D),\n",
+       "    D=[41|B].\n",
+       "wff(A, B) :-\n",
+       "    A=[40|C],\n",
+       "    wff(C, D),\n",
+       "    D=[8743|E],\n",
+       "    wff(E, F),\n",
+       "    F=[41|B].\n",
+       "</pre></details>"
+      ],
+      "text/plain": [
+       "Previously defined clauses of user:wff/2 were retracted:\n",
+       ":- dynamic wff/2.\n",
+       "\n",
+       "wff(A, B) :-\n",
+       "    A=[112|B].\n",
+       "wff(A, B) :-\n",
+       "    A=[113|B].\n",
+       "wff(A, B) :-\n",
+       "    A=[40, 172|C],\n",
+       "    wff(C, D),\n",
+       "    D=[41|B].\n",
+       "wff(A, B) :-\n",
+       "    A=[40|C],\n",
+       "    wff(C, D),\n",
+       "    D=[8743|E],\n",
+       "    wff(E, F),\n",
+       "    F=[41|B].\n"
+      ]
+     },
+     "metadata": {
+      "application/json": {}
+     },
+     "output_type": "display_data"
+    },
+    {
+     "data": {
+      "text/plain": [
+       "% Asserting clauses for user:wff/2\n"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    }
+   ],
+   "source": [
+    " :- set_prolog_flag(double_quotes, codes).\n",
+    "wff --> \"p\". % atomic proposition\n",
+    "wff --> \"q\". % atomic proposition\n",
+    "wff --> \"(¬\",wff,\")\".\n",
+    "wff --> \"(\", wff, \"∧\", wff, \")\".\n",
+    "wff --> \"(\", wff, \"∨\", wff, \")\".\n",
+    "wff --> \"(\", wff, \"⇒\", wff, \")\".\n",
+    "wff --> \"(\", wff, \"⟺\", wff, \")\"."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 17,
+   "id": "fc6823ad",
+   "metadata": {
+    "vscode": {
+     "languageId": "prolog"
+    }
+   },
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "\u001b[1mtrue"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    }
+   ],
+   "source": [
+    "?- wff(\"p\",\"\")."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 18,
+   "id": "152289b6",
+   "metadata": {
+    "vscode": {
+     "languageId": "prolog"
+    }
+   },
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "\u001b[1mtrue"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    }
+   ],
+   "source": [
+    "?- wff(\"(¬p)\",\"\")."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 29,
+   "id": "2c3dd1bf",
+   "metadata": {
+    "vscode": {
+     "languageId": "prolog"
+    }
+   },
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "\u001b[1mtrue"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    }
+   ],
+   "source": [
+    "?- wff(\"(p∧(q∨(¬p)))\",\"\").\n",
+    "%comment."
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "92b6dc2d",
+   "metadata": {},
+   "source": [
+    "We will also see much later that Prolog allows one to annotate grammars with semantic values, here to generate\n",
+    "a Prolog term representing the logical formal in the form of a syntax tree:"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 24,
+   "id": "78163b60",
+   "metadata": {
+    "vscode": {
+     "languageId": "prolog"
+    }
+   },
+   "outputs": [
+    {
+     "data": {
+      "text/html": [
+       "\n",
+       "            <style>\n",
+       "            details  {\n",
+       "              font-family: Menlo, Consolas, 'DejaVu Sans Mono', monospace; font-size: 13px;\n",
+       "            }\n",
+       "\n",
+       "            details > summary {\n",
+       "              cursor: pointer;\n",
+       "            }\n",
+       "            </style>\n",
+       "            <details><summary>Previously defined clauses of user:wff/3 were retracted (click to expand)</summary><pre>:- dynamic wff/3.\n",
+       "\n",
+       "wff(p, [112|A], A).\n",
+       "wff(q, A, B) :-\n",
+       "    A=[113|B].\n",
+       "wff(not(A), B, C) :-\n",
+       "    B=[40, 172|D],\n",
+       "    wff(A, D, E),\n",
+       "    E=[41|C].\n",
+       "wff(and(A, B), C, D) :-\n",
+       "    C=[40|E],\n",
+       "    wff(A, E, F),\n",
+       "    F=[8743|G],\n",
+       "    wff(B, G, H),\n",
+       "    H=[41|D].\n",
+       "</pre></details>"
+      ],
+      "text/plain": [
+       "Previously defined clauses of user:wff/3 were retracted:\n",
+       ":- dynamic wff/3.\n",
+       "\n",
+       "wff(p, [112|A], A).\n",
+       "wff(q, A, B) :-\n",
+       "    A=[113|B].\n",
+       "wff(not(A), B, C) :-\n",
+       "    B=[40, 172|D],\n",
+       "    wff(A, D, E),\n",
+       "    E=[41|C].\n",
+       "wff(and(A, B), C, D) :-\n",
+       "    C=[40|E],\n",
+       "    wff(A, E, F),\n",
+       "    F=[8743|G],\n",
+       "    wff(B, G, H),\n",
+       "    H=[41|D].\n"
+      ]
+     },
+     "metadata": {
+      "application/json": {}
+     },
+     "output_type": "display_data"
+    },
+    {
+     "data": {
+      "text/plain": [
+       "% Asserting clauses for user:wff/3\n"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    }
+   ],
+   "source": [
+    " :- set_prolog_flag(double_quotes, codes).\n",
+    "wff(p) --> \"p\". % atomic proposition\n",
+    "wff(q) --> \"q\". % atomic proposition\n",
+    "wff(not(A)) --> \"(¬\",wff(A),\")\".\n",
+    "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), \")\"."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 25,
+   "id": "8ddb568d",
+   "metadata": {
+    "vscode": {
+     "languageId": "prolog"
+    }
+   },
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "\u001b[1mFormula = not(p)"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    }
+   ],
+   "source": [
+    "?- wff(Formula,\"(¬p)\",\"\")."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 26,
+   "id": "075dc3b2",
+   "metadata": {
+    "vscode": {
+     "languageId": "prolog"
+    }
+   },
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "\u001b[1mFormula = not(and(p,q))"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    }
+   ],
+   "source": [
+    "?- wff(Formula,\"(¬(p∧q))\",\"\")."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 28,
+   "id": "338cb7dd",
+   "metadata": {
+    "vscode": {
+     "languageId": "prolog"
+    }
+   },
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "\u001b[1mFormula = and(p,or(q,not(p)))"
+      ]
+     },
+     "metadata": {},
+     "output_type": "display_data"
+    }
+   ],
+   "source": [
+    "?- wff(Formula,\"(p∧(q∨(¬p)))\",\"\")."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "id": "f6116612",
+   "metadata": {
+    "vscode": {
+     "languageId": "prolog"
+    }
+   },
+   "outputs": [],
+   "source": []
+  }
+ ],
+ "metadata": {
+  "kernelspec": {
+   "display_name": "Prolog",
+   "language": "prolog",
+   "name": "prolog_kernel"
+  },
+  "language_info": {
+   "codemirror_mode": "prolog",
+   "file_extension": ".pl",
+   "mimetype": "text/x-prolog",
+   "name": "Prolog"
+  }
+ },
+ "nbformat": 4,
+ "nbformat_minor": 5
+}