diff --git a/logic_programming/3_PropositionalLogic.ipynb b/logic_programming/3_PropositionalLogic.ipynb new file mode 100644 index 0000000000000000000000000000000000000000..1d7bf85f5f534d9fad82f9e2ca327008d2e24b3f --- /dev/null +++ b/logic_programming/3_PropositionalLogic.ipynb @@ -0,0 +1,397 @@ +{ + "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 +}