From 72538c53331be50a3180ac4bf7fb787c7d59c7d5 Mon Sep 17 00:00:00 2001
From: dgelessus <dgelessus@users.noreply.github.com>
Date: Mon, 3 Apr 2023 16:41:06 +0200
Subject: [PATCH] Minor updates to Logik.ipynb

---
 info4/kapitel-0/Logik.ipynb | 466 +++++++++++++++++-------------------
 1 file changed, 221 insertions(+), 245 deletions(-)

diff --git a/info4/kapitel-0/Logik.ipynb b/info4/kapitel-0/Logik.ipynb
index f687b42..611dc2c 100644
--- a/info4/kapitel-0/Logik.ipynb
+++ b/info4/kapitel-0/Logik.ipynb
@@ -6,7 +6,7 @@
    "source": [
     "# Theoretische Informatik - Vorlesung 0 - Teil 1 Logik\n",
     "\n",
-    "* April 2020\n",
+    "* April 2023\n",
     "* Michael Leuschel\n",
     "* Lehrstuhl Softwaretechnik und Programmiersprachen\n",
     "* Heinrich-Heine Universität Düsseldorf\n",
@@ -15,7 +15,7 @@
     "Hier definieren wir einige Grundlagen und Notationen, die im Skript verwendet werden.\n",
     "Ein gutes Verständnis dieser Grundlagen und Notationen ist für das Verständnis des Skripts, aber auch anderer Teile der Informatik unumgänglich.\n",
     "\n",
-    "Die Folien für diese Grundlagen sind als Jupyter Notebooks erstellt worden und im [Gitlab der Informatik](https://gitlab.cs.uni-duesseldorf.de/general/stups/prob-teaching-notebooks) erhältlich.\n"
+    "Die Folien für diese Grundlagen sind als Jupyter Notebooks erstellt worden und im [GitLab der Informatik](https://gitlab.cs.uni-duesseldorf.de/general/stups/prob-teaching-notebooks) erhältlich."
    ]
   },
   {
@@ -46,8 +46,7 @@
     "* Stammt aus der Python-Community, in Python implementiert\n",
     "* ACM System Software Award 2017\n",
     "* Jupyter-Notebooks verschiedene Programmiersprachen verwenden\n",
-    " * Ein sprachspezifischer **Kernel** stellt die Sprache dem Jupyter Frontend zur Verfügung\n",
-    "    "
+    "    * Ein sprachspezifischer **Kernel** stellt die Sprache dem Jupyter Frontend zur Verfügung"
    ]
   },
   {
@@ -64,10 +63,10 @@
     "* Entwicklung am STUPS Lehrstuhl\n",
     "* Grundlage: Solver für Prädikatenlogik, Mengentheorie mit Relationen, Funktionen und Arithmetik.\n",
     "* Eignet sich aber auch für mathematische Ausführungen\n",
-    "* Der [ProB-Jupyter-Kernel](https://gitlab.cs.uni-duesseldorf.de/general/stups/prob2-jupyter-kernel) stellt die B Sprache und die mathematischen Grundlagen für Jupyter Notebooks zur Verfügung\n",
+    "* Der [ProB-Jupyter-Kernel](https://gitlab.cs.uni-duesseldorf.de/general/stups/prob2-jupyter-kernel) stellt die B-Sprache und die mathematischen Grundlagen für Jupyter Notebooks zur Verfügung\n",
     "\n",
     "\n",
-    "Um diese Notebooks zu starten kann man entweder selber Jupyter und den [ProB Kernel](https://gitlab.cs.uni-duesseldorf.de/general/stups/prob2-jupyter-kernel) installieren.\n",
+    "Um diese Notebooks zu starten kann man entweder selber Jupyter und den [ProB-Kernel](https://gitlab.cs.uni-duesseldorf.de/general/stups/prob2-jupyter-kernel) installieren.\n",
     "Man kann aber auch die Notebooks vom Browser aus mit Binder starten (das dauert besonders beim ersten Mal etwas länger):\n",
     "\n",
     "[![Binder](https://mybinder.org/badge_logo.svg)](https://mybinder.org/v2/git/https%3A%2F%2Fgitlab.cs.uni-duesseldorf.de%2Fgeneral%2Fstups%2Fprob-teaching-notebooks.git/HEAD?urlpath=%2Ftree%2Finfo4%2F)\n",
@@ -99,8 +98,9 @@
     "* Überlegungen über Programme: Verifikation, statische Programmanalyse, Programmoptimierung,...\n",
     "* Universale Vorrichtung zur Berechnung: Datenbanken, logische Programmierung, ...\n",
     "* Grundlage der Mathematik und auch der theoretischen Informatik\n",
-    " * Halpern et al. On the Unusual Effectiveness of Logic in Computer Science. https://www.cs.cmu.edu/~rwh/papers/unreasonable/basl.pdf\n",
-    " * Zitat aus diesem Artikel: ```The effectiveness of logic in computer science is not by any means limited to the areas mentioned in here. As a matter of fact, it spans a wide spectrum of areas, from artificial intelligence to software engineering. Overall, logic provides computer science with both a unifying foundational framework and a powerful tool for modeling and reasoning about aspects of computation.```"
+    "    * Halpern et al. On the Unusual Effectiveness of Logic in Computer Science. https://www.cs.cmu.edu/~rwh/papers/unreasonable/basl.pdf\n",
+    "    * Zitat aus diesem Artikel:\n",
+    "        > The effectiveness of logic in computer science is not by any means limited to the areas mentioned in here. As a matter of fact, it spans a wide spectrum of areas, from artificial intelligence to software engineering. Overall, logic provides computer science with both a unifying foundational framework and a powerful tool for modeling and reasoning about aspects of computation."
    ]
   },
   {
@@ -116,8 +116,8 @@
     "* Relevanzlogik, lineare Logik\n",
     "* eine nichtmonotone Logik\n",
     "\n",
-    " Wir werden die klassische, zweiwertige, monotone **Aussagenlogik**\n",
-    "  und **Prädikatenlogik** studieren (zusammen mit Mengentheorie)."
+    "Wir werden die klassische, zweiwertige, monotone **Aussagenlogik**\n",
+    "und **Prädikatenlogik** studieren (zusammen mit Mengentheorie)."
    ]
   },
   {
@@ -126,7 +126,7 @@
    "source": [
     "# Aussagenlogik\n",
     "\n",
-    "Eine Aussage ist endweder wahr (TRUE) oder falsch (FALSE).\n",
+    "Eine Aussage ist endweder wahr ($\\mathit{TRUE}$) oder falsch ($\\mathit{FALSE}$).\n",
     "Hier sind vier Aussagen:\n",
     "1. Siegfried ist ein Ritter\n",
     "2. Alle Ritter sagen die Wahrheit\n",
@@ -220,7 +220,7 @@
     "Jede Aussage ist auch eine Formel der Aussagenlogik.\n",
     "Mit den Junktoren kann man Aussagen und Formeln zu grösseren Formeln der Aussagenlogik kombinieren.\n",
     "\n",
-    "Die Negation ```¬(F)``` einer Formel F ist auch eine Formel. Die negierte Formel ist wahr genau dann wenn (gdw) die ursprünglihe Formel falsch ist:"
+    "Die Negation `¬(F)` einer Formel F ist auch eine Formel. Die negierte Formel ist wahr genau dann wenn (gdw) die ursprünglihe Formel falsch ist:"
    ]
   },
   {
@@ -280,7 +280,7 @@
    "cell_type": "markdown",
    "metadata": {},
    "source": [
-    "Die Konjunktion ```F ∧ G``` von zwei Formeln ist wahr gdw beide Formeln wahr sind:"
+    "Die Konjunktion `F ∧ G` von zwei Formeln ist wahr gdw beide Formeln wahr sind:"
    ]
   },
   {
@@ -333,7 +333,7 @@
    "cell_type": "markdown",
    "metadata": {},
    "source": [
-    "Die Disjunktion ```F ∨ G``` von zwei Formeln ist wahr gdw  mindestes eine der beiden Formeln wahr sind:"
+    "Die Disjunktion `F ∨ G` von zwei Formeln ist wahr gdw mindestes eine der beiden Formeln wahr sind:"
    ]
   },
   {
@@ -386,7 +386,7 @@
    "cell_type": "markdown",
    "metadata": {},
    "source": [
-    "Die Implikation ```F ⇒ G``` von zwei Formeln ist wahr wenn entweder beide Formeln wahr sind oder die erste Formel F falsch ist:"
+    "Die Implikation `F ⇒ G` von zwei Formeln ist wahr wenn entweder beide Formeln wahr sind oder die erste Formel F falsch ist:"
    ]
   },
   {
@@ -462,7 +462,7 @@
    "cell_type": "markdown",
    "metadata": {},
    "source": [
-    "Die Äquivalenz ```F ⇔ G``` von zwei Formeln ist wahr wenn entweder beide Formeln wahr sind oder beide Formeln falsch sind:"
+    "Die Äquivalenz `F ⇔ G` von zwei Formeln ist wahr wenn entweder beide Formeln wahr sind oder beide Formeln falsch sind:"
    ]
   },
   {
@@ -544,7 +544,7 @@
     "\n",
     "Die Formel $(p \\vee (\\neg p \\wedge q))$ steht also für $(p \\vee (\\neg(p) \\wedge q)$.\n",
     "\n",
-    "Eine Formel kann man immer als einen Baum sehen"
+    "Eine Formel kann man immer als einen Baum sehen."
    ]
   },
   {
@@ -578,14 +578,14 @@
        "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
        "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
        " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
-       "<!-- Generated by graphviz version 2.44.1 (0)\n",
+       "<!-- Generated by graphviz version 7.1.0 (20230121.1956)\n",
        " -->\n",
        "<!-- Title: g Pages: 1 -->\n",
-       "<svg width=\"396pt\" height=\"320pt\"\n",
-       " viewBox=\"0.00 0.00 396.00 320.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
+       "<svg width=\"374pt\" height=\"320pt\"\n",
+       " viewBox=\"0.00 0.00 374.00 320.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
        "<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 316)\">\n",
        "<title>g</title>\n",
-       "<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-316 392,-316 392,4 -4,4\"/>\n",
+       "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-316 370,-316 370,4 -4,4\"/>\n",
        "<!-- Noderoot -->\n",
        "<g id=\"node1\" class=\"node\">\n",
        "<title>Noderoot</title>\n",
@@ -596,150 +596,150 @@
        "<!-- Node1 -->\n",
        "<g id=\"node2\" class=\"node\">\n",
        "<title>Node1</title>\n",
-       "<path fill=\"#b3ee3a\" stroke=\"black\" d=\"M194,-188C194,-188 102,-188 102,-188 96,-188 90,-182 90,-176 90,-176 90,-147 90,-147 90,-141 96,-135 102,-135 102,-135 194,-135 194,-135 200,-135 206,-141 206,-147 206,-147 206,-176 206,-176 206,-182 200,-188 194,-188\"/>\n",
-       "<text text-anchor=\"middle\" x=\"148\" y=\"-172.8\" font-family=\"Times,serif\" font-size=\"14.00\">⇒</text>\n",
-       "<text text-anchor=\"middle\" x=\"148\" y=\"-157.8\" font-family=\"Times,serif\" font-size=\"14.00\">true</text>\n",
-       "<text text-anchor=\"middle\" x=\"148\" y=\"-142.8\" font-family=\"Times,serif\" font-size=\"14.00\">2 &gt; 3 ⇒ 4 &gt; 1</text>\n",
+       "<path fill=\"#b3ee3a\" stroke=\"black\" d=\"M174,-188C174,-188 102,-188 102,-188 96,-188 90,-182 90,-176 90,-176 90,-147 90,-147 90,-141 96,-135 102,-135 102,-135 174,-135 174,-135 180,-135 186,-141 186,-147 186,-147 186,-176 186,-176 186,-182 180,-188 174,-188\"/>\n",
+       "<text text-anchor=\"middle\" x=\"138\" y=\"-172.8\" font-family=\"Times,serif\" font-size=\"14.00\">⇒</text>\n",
+       "<text text-anchor=\"middle\" x=\"138\" y=\"-157.8\" font-family=\"Times,serif\" font-size=\"14.00\">true</text>\n",
+       "<text text-anchor=\"middle\" x=\"138\" y=\"-142.8\" font-family=\"Times,serif\" font-size=\"14.00\">2 &gt; 3 ⇒ 4 &gt; 1</text>\n",
        "</g>\n",
        "<!-- Node1&#45;&gt;Noderoot -->\n",
        "<g id=\"edge1\" class=\"edge\">\n",
        "<title>Node1&#45;&gt;Noderoot</title>\n",
-       "<path fill=\"none\" stroke=\"black\" d=\"M89.94,-138.96C80.94,-135.41 71.86,-131.82 63.53,-128.53\"/>\n",
-       "<polygon fill=\"black\" stroke=\"black\" points=\"64.74,-125.25 54.15,-124.83 62.17,-131.76 64.74,-125.25\"/>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M89.51,-141.02C81.23,-137.45 72.72,-133.78 64.78,-130.36\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"66.34,-127.22 55.77,-126.47 63.57,-133.65 66.34,-127.22\"/>\n",
        "</g>\n",
        "<!-- Node2 -->\n",
        "<g id=\"node3\" class=\"node\">\n",
        "<title>Node2</title>\n",
-       "<path fill=\"tomato\" stroke=\"black\" d=\"M286,-265C286,-265 254,-265 254,-265 248,-265 242,-259 242,-253 242,-253 242,-224 242,-224 242,-218 248,-212 254,-212 254,-212 286,-212 286,-212 292,-212 298,-218 298,-224 298,-224 298,-253 298,-253 298,-259 292,-265 286,-265\"/>\n",
-       "<text text-anchor=\"middle\" x=\"270\" y=\"-249.8\" font-family=\"Times,serif\" font-size=\"14.00\">&gt;</text>\n",
-       "<text text-anchor=\"middle\" x=\"270\" y=\"-234.8\" font-family=\"Times,serif\" font-size=\"14.00\">false</text>\n",
-       "<text text-anchor=\"middle\" x=\"270\" y=\"-219.8\" font-family=\"Times,serif\" font-size=\"14.00\">2 &gt; 3</text>\n",
+       "<path fill=\"tomato\" stroke=\"black\" d=\"M264,-265C264,-265 234,-265 234,-265 228,-265 222,-259 222,-253 222,-253 222,-224 222,-224 222,-218 228,-212 234,-212 234,-212 264,-212 264,-212 270,-212 276,-218 276,-224 276,-224 276,-253 276,-253 276,-259 270,-265 264,-265\"/>\n",
+       "<text text-anchor=\"middle\" x=\"249\" y=\"-249.8\" font-family=\"Times,serif\" font-size=\"14.00\">&gt;</text>\n",
+       "<text text-anchor=\"middle\" x=\"249\" y=\"-234.8\" font-family=\"Times,serif\" font-size=\"14.00\">false</text>\n",
+       "<text text-anchor=\"middle\" x=\"249\" y=\"-219.8\" font-family=\"Times,serif\" font-size=\"14.00\">2 &gt; 3</text>\n",
        "</g>\n",
        "<!-- Node2&#45;&gt;Node1 -->\n",
        "<g id=\"edge2\" class=\"edge\">\n",
        "<title>Node2&#45;&gt;Node1</title>\n",
-       "<path fill=\"none\" stroke=\"black\" d=\"M241.77,-221.03C229.17,-212.94 213.78,-203.07 199.2,-193.71\"/>\n",
-       "<polygon fill=\"black\" stroke=\"black\" points=\"201.03,-190.73 190.73,-188.27 197.25,-196.62 201.03,-190.73\"/>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M221.61,-219.86C210.97,-212.34 198.36,-203.43 186.23,-194.86\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"188.52,-192.2 178.33,-189.28 184.48,-197.91 188.52,-192.2\"/>\n",
        "</g>\n",
        "<!-- Node3 -->\n",
        "<g id=\"node4\" class=\"node\">\n",
        "<title>Node3</title>\n",
-       "<polygon fill=\"white\" stroke=\"black\" points=\"334,-275.5 334,-311.5 388,-311.5 388,-275.5 334,-275.5\"/>\n",
-       "<text text-anchor=\"middle\" x=\"361\" y=\"-289.8\" font-family=\"Times,serif\" font-size=\"14.00\">2</text>\n",
+       "<polygon fill=\"white\" stroke=\"black\" points=\"312,-275.5 312,-311.5 366,-311.5 366,-275.5 312,-275.5\"/>\n",
+       "<text text-anchor=\"middle\" x=\"339\" y=\"-289.8\" font-family=\"Times,serif\" font-size=\"14.00\">2</text>\n",
        "</g>\n",
        "<!-- Node3&#45;&gt;Node2 -->\n",
        "<g id=\"edge3\" class=\"edge\">\n",
        "<title>Node3&#45;&gt;Node2</title>\n",
-       "<path fill=\"none\" stroke=\"black\" d=\"M333.78,-277.3C325.39,-272.11 315.96,-266.29 307.01,-260.75\"/>\n",
-       "<polygon fill=\"black\" stroke=\"black\" points=\"308.62,-257.63 298.27,-255.35 304.94,-263.59 308.62,-257.63\"/>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M312.07,-277.3C303.9,-272.18 294.71,-266.44 285.96,-260.98\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"287.97,-258.1 277.63,-255.77 284.26,-264.04 287.97,-258.1\"/>\n",
        "</g>\n",
        "<!-- Node4 -->\n",
        "<g id=\"node5\" class=\"node\">\n",
        "<title>Node4</title>\n",
-       "<polygon fill=\"white\" stroke=\"black\" points=\"334,-220.5 334,-256.5 388,-256.5 388,-220.5 334,-220.5\"/>\n",
-       "<text text-anchor=\"middle\" x=\"361\" y=\"-234.8\" font-family=\"Times,serif\" font-size=\"14.00\">3</text>\n",
+       "<polygon fill=\"white\" stroke=\"black\" points=\"312,-220.5 312,-256.5 366,-256.5 366,-220.5 312,-220.5\"/>\n",
+       "<text text-anchor=\"middle\" x=\"339\" y=\"-234.8\" font-family=\"Times,serif\" font-size=\"14.00\">3</text>\n",
        "</g>\n",
        "<!-- Node4&#45;&gt;Node2 -->\n",
        "<g id=\"edge4\" class=\"edge\">\n",
        "<title>Node4&#45;&gt;Node2</title>\n",
-       "<path fill=\"none\" stroke=\"black\" d=\"M333.78,-238.5C325.83,-238.5 316.94,-238.5 308.41,-238.5\"/>\n",
-       "<polygon fill=\"black\" stroke=\"black\" points=\"308.27,-235 298.27,-238.5 308.27,-242 308.27,-235\"/>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M312.07,-238.5C304.42,-238.5 295.89,-238.5 287.66,-238.5\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"287.86,-235 277.86,-238.5 287.86,-242 287.86,-235\"/>\n",
        "</g>\n",
        "<!-- Node5 -->\n",
        "<g id=\"node6\" class=\"node\">\n",
        "<title>Node5</title>\n",
-       "<path fill=\"#b3ee3a\" stroke=\"black\" d=\"M286,-188C286,-188 254,-188 254,-188 248,-188 242,-182 242,-176 242,-176 242,-147 242,-147 242,-141 248,-135 254,-135 254,-135 286,-135 286,-135 292,-135 298,-141 298,-147 298,-147 298,-176 298,-176 298,-182 292,-188 286,-188\"/>\n",
-       "<text text-anchor=\"middle\" x=\"270\" y=\"-172.8\" font-family=\"Times,serif\" font-size=\"14.00\">&gt;</text>\n",
-       "<text text-anchor=\"middle\" x=\"270\" y=\"-157.8\" font-family=\"Times,serif\" font-size=\"14.00\">true</text>\n",
-       "<text text-anchor=\"middle\" x=\"270\" y=\"-142.8\" font-family=\"Times,serif\" font-size=\"14.00\">4 &gt; 1</text>\n",
+       "<path fill=\"#b3ee3a\" stroke=\"black\" d=\"M264,-188C264,-188 234,-188 234,-188 228,-188 222,-182 222,-176 222,-176 222,-147 222,-147 222,-141 228,-135 234,-135 234,-135 264,-135 264,-135 270,-135 276,-141 276,-147 276,-147 276,-176 276,-176 276,-182 270,-188 264,-188\"/>\n",
+       "<text text-anchor=\"middle\" x=\"249\" y=\"-172.8\" font-family=\"Times,serif\" font-size=\"14.00\">&gt;</text>\n",
+       "<text text-anchor=\"middle\" x=\"249\" y=\"-157.8\" font-family=\"Times,serif\" font-size=\"14.00\">true</text>\n",
+       "<text text-anchor=\"middle\" x=\"249\" y=\"-142.8\" font-family=\"Times,serif\" font-size=\"14.00\">4 &gt; 1</text>\n",
        "</g>\n",
        "<!-- Node5&#45;&gt;Node1 -->\n",
        "<g id=\"edge5\" class=\"edge\">\n",
        "<title>Node5&#45;&gt;Node1</title>\n",
-       "<path fill=\"none\" stroke=\"black\" d=\"M241.77,-161.5C234.03,-161.5 225.25,-161.5 216.24,-161.5\"/>\n",
-       "<polygon fill=\"black\" stroke=\"black\" points=\"216.02,-158 206.02,-161.5 216.02,-165 216.02,-158\"/>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M221.61,-161.5C214.34,-161.5 206.14,-161.5 197.81,-161.5\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"197.95,-158 187.95,-161.5 197.95,-165 197.95,-158\"/>\n",
        "</g>\n",
        "<!-- Node6 -->\n",
        "<g id=\"node7\" class=\"node\">\n",
        "<title>Node6</title>\n",
-       "<polygon fill=\"white\" stroke=\"black\" points=\"334,-165.5 334,-201.5 388,-201.5 388,-165.5 334,-165.5\"/>\n",
-       "<text text-anchor=\"middle\" x=\"361\" y=\"-179.8\" font-family=\"Times,serif\" font-size=\"14.00\">4</text>\n",
+       "<polygon fill=\"white\" stroke=\"black\" points=\"312,-165.5 312,-201.5 366,-201.5 366,-165.5 312,-165.5\"/>\n",
+       "<text text-anchor=\"middle\" x=\"339\" y=\"-179.8\" font-family=\"Times,serif\" font-size=\"14.00\">4</text>\n",
        "</g>\n",
        "<!-- Node6&#45;&gt;Node5 -->\n",
        "<g id=\"edge6\" class=\"edge\">\n",
        "<title>Node6&#45;&gt;Node5</title>\n",
-       "<path fill=\"none\" stroke=\"black\" d=\"M333.78,-177.02C325.74,-175.03 316.75,-172.81 308.13,-170.68\"/>\n",
-       "<polygon fill=\"black\" stroke=\"black\" points=\"308.82,-167.24 298.27,-168.24 307.14,-174.04 308.82,-167.24\"/>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M312.07,-177.02C304.34,-175.08 295.69,-172.92 287.38,-170.84\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"288.37,-167.48 277.82,-168.45 286.67,-174.28 288.37,-167.48\"/>\n",
        "</g>\n",
        "<!-- Node7 -->\n",
        "<g id=\"node8\" class=\"node\">\n",
        "<title>Node7</title>\n",
-       "<polygon fill=\"white\" stroke=\"black\" points=\"334,-110.5 334,-146.5 388,-146.5 388,-110.5 334,-110.5\"/>\n",
-       "<text text-anchor=\"middle\" x=\"361\" y=\"-124.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
+       "<polygon fill=\"white\" stroke=\"black\" points=\"312,-110.5 312,-146.5 366,-146.5 366,-110.5 312,-110.5\"/>\n",
+       "<text text-anchor=\"middle\" x=\"339\" y=\"-124.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
        "</g>\n",
        "<!-- Node7&#45;&gt;Node5 -->\n",
        "<g id=\"edge7\" class=\"edge\">\n",
        "<title>Node7&#45;&gt;Node5</title>\n",
-       "<path fill=\"none\" stroke=\"black\" d=\"M333.78,-138.22C325.66,-141.23 316.55,-144.61 307.85,-147.84\"/>\n",
-       "<polygon fill=\"black\" stroke=\"black\" points=\"306.43,-144.63 298.27,-151.39 308.86,-151.19 306.43,-144.63\"/>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M312.07,-138.22C304.25,-141.16 295.5,-144.44 287.09,-147.59\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"285.9,-144.3 277.77,-151.09 288.36,-150.85 285.9,-144.3\"/>\n",
        "</g>\n",
        "<!-- Node8 -->\n",
        "<g id=\"node9\" class=\"node\">\n",
        "<title>Node8</title>\n",
-       "<path fill=\"#b3ee3a\" stroke=\"black\" d=\"M175,-106C175,-106 121,-106 121,-106 115,-106 109,-100 109,-94 109,-94 109,-65 109,-65 109,-59 115,-53 121,-53 121,-53 175,-53 175,-53 181,-53 187,-59 187,-65 187,-65 187,-94 187,-94 187,-100 181,-106 175,-106\"/>\n",
-       "<text text-anchor=\"middle\" x=\"148\" y=\"-90.8\" font-family=\"Times,serif\" font-size=\"14.00\">¬</text>\n",
-       "<text text-anchor=\"middle\" x=\"148\" y=\"-75.8\" font-family=\"Times,serif\" font-size=\"14.00\">true</text>\n",
-       "<text text-anchor=\"middle\" x=\"148\" y=\"-60.8\" font-family=\"Times,serif\" font-size=\"14.00\">¬(5 &lt; 1)</text>\n",
+       "<path fill=\"#b3ee3a\" stroke=\"black\" d=\"M157.5,-106C157.5,-106 118.5,-106 118.5,-106 112.5,-106 106.5,-100 106.5,-94 106.5,-94 106.5,-65 106.5,-65 106.5,-59 112.5,-53 118.5,-53 118.5,-53 157.5,-53 157.5,-53 163.5,-53 169.5,-59 169.5,-65 169.5,-65 169.5,-94 169.5,-94 169.5,-100 163.5,-106 157.5,-106\"/>\n",
+       "<text text-anchor=\"middle\" x=\"138\" y=\"-90.8\" font-family=\"Times,serif\" font-size=\"14.00\">¬</text>\n",
+       "<text text-anchor=\"middle\" x=\"138\" y=\"-75.8\" font-family=\"Times,serif\" font-size=\"14.00\">true</text>\n",
+       "<text text-anchor=\"middle\" x=\"138\" y=\"-60.8\" font-family=\"Times,serif\" font-size=\"14.00\">¬(5 &lt; 1)</text>\n",
        "</g>\n",
        "<!-- Node8&#45;&gt;Noderoot -->\n",
        "<g id=\"edge8\" class=\"edge\">\n",
        "<title>Node8&#45;&gt;Noderoot</title>\n",
-       "<path fill=\"none\" stroke=\"black\" d=\"M108.69,-90.77C94.37,-94.98 78.16,-99.75 64.04,-103.9\"/>\n",
-       "<polygon fill=\"black\" stroke=\"black\" points=\"62.8,-100.62 54.2,-106.8 64.78,-107.33 62.8,-100.62\"/>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M106.06,-89.44C93.27,-93.54 78.35,-98.33 64.99,-102.62\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"64.11,-99.23 55.66,-105.62 66.25,-105.89 64.11,-99.23\"/>\n",
        "</g>\n",
        "<!-- Node9 -->\n",
        "<g id=\"node10\" class=\"node\">\n",
        "<title>Node9</title>\n",
-       "<path fill=\"tomato\" stroke=\"black\" d=\"M286,-100C286,-100 254,-100 254,-100 248,-100 242,-94 242,-88 242,-88 242,-59 242,-59 242,-53 248,-47 254,-47 254,-47 286,-47 286,-47 292,-47 298,-53 298,-59 298,-59 298,-88 298,-88 298,-94 292,-100 286,-100\"/>\n",
-       "<text text-anchor=\"middle\" x=\"270\" y=\"-84.8\" font-family=\"Times,serif\" font-size=\"14.00\">&lt;</text>\n",
-       "<text text-anchor=\"middle\" x=\"270\" y=\"-69.8\" font-family=\"Times,serif\" font-size=\"14.00\">false</text>\n",
-       "<text text-anchor=\"middle\" x=\"270\" y=\"-54.8\" font-family=\"Times,serif\" font-size=\"14.00\">5 &lt; 1</text>\n",
+       "<path fill=\"tomato\" stroke=\"black\" d=\"M264,-100C264,-100 234,-100 234,-100 228,-100 222,-94 222,-88 222,-88 222,-59 222,-59 222,-53 228,-47 234,-47 234,-47 264,-47 264,-47 270,-47 276,-53 276,-59 276,-59 276,-88 276,-88 276,-94 270,-100 264,-100\"/>\n",
+       "<text text-anchor=\"middle\" x=\"249\" y=\"-84.8\" font-family=\"Times,serif\" font-size=\"14.00\">&lt;</text>\n",
+       "<text text-anchor=\"middle\" x=\"249\" y=\"-69.8\" font-family=\"Times,serif\" font-size=\"14.00\">false</text>\n",
+       "<text text-anchor=\"middle\" x=\"249\" y=\"-54.8\" font-family=\"Times,serif\" font-size=\"14.00\">5 &lt; 1</text>\n",
        "</g>\n",
        "<!-- Node9&#45;&gt;Node8 -->\n",
        "<g id=\"edge9\" class=\"edge\">\n",
        "<title>Node9&#45;&gt;Node8</title>\n",
-       "<path fill=\"none\" stroke=\"black\" d=\"M241.77,-74.86C228.62,-75.52 212.45,-76.33 197.31,-77.08\"/>\n",
-       "<polygon fill=\"black\" stroke=\"black\" points=\"196.85,-73.6 187.04,-77.6 197.2,-80.59 196.85,-73.6\"/>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M221.61,-74.95C209.41,-75.62 194.61,-76.44 180.93,-77.19\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"181.08,-73.68 171.29,-77.72 181.47,-80.67 181.08,-73.68\"/>\n",
        "</g>\n",
        "<!-- Node10 -->\n",
        "<g id=\"node11\" class=\"node\">\n",
        "<title>Node10</title>\n",
-       "<polygon fill=\"white\" stroke=\"black\" points=\"334,-55.5 334,-91.5 388,-91.5 388,-55.5 334,-55.5\"/>\n",
-       "<text text-anchor=\"middle\" x=\"361\" y=\"-69.8\" font-family=\"Times,serif\" font-size=\"14.00\">5</text>\n",
+       "<polygon fill=\"white\" stroke=\"black\" points=\"312,-55.5 312,-91.5 366,-91.5 366,-55.5 312,-55.5\"/>\n",
+       "<text text-anchor=\"middle\" x=\"339\" y=\"-69.8\" font-family=\"Times,serif\" font-size=\"14.00\">5</text>\n",
        "</g>\n",
        "<!-- Node10&#45;&gt;Node9 -->\n",
        "<g id=\"edge10\" class=\"edge\">\n",
        "<title>Node10&#45;&gt;Node9</title>\n",
-       "<path fill=\"none\" stroke=\"black\" d=\"M333.78,-73.5C325.83,-73.5 316.94,-73.5 308.41,-73.5\"/>\n",
-       "<polygon fill=\"black\" stroke=\"black\" points=\"308.27,-70 298.27,-73.5 308.27,-77 308.27,-70\"/>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M312.07,-73.5C304.42,-73.5 295.89,-73.5 287.66,-73.5\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"287.86,-70 277.86,-73.5 287.86,-77 287.86,-70\"/>\n",
        "</g>\n",
        "<!-- Node11 -->\n",
        "<g id=\"node12\" class=\"node\">\n",
        "<title>Node11</title>\n",
-       "<polygon fill=\"white\" stroke=\"black\" points=\"334,-0.5 334,-36.5 388,-36.5 388,-0.5 334,-0.5\"/>\n",
-       "<text text-anchor=\"middle\" x=\"361\" y=\"-14.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
+       "<polygon fill=\"white\" stroke=\"black\" points=\"312,-0.5 312,-36.5 366,-36.5 366,-0.5 312,-0.5\"/>\n",
+       "<text text-anchor=\"middle\" x=\"339\" y=\"-14.8\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
        "</g>\n",
        "<!-- Node11&#45;&gt;Node9 -->\n",
        "<g id=\"edge11\" class=\"edge\">\n",
        "<title>Node11&#45;&gt;Node9</title>\n",
-       "<path fill=\"none\" stroke=\"black\" d=\"M333.78,-34.7C325.39,-39.89 315.96,-45.71 307.01,-51.25\"/>\n",
-       "<polygon fill=\"black\" stroke=\"black\" points=\"304.94,-48.41 298.27,-56.65 308.62,-54.37 304.94,-48.41\"/>\n",
+       "<path fill=\"none\" stroke=\"black\" d=\"M312.07,-34.7C303.9,-39.82 294.71,-45.56 285.96,-51.02\"/>\n",
+       "<polygon fill=\"black\" stroke=\"black\" points=\"284.26,-47.96 277.63,-56.23 287.97,-53.9 284.26,-47.96\"/>\n",
        "</g>\n",
        "</g>\n",
-       "</svg>"
+       "</svg>\n"
       ],
       "text/plain": [
-       "<Dot visualization: formula_tree [(2>3 => 4>1) <=> not(5<1)]>"
+       "<Dot visualization: formula_tree [(2>3 ⇒ 4>1) ⇔ ¬(5<1)]>"
       ]
      },
      "execution_count": 17,
@@ -761,10 +761,7 @@
     "\n",
     "<img src=\"./img/wahrheitstabelle.png\" width=\"600\">\n",
     "\n",
-    "Wie berechnet man damit den Wahrheitswert einer Formel wie $(p \\vee (\\neg p \\wedge q))$?\n",
-    "\n",
-    "\n",
-    "\n"
+    "Wie berechnet man damit den Wahrheitswert einer Formel wie $(p \\vee (\\neg p \\wedge q))$?"
    ]
   },
   {
@@ -774,7 +771,7 @@
     "\n",
     "## Interpretationen\n",
     "Man braucht erst die Wahrheitswerte für die atomaren Aussagen $p$ und $q$.\n",
-    "Diese Information nennt man eine <b>Interpretation</b> für die Formel.\n",
+    "Diese Information nennt man eine **Interpretation** für die Formel.\n",
     "Die Formel oben hat 4 Interpretationen, da $p$ und $q$ jeweils wahr oder falsch sein können.\n",
     "\n",
     "Mit einer Interpretation kann man nun \n",
@@ -782,12 +779,12 @@
     "* und mit der Wahrheitstabelle dann den Wert von immer grösseren Unterformeln berechnen.\n",
     "\n",
     "Beispiel:\n",
-    "Sei $i$ =  $\\{p\\mapsto TRUE,q\\mapsto FALSE\\}$ eine Interpretation für die Formel $(p \\vee (\\neg p \\wedge q))$.\n",
+    "Sei $i$ =  $\\{p\\mapsto \\mathit{TRUE},q\\mapsto \\mathit{FALSE}\\}$ eine Interpretation für die Formel $(p \\vee (\\neg p \\wedge q))$.\n",
     "\n",
-    "* Schritt 1: alle Aussagen berechnen:       $~(TRUE \\vee (\\neg TRUE \\wedge FALSE)$\n",
-    "* Schritt 2: $\\neg TRUE = FALSE$:           $~(TRUE \\vee (FALSE \\wedge FALSE)$\n",
-    "* Schritt 3: $FALSE \\wedge FALSE = FALSE$:  $~(TRUE \\vee FALSE)$\n",
-    "* Schritt 3: $TRUE \\vee FALSE = TRUE$:      $~TRUE$\n",
+    "* Schritt 1: alle Aussagen berechnen:                                  $~(\\mathit{TRUE} \\vee (\\neg \\mathit{TRUE} \\wedge \\mathit{FALSE})$\n",
+    "* Schritt 2: $\\neg \\mathit{TRUE} = \\mathit{FALSE}$:                    $~(\\mathit{TRUE} \\vee (\\mathit{FALSE} \\wedge \\mathit{FALSE})$\n",
+    "* Schritt 3: $\\mathit{FALSE} \\wedge \\mathit{FALSE} = \\mathit{FALSE}$:  $~(\\mathit{TRUE} \\vee \\mathit{FALSE})$\n",
+    "* Schritt 3: $\\mathit{TRUE} \\vee \\mathit{FALSE} = \\mathit{TRUE}$:      $~\\mathit{TRUE}$\n",
     "\n",
     "Unter der Interpretation $i$ ist die Formel $(p \\vee (\\neg p \\wedge q)$ wahr."
    ]
@@ -798,16 +795,16 @@
    "source": [
     "## Modelle\n",
     "\n",
-    "Man nennt so eine Interpretation ein <b>Modell</b> für die Formel.\n",
+    "Man nennt so eine Interpretation ein **Modell** für die Formel.\n",
     "\n",
-    "* eine Interpretation $i$ so dass $i(\\phi)={\\color{olive}{TRUE}}$ ist ein <b>Modell</b> für $\\phi$\n",
-    "* eine Formel $\\phi$ die mindestens ein Modell hat heißt <b>erfüllbar</b>\n",
-    "* eine Formel $\\phi$ wo alle Interpretationen auch Modelle sind wird eine <b>Tautologie</b> genannt\n",
-    "* eine Formel ohne Modell heißt <b>unerfüllbar</b> oder ein Widerspruch\n",
+    "* eine Interpretation $i$ so dass $i(\\phi)={\\color{olive}{\\mathit{TRUE}}}$ ist ein **Modell** für $\\phi$\n",
+    "* eine Formel $\\phi$ die mindestens ein Modell hat heißt **erfüllbar**\n",
+    "* eine Formel $\\phi$ wo alle Interpretationen auch Modelle sind wird eine **Tautologie** genannt\n",
+    "* eine Formel ohne Modell heißt **unerfüllbar** oder ein Widerspruch\n",
     "\n",
     "\n",
     "\n",
-    "Die Interpretation $i'$ =  $\\{p\\mapsto FALSE,q\\mapsto FALSE\\}$ ist kein Modell von $(p \\vee (\\neg p \\wedge q))$.\n",
+    "Die Interpretation $i'$ =  $\\{p\\mapsto \\mathit{FALSE},q\\mapsto \\mathit{FALSE}\\}$ ist kein Modell von $(p \\vee (\\neg p \\wedge q))$.\n",
     "Die Formel ist also keine Tautologie, aber erfüllbar.\n",
     "\n",
     "Die Formel $p \\vee \\neg p$ ist eine Tautologie: alle Interpretation machen die Formel wahr.\n",
@@ -821,7 +818,7 @@
     "\n",
     "# Äquivalenz von Formeln\n",
     "\n",
-    "Zwei Formeln sind <b>äquivalent</b> gdw sie die selben Modelle haben.\n",
+    "Zwei Formeln sind **äquivalent** gdw sie die selben Modelle haben.\n",
     "\n",
     "$(p \\vee (\\neg p \\wedge q))$ ist zum Beispiel äquivalent zu $p \\vee q$.\n",
     "Hier stellen wir die Interpretationen und Modelle tabellarisch dar:"
@@ -837,10 +834,10 @@
       "text/markdown": [
        "|p|q|F1|F2|\n",
        "|---|---|---|---|\n",
-       "|$\\mathit{FALSE}$|$\\mathit{FALSE}$|$\\mathit{FALSE}$|$\\mathit{FALSE}$|\n",
-       "|$\\mathit{FALSE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|\n",
-       "|$\\mathit{TRUE}$|$\\mathit{FALSE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|\n",
-       "|$\\mathit{TRUE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|\n"
+       "|FALSE|FALSE|FALSE|FALSE|\n",
+       "|FALSE|TRUE|TRUE|TRUE|\n",
+       "|TRUE|FALSE|TRUE|TRUE|\n",
+       "|TRUE|TRUE|TRUE|TRUE|\n"
       ],
       "text/plain": [
        "p\tq\tF1\tF2\n",
@@ -868,7 +865,7 @@
    "source": [
     "Wir schreiben diesen Tatbestand als $(p \\vee (\\neg p \\wedge q)) \\equiv p \\vee q$.\n",
     "\n",
-    "Kleine Anmerkung: das Werkzeug im Jupyter Notebook akzeptiert keine aussagenlogische Variablen sondern nur Bool'sche Datenvariablen. Anstatt $p$ muss man  ```p=TRUE``` schreiben und anstatt $p \\vee q$ muss man ```p=TRUE ∨ q=TRUE``` schreiben. Mit ```bool(P)``` konvertiert man den Wahrheitswert einer Formel in einen Bool'schen Datenwert um.\n",
+    "Kleine Anmerkung: das Werkzeug im Jupyter Notebook akzeptiert keine aussagenlogische Variablen sondern nur Bool'sche Datenvariablen. Anstatt $p$ muss man `p=TRUE` schreiben und anstatt $p \\vee q$ muss man `p=TRUE ∨ q=TRUE` schreiben. Mit `bool(P)` konvertiert man den Wahrheitswert einer Formel in einen Bool'schen Datenwert um.\n",
     "\n",
     "$\\equiv$ ist eine Relation zwischen logischen Formeln.\n",
     "$\\equiv$ ist transitiv und kommutativ."
@@ -905,10 +902,10 @@
       "text/markdown": [
        "|p|q|ODER|NODER|NUND|np|nq|\n",
        "|---|---|---|---|---|---|---|\n",
-       "|$\\mathit{FALSE}$|$\\mathit{FALSE}$|$\\mathit{FALSE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|\n",
-       "|$\\mathit{FALSE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|$\\mathit{FALSE}$|$\\mathit{FALSE}$|$\\mathit{TRUE}$|$\\mathit{FALSE}$|\n",
-       "|$\\mathit{TRUE}$|$\\mathit{FALSE}$|$\\mathit{TRUE}$|$\\mathit{FALSE}$|$\\mathit{FALSE}$|$\\mathit{FALSE}$|$\\mathit{TRUE}$|\n",
-       "|$\\mathit{TRUE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|$\\mathit{FALSE}$|$\\mathit{FALSE}$|$\\mathit{FALSE}$|$\\mathit{FALSE}$|\n"
+       "|FALSE|FALSE|FALSE|TRUE|TRUE|TRUE|TRUE|\n",
+       "|FALSE|TRUE|TRUE|FALSE|FALSE|TRUE|FALSE|\n",
+       "|TRUE|FALSE|TRUE|FALSE|FALSE|FALSE|TRUE|\n",
+       "|TRUE|TRUE|TRUE|FALSE|FALSE|FALSE|FALSE|\n"
       ],
       "text/plain": [
        "p\tq\tODER\tNODER\tNUND\tnp\tnq\n",
@@ -925,9 +922,9 @@
    ],
    "source": [
     ":table {p,q,ODER,NODER,NUND,np,nq| p:BOOL & q:BOOL & np = bool(¬(p=TRUE)) & nq = bool(¬(q=TRUE)) &\n",
-    "                            ODER=bool(p=TRUE ∨ q=TRUE) &\n",
-    "                            NODER = bool(¬(ODER=TRUE)) &\n",
-    "                            NUND=bool((np=TRUE) ∧ (nq=TRUE))}"
+    "                                   ODER=bool(p=TRUE ∨ q=TRUE) &\n",
+    "                                   NODER = bool(¬(ODER=TRUE)) &\n",
+    "                                   NUND=bool((np=TRUE) ∧ (nq=TRUE))}"
    ]
   },
   {
@@ -952,10 +949,10 @@
       "text/markdown": [
        "|p|q|IMPL|KONT|np|nq|\n",
        "|---|---|---|---|---|---|\n",
-       "|$\\mathit{FALSE}$|$\\mathit{FALSE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|\n",
-       "|$\\mathit{FALSE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|$\\mathit{FALSE}$|\n",
-       "|$\\mathit{TRUE}$|$\\mathit{FALSE}$|$\\mathit{FALSE}$|$\\mathit{FALSE}$|$\\mathit{FALSE}$|$\\mathit{TRUE}$|\n",
-       "|$\\mathit{TRUE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|$\\mathit{FALSE}$|$\\mathit{FALSE}$|\n"
+       "|FALSE|FALSE|TRUE|TRUE|TRUE|TRUE|\n",
+       "|FALSE|TRUE|TRUE|TRUE|TRUE|FALSE|\n",
+       "|TRUE|FALSE|FALSE|FALSE|FALSE|TRUE|\n",
+       "|TRUE|TRUE|TRUE|TRUE|FALSE|FALSE|\n"
       ],
       "text/plain": [
        "p\tq\tIMPL\tKONT\tnp\tnq\n",
@@ -972,8 +969,8 @@
    ],
    "source": [
     ":table {p,q,IMPL,KONT,np,nq| p:BOOL & q:BOOL & np = bool(¬(p=TRUE)) & nq = bool(¬(q=TRUE)) &\n",
-    "                            IMPL=bool(p=TRUE => q=TRUE) &\n",
-    "                            KONT=bool((nq=TRUE) => (np=TRUE))}"
+    "                             IMPL=bool(p=TRUE => q=TRUE) &\n",
+    "                             KONT=bool((nq=TRUE) => (np=TRUE))}"
    ]
   },
   {
@@ -981,7 +978,7 @@
    "metadata": {},
    "source": [
     "Es gilt also:\n",
-    "$\\phi \\Rightarrow \\psi$ $\\equiv$ $\\neg \\psi \\Rightarrow \\neg \\phi$  ."
+    "$\\phi \\Rightarrow \\psi$ $\\equiv$ $\\neg \\psi \\Rightarrow \\neg \\phi$."
    ]
   },
   {
@@ -1007,10 +1004,10 @@
       "text/markdown": [
        "|p|q|F1|F2|\n",
        "|---|---|---|---|\n",
-       "|$\\mathit{FALSE}$|$\\mathit{FALSE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|\n",
-       "|$\\mathit{FALSE}$|$\\mathit{TRUE}$|$\\mathit{FALSE}$|$\\mathit{TRUE}$|\n",
-       "|$\\mathit{TRUE}$|$\\mathit{FALSE}$|$\\mathit{FALSE}$|$\\mathit{FALSE}$|\n",
-       "|$\\mathit{TRUE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|\n"
+       "|FALSE|FALSE|TRUE|TRUE|\n",
+       "|FALSE|TRUE|FALSE|TRUE|\n",
+       "|TRUE|FALSE|FALSE|FALSE|\n",
+       "|TRUE|TRUE|TRUE|TRUE|\n"
       ],
       "text/plain": [
        "p\tq\tF1\tF2\n",
@@ -1046,9 +1043,9 @@
     "* $(\\phi \\Leftrightarrow \\psi) \\wedge \\psi \\models \\phi$\n",
     "* $(\\phi \\Leftrightarrow \\psi) \\wedge \\neg\\psi \\models \\neg\\phi$\n",
     "\n",
-    "Achtung $\\phi \\wedge \\neg \\phi \\models \\psi$ für beliebiges $\\psi$ !\n",
+    "Achtung $\\phi \\wedge \\neg \\phi \\models \\psi$ für beliebiges $\\psi$!\n",
     "Also:\n",
-    "* $1>2 \\models 1+1=100$\n"
+    "* $1>2 \\models 1+1=100$"
    ]
   },
   {
@@ -1058,15 +1055,15 @@
     "# Smullyan  - Einfaches Puzzle\n",
     "    \n",
     "Raymond Smullyan beschreibt in seinen Büchern eine Insel auf der es (nur) zwei Arten von Personen gibt:\n",
-    "* Ritter die immer die Wahrheit sagen, und\n",
-    "* Schurken die immer lügen.\n",
+    "* Ritter, die immer die Wahrheit sagen, und\n",
+    "* Schurken, die immer lügen.\n",
     "\n",
     "Hier ist ein Puzzle aus einem seiner Bücher:\n",
     "    \n",
-    "* X sagt: ```Y ist ein Ritter```\n",
-    "* Y sagt: ```X und ich sind von einem unterschiedlichen Typ.```\n",
+    "* X sagt: \"Y ist ein Ritter\"\n",
+    "* Y sagt: \"X und ich sind von einem unterschiedlichen Typ\"\n",
     "\n",
-    "Können wir bestimmen ob X und Y Ritter oder Schurken sind?\n"
+    "Können wir bestimmen ob X und Y Ritter oder Schurken sind?"
    ]
   },
   {
@@ -1082,9 +1079,9 @@
     "\n",
     "Schritt 2: Übersetzung der Informationen in Aussagenlogik\n",
     "* $\\mathit{X} \\Leftrightarrow  \\mathit{Y}$ ist die Übersetzung von:\n",
-    " * X sagt: ```Y ist ein Ritter``` \n",
+    "    * X sagt: \"Y ist ein Ritter\"\n",
     "* $\\mathit{Y} \\Leftrightarrow  (\\mathit{X} \\Leftrightarrow  \\neg (\\mathit{Y}))$ ist die Übersetzung von:\n",
-    " * Y sagt: ```X und ich sind von einem unterschiedlichen Typ.```\n",
+    "    * Y sagt: \"X und ich sind von einem unterschiedlichen Typ\"\n",
     "\n",
     "\n",
     "Schritt 3: Bestimmung der Modelle:"
@@ -1100,10 +1097,10 @@
       "text/markdown": [
        "|x|y|S1|S2|Puzzle|\n",
        "|---|---|---|---|---|\n",
-       "|$\\mathit{FALSE}$|$\\mathit{FALSE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|\n",
-       "|$\\mathit{FALSE}$|$\\mathit{TRUE}$|$\\mathit{FALSE}$|$\\mathit{TRUE}$|$\\mathit{FALSE}$|\n",
-       "|$\\mathit{TRUE}$|$\\mathit{FALSE}$|$\\mathit{FALSE}$|$\\mathit{FALSE}$|$\\mathit{FALSE}$|\n",
-       "|$\\mathit{TRUE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|$\\mathit{FALSE}$|$\\mathit{FALSE}$|\n"
+       "|FALSE|FALSE|TRUE|TRUE|TRUE|\n",
+       "|FALSE|TRUE|FALSE|TRUE|FALSE|\n",
+       "|TRUE|FALSE|FALSE|FALSE|FALSE|\n",
+       "|TRUE|TRUE|TRUE|FALSE|FALSE|\n"
       ],
       "text/plain": [
        "x\ty\tS1\tS2\tPuzzle\n",
@@ -1120,9 +1117,9 @@
    ],
    "source": [
     ":table {x,y,S1,S2,Puzzle | x:BOOL & y:BOOL & \n",
-    "                   S1=bool(x=TRUE ⇔ y=TRUE) &\n",
-    "                   S2=bool(y=TRUE ⇔ (x=TRUE ⇔ ¬(y=TRUE))) &\n",
-    "                   Puzzle=bool(S1=TRUE & S2=TRUE)}"
+    "                           S1=bool(x=TRUE ⇔ y=TRUE) &\n",
+    "                           S2=bool(y=TRUE ⇔ (x=TRUE ⇔ ¬(y=TRUE))) &\n",
+    "                           Puzzle=bool(S1=TRUE & S2=TRUE)}"
    ]
   },
   {
@@ -1135,9 +1132,9 @@
     "Ein typische fehlerhafte Übersetzung des Puzzles ist diese:\n",
     "\n",
     "* $\\mathit{X} \\Rightarrow  \\mathit{Y}$ ist die Übersetzung von:\n",
-    " * X sagt: ```Y ist ein Ritter``` \n",
+    "    * X sagt: \"Y ist ein Ritter\"\n",
     "* $\\mathit{Y} \\Rightarrow  (\\mathit{X} \\Leftrightarrow  \\neg (\\mathit{Y}))$ ist die Übersetzung von:\n",
-    " * Y sagt: ```X und ich sind von einem unterschiedlichen Typ.```\n"
+    "    * Y sagt: \"X und ich sind von einem unterschiedlichen Typ\""
    ]
   },
   {
@@ -1150,10 +1147,10 @@
       "text/markdown": [
        "|x|y|S1|S2|Puzzle|\n",
        "|---|---|---|---|---|\n",
-       "|$\\mathit{FALSE}$|$\\mathit{FALSE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|\n",
-       "|$\\mathit{FALSE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|\n",
-       "|$\\mathit{TRUE}$|$\\mathit{FALSE}$|$\\mathit{FALSE}$|$\\mathit{TRUE}$|$\\mathit{FALSE}$|\n",
-       "|$\\mathit{TRUE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|$\\mathit{FALSE}$|$\\mathit{FALSE}$|\n"
+       "|FALSE|FALSE|TRUE|TRUE|TRUE|\n",
+       "|FALSE|TRUE|TRUE|TRUE|TRUE|\n",
+       "|TRUE|FALSE|FALSE|TRUE|FALSE|\n",
+       "|TRUE|TRUE|TRUE|FALSE|FALSE|\n"
       ],
       "text/plain": [
        "x\ty\tS1\tS2\tPuzzle\n",
@@ -1170,16 +1167,15 @@
    ],
    "source": [
     ":table {x,y,S1,S2,Puzzle | x:BOOL & y:BOOL & \n",
-    "                   S1=bool(x=TRUE ⇒ y=TRUE) &\n",
-    "                   S2=bool(y=TRUE ⇒ (x=TRUE ⇔ ¬(y=TRUE))) &\n",
-    "                   Puzzle=bool(S1=TRUE & S2=TRUE)}"
+    "                           S1=bool(x=TRUE ⇒ y=TRUE) &\n",
+    "                           S2=bool(y=TRUE ⇒ (x=TRUE ⇔ ¬(y=TRUE))) &\n",
+    "                           Puzzle=bool(S1=TRUE & S2=TRUE)}"
    ]
   },
   {
    "cell_type": "markdown",
    "metadata": {},
    "source": [
-    "\n",
     "Diese Übersetzung erlaubt zwei Modelle, und auch eine fehlerhafte \"Lösung\" mit X als Schurken und Y als Ritter. Diese Lösung ist falsch, da X und Y die Wahrheit sagen, aber nur Y ein Ritter ist."
    ]
   },
@@ -1191,21 +1187,19 @@
     "    \n",
     "* Theorem: $\\phi \\models \\psi$ genau dann wenn $\\phi \\wedge \\neg \\psi$ kein Modell hat\n",
     "\n",
-    "    \n",
-    " Beweis (ist ein Äquivalenzbeweis auf Metaebene):\n",
+    "Beweis (ist ein Äquivalenzbeweis auf Metaebene):\n",
     "    \n",
     "* $\\phi \\models \\psi$\n",
     "* $\\Longleftrightarrow$ alle Modelle von $\\phi$ sind auch Modelle von $\\psi$ (per Definition von $\\models$)\n",
     "* $\\Longleftrightarrow$ in allen Modellen von $\\phi$ hat $\\neg \\psi$ den Wahrheitswert falsch (per Definition von $\\neg$)\n",
     "* $\\Longleftrightarrow$ alle Modelle von $\\phi$ sind kein Modell von $\\phi \\wedge \\neg \\psi$ (per Definition von $\\wedge$)\n",
-    "* $\\Longleftrightarrow$ $\\phi \\wedge \\neg \\psi$ hat kein Modell  (da auch kein Modell von $\\neg \\phi$ ein Modell von $\\phi  \\wedge \\neg \\psi$ sein kann)\n"
+    "* $\\Longleftrightarrow$ $\\phi \\wedge \\neg \\psi$ hat kein Modell  (da auch kein Modell von $\\neg \\phi$ ein Modell von $\\phi  \\wedge \\neg \\psi$ sein kann)"
    ]
   },
   {
    "cell_type": "markdown",
    "metadata": {},
    "source": [
-    "\n",
     "Anwendung auf unser Puzzle:\n",
     "* Sei $\\phi$ = $(\\mathit{X} \\Leftrightarrow  \\mathit{Y}) \\wedge (\\mathit{Y} \\Leftrightarrow  (\\mathit{X} \\Leftrightarrow  \\neg (\\mathit{Y})))$\n",
     "* Sei $\\psi$ = $\\neg X \\wedge \\neg Y$  (X und Y sind Schurken)\n",
@@ -1223,10 +1217,10 @@
       "text/markdown": [
        "|x|y|S1|S2|Puzzle|WS|\n",
        "|---|---|---|---|---|---|\n",
-       "|$\\mathit{FALSE}$|$\\mathit{FALSE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|$\\mathit{FALSE}$|\n",
-       "|$\\mathit{FALSE}$|$\\mathit{TRUE}$|$\\mathit{FALSE}$|$\\mathit{TRUE}$|$\\mathit{FALSE}$|$\\mathit{FALSE}$|\n",
-       "|$\\mathit{TRUE}$|$\\mathit{FALSE}$|$\\mathit{FALSE}$|$\\mathit{FALSE}$|$\\mathit{FALSE}$|$\\mathit{FALSE}$|\n",
-       "|$\\mathit{TRUE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|$\\mathit{FALSE}$|$\\mathit{FALSE}$|$\\mathit{FALSE}$|\n"
+       "|FALSE|FALSE|TRUE|TRUE|TRUE|FALSE|\n",
+       "|FALSE|TRUE|FALSE|TRUE|FALSE|FALSE|\n",
+       "|TRUE|FALSE|FALSE|FALSE|FALSE|FALSE|\n",
+       "|TRUE|TRUE|TRUE|FALSE|FALSE|FALSE|\n"
       ],
       "text/plain": [
        "x\ty\tS1\tS2\tPuzzle\tWS\n",
@@ -1243,10 +1237,10 @@
    ],
    "source": [
     ":table {x,y,S1,S2,Puzzle,WS | x:BOOL & y:BOOL & \n",
-    "                   S1=bool(x=TRUE ⇔ y=TRUE) &\n",
-    "                   S2=bool(y=TRUE ⇔ (x=TRUE ⇔ ¬(y=TRUE))) &\n",
-    "                   Puzzle=bool(S1=TRUE & S2=TRUE) &\n",
-    "                   WS=bool(Puzzle=TRUE & not( not(x=TRUE) & not(y=TRUE)))}"
+    "                              S1=bool(x=TRUE ⇔ y=TRUE) &\n",
+    "                              S2=bool(y=TRUE ⇔ (x=TRUE ⇔ ¬(y=TRUE))) &\n",
+    "                              Puzzle=bool(S1=TRUE & S2=TRUE) &\n",
+    "                              WS=bool(Puzzle=TRUE & not( not(x=TRUE) & not(y=TRUE)))}"
    ]
   },
   {
@@ -1269,15 +1263,13 @@
     "    \n",
     "Wir haben per Transitivität von $\\equiv$, dass $\\phi_1 \\equiv \\phi_k$.\n",
     "Da $\\equiv$ auch kommutativ ist, gilt der Beweis auch in die andere Richtung: $\\phi_k \\equiv \\phi_1$.\n",
-    "Wir haben sowohl $\\phi_1 \\models \\phi_k$ als auch $\\phi_k \\models \\phi_1$.\n",
-    "    "
+    "Wir haben sowohl $\\phi_1 \\models \\phi_k$ als auch $\\phi_k \\models \\phi_1$."
    ]
   },
   {
    "cell_type": "markdown",
    "metadata": {},
    "source": [
-    "\n",
     "Als kleines Beispiel beweisen wir, dass $\\neg b \\Rightarrow a \\equiv a \\vee b$:\n",
     "* $\\neg b \\Rightarrow a$\n",
     "* $\\Longleftrightarrow$ $\\neg \\neg b \\vee a$  (Regel: $\\phi \\Rightarrow \\psi \\equiv \\neg \\phi \\vee \\psi$)\n",
@@ -1303,21 +1295,19 @@
     "    \n",
     "Wir haben per Transitiviät von $\\models$, dass $\\phi_1 \\models \\phi_k$.\n",
     "Aber im Gegensatz zum Äquivalenzbeweis gilt hier generell nicht $\\phi_k \\models \\phi_1$!\n",
-    "Dieser Beweis kann nicht umgekehrt werden.\n",
-    "\n"
+    "Dieser Beweis kann nicht umgekehrt werden."
    ]
   },
   {
    "cell_type": "markdown",
    "metadata": {},
    "source": [
-    "\n",
     "Wir illustrieren dies Art der Beweisführung mit einem anderen kleinen Puzzle von unserer Insel der Ritter und Schurken:\n",
-    "* A sagt: ``B ist ein Ritter''\n",
-    "* B sagt: ``1+1=3''\n",
+    "* A sagt: \"B ist ein Ritter\"\n",
+    "* B sagt: \"1+1=3\"\n",
     "\n",
-    "* $\\phi_1$ = $A \\Leftrightarrow B$ $\\wedge$  $B \\Leftrightarrow FALSE$\n",
-    "* $\\neg B$  (nach der zweiten Aussage $B \\Leftrightarrow FALSE$ muss B ein Schurke sein)\n",
+    "* $\\phi_1$ = $A \\Leftrightarrow B$ $\\wedge$  $B \\Leftrightarrow \\mathit{FALSE}$\n",
+    "* $\\neg B$  (nach der zweiten Aussage $B \\Leftrightarrow \\mathit{FALSE}$ muss B ein Schurke sein)\n",
     "* $\\neg A$  (nach der ersten Aussage $A \\Leftrightarrow B$ muss A demnach auch ein Schurke sein)\n",
     "\n",
     "Wir haben per Transitiviät, dass $\\phi_1 \\models \\neg A$, d.h. es folgt aus dem Puzzle, dass A ein Schurke ist."
@@ -1331,14 +1321,13 @@
     "\n",
     "Die [Syllogistik](https://de.wikipedia.org/wiki/Syllogismus), einer Vorform der Prädikatenlogik, geht auf Aristoteles zurück.\n",
     "\n",
-    "\n",
     "Was ist der Zusammenhang zwischen folgenden vier Aussagen, unter der Annahme, dass es mindestens einen Mensch gibt?\n",
     "(In die Aussagenlogik sind alle vier Aussagen unabhängig.)\n",
     "\n",
     "1. Alle Menschen sind sterblich.\n",
     "2. Einige Menschen sind sterblich.\n",
     "3. Alle Menschen sind unsterblich.\n",
-    "4. Einige Menschen sind unsterblich.\n"
+    "4. Einige Menschen sind unsterblich."
    ]
   },
   {
@@ -1348,11 +1337,11 @@
     "# Prädikatenlogik\n",
     "    \n",
     "Im Vergleich zur Aussagenlogik mit den Wahrheitswerten und Aussagen, gibt es in der Prädikatenlogik:\n",
-    "* Objekte\n",
-    "* <b>Konstanten</b> und <b>Variablen</b> die Objekte darstellen,\n",
-    "* <b>Funktionen</b> die Objekte auf Objekte abbilden,\n",
-    "* <b>Prädikate</b> die Objekte oder Objekt-kombinationen auf einen Wahrheitswert abbilden,\n",
-    "* <b>Quantoren</b> mit denen man Variablen einführt und Aussagen über alle Objekte machen kann, oder die Existenz eines Objekts zusichert\n"
+    "* **Objekte**\n",
+    "* **Konstanten** und **Variablen** die Objekte darstellen,\n",
+    "* **Funktionen** die Objekte auf Objekte abbilden,\n",
+    "* **Prädikate** die Objekte oder Objekt-kombinationen auf einen Wahrheitswert abbilden,\n",
+    "* **Quantoren** mit denen man Variablen einführt und Aussagen über alle Objekte machen kann, oder die Existenz eines Objekts zusichert"
    ]
   },
   {
@@ -1361,15 +1350,15 @@
    "source": [
     "\n",
     "Erläuterung:\n",
-    "* ```2+2 < 5``` ist eine Aussage\n",
-    "* ```2``` und ```5``` sind Konstanten: sie stellen keinen Wahrheitswert dar, sondern ein Objekt (hier eine Zahl)\n",
-    "* ```+``` ist eine Funktion: sie bekommt Objekte als Parameter und stellt ein Objekt dar. ```2+2``` stellt die Zahl ```4``` dar.\n",
-    "*  ```x < 5``` falls der Wert von $x$ nicht bestimmt ist, ist dies keine Aussage, der Wahrheitswert hängt von dem Wert der Variable ```x``` ab\n",
-    "* ```x < 5``` ist ein <b>Prädikat</b>, für jeden möglichen Wert von ```x``` können wir bestimmen ob das Prädikat wahr oder falsch ist\n",
+    "* `2+2 < 5` ist eine Aussage\n",
+    "* `2` und `5` sind **Konstanten**: sie stellen keinen Wahrheitswert dar, sondern ein Objekt (hier eine Zahl)\n",
+    "* `+` ist eine **Funktion**: sie bekommt Objekte als Parameter und stellt ein Objekt dar. `2+2` stellt die Zahl `4` dar.\n",
+    "*  `x < 5` falls der Wert von $x$ nicht bestimmt ist, ist dies keine Aussage, der Wahrheitswert hängt von dem Wert der Variable `x` ab\n",
+    "* `x < 5` ist ein **Prädikat**, für jeden möglichen Wert von `x` können wir bestimmen ob das Prädikat wahr oder falsch ist\n",
     "* Prädikate sind parametrisierte Aussagen\n",
     "\n",
     "Weitere Beispiele:\n",
-    "* ```<``` ist ein <b>binäres Prädikat</b>, für jede Kombination an Werten können wir bestimmen ob das Prädikat wahr oder falsch ist:"
+    "* `<` ist ein **binäres Prädikat**, für jede Kombination an Werten können wir bestimmen ob das Prädikat wahr oder falsch ist:"
    ]
   },
   {
@@ -1382,12 +1371,12 @@
       "text/markdown": [
        "|x|y|res|\n",
        "|---|---|---|\n",
-       "|$1$|$1$|$\\mathit{FALSE}$|\n",
-       "|$1$|$2$|$\\mathit{TRUE}$|\n",
-       "|$1$|$3$|$\\mathit{TRUE}$|\n",
-       "|$2$|$1$|$\\mathit{FALSE}$|\n",
-       "|$2$|$2$|$\\mathit{FALSE}$|\n",
-       "|$2$|$3$|$\\mathit{TRUE}$|\n"
+       "|1|1|FALSE|\n",
+       "|1|2|TRUE|\n",
+       "|1|3|TRUE|\n",
+       "|2|1|FALSE|\n",
+       "|2|2|FALSE|\n",
+       "|2|3|TRUE|\n"
       ],
       "text/plain": [
        "x\ty\tres\n",
@@ -1413,15 +1402,16 @@
    "metadata": {},
    "source": [
     "# Freie Variablen\n",
-    "Die Formel ```x<5``` besteht formal gesehen aus:\n",
+    "\n",
+    "Die Formel `x<5` besteht formal gesehen aus:\n",
     "* einer logischen Variable $x$,\n",
     "* der Konstante $5$ die für die Zahl $5$ steht,\n",
     "* dem binären Prädikatensymbol $<$, hier in Infix-Notation, mit zwei Argumenten: $x$ und $5$. (In Präfix-Notation würde man $<(x,5)$ schreiben.)\n",
     "\n",
     "\n",
-    "Innerhalb von ```x<5``` ist $x$ eine freie Variable.\n",
+    "Innerhalb von `x<5` ist $x$ eine freie Variable.\n",
     "\n",
-    "In einer <b>geschlossenen</b> Formel der Prädikatenlogik müssen alle Variablen durch Quantoren gebunden werden."
+    "In einer **geschlossenen** Formel der Prädikatenlogik müssen alle Variablen durch Quantoren gebunden werden."
    ]
   },
   {
@@ -1429,13 +1419,14 @@
    "metadata": {},
    "source": [
     "# Quantoren\n",
+    "\n",
     "In der Prädikatenlogik gibt es zwei Quantoren:\n",
     "\n",
-    "* den <b>Existenzquantor</b> $\\exists$\n",
+    "* den **Existenzquantor** $\\exists$\n",
     "\n",
     "$\\exists x. P$ ist wahr, wenn es mindestens ein Objekt $o$ gibt, so dass wenn man $x$ durch $o$ in $P$ ersetzt die Formel (ohne den Quantor) wahr ist \n",
     "\n",
-    "* den <b>Allquantor</b> $\\forall$ (auch Universalquantor genannt)\n",
+    "* den **Allquantor** $\\forall$ (auch Universalquantor genannt)\n",
     "\n",
     "$\\forall x. P$ ist wahr wenn die Formel $P$ für alle möglichen Ersetzungen von $x$ durch ein Objekt $o$ wahr ist\n",
     "\n",
@@ -1576,19 +1567,16 @@
     "\n",
     "Diese beiden Definitionen übernehmen wir wortwörtlich aus der Aussagenlogik:\n",
     "\n",
-    "* Zwei Formeln $\\phi$ und $\\psi$ sind <b>äquivalent</b> gdw sie die selben Modelle haben.\n",
-    " * Wir schreiben dies als $\\phi \\equiv \\psi$.\n",
-    "     \n",
-    "* Eine Formel $\\psi$ ist eine <b>logische Schlussfolgerung</b> von $\\phi$, wenn alle Modelle von $\\phi$ auch Modelle von $\\psi$ sind.\n",
-    " * Wir schreiben dies als $\\phi \\models \\psi$.\n",
-    "     "
+    "* Zwei Formeln $\\phi$ und $\\psi$ sind **äquivalent** gdw sie die selben Modelle haben.\n",
+    "    * Wir schreiben dies als $\\phi \\equiv \\psi$.\n",
+    "* Eine Formel $\\psi$ ist eine **logische Schlussfolgerung** von $\\phi$, wenn alle Modelle von $\\phi$ auch Modelle von $\\psi$ sind.\n",
+    "    * Wir schreiben dies als $\\phi \\models \\psi$."
    ]
   },
   {
    "cell_type": "markdown",
    "metadata": {},
    "source": [
-    "\n",
     "Das Konzept der Modelle ist aber in Prädikatenlogik komplizierter:\n",
     "\n",
     "* eine Menge an Objekten muss ausgewählt werden\n",
@@ -1607,26 +1595,25 @@
     "\n",
     "Mit diesen beiden Gesetzen kann man die Negation zu den atomaren Aussagen und Prädikaten verschieben:\n",
     "* $\\neg \\exists x. P  \\equiv \\forall x. \\neg P$\n",
-    " * $\\neg \\exists x. (x>0 \\wedge x<0)  \\equiv \\forall x. \\neg (x>0 \\wedge x<0) \\equiv$ $\\forall x. (x\\leq 0 \\vee x\\geq 0)$\n",
+    "    * $\\neg \\exists x. (x>0 \\wedge x<0)  \\equiv \\forall x. \\neg (x>0 \\wedge x<0) \\equiv$ $\\forall x. (x\\leq 0 \\vee x\\geq 0)$\n",
     "\n",
     "* $\\neg \\forall x. P  \\equiv \\exists x. \\neg P$\n",
     "\n",
     "Diese Gesetze erlauben es einem Quantoren zu vertauschen:\n",
     "* $\\forall x.( \\forall y. P)  \\equiv \\forall y.( \\forall x. P)$ \n",
-    " * Beispiel: $\\forall x. (\\forall y. (x \\leq y \\vee x>y)) \\equiv \\forall y. (\\forall x. (x \\leq y \\vee x>y))$\n",
+    "    * Beispiel: $\\forall x. (\\forall y. (x \\leq y \\vee x>y)) \\equiv \\forall y. (\\forall x. (x \\leq y \\vee x>y))$\n",
     "\n",
     "* $\\exists x.( \\exists y. P)  \\equiv \\exists y.( \\exists x. P)$\n",
-    " * Beispiel: $\\exists x. (\\exists y. (x+y=0)) \\equiv \\exists y. (\\exists x. (x+y=0))$\n"
+    "    * Beispiel: $\\exists x. (\\exists y. (x+y=0)) \\equiv \\exists y. (\\exists x. (x+y=0))$"
    ]
   },
   {
    "cell_type": "markdown",
    "metadata": {},
    "source": [
-    "\n",
     "Aber Achtung:\n",
     "* $\\forall x.( \\exists y. P)  \\not\\equiv \\exists y.( \\forall x. P)$\n",
-    " * Beispiel: $\\forall x. (\\exists y. (y > x)) \\not\\equiv \\exists y. (\\forall x. (y > x)$"
+    "    * Beispiel: $\\forall x. (\\exists y. (y > x)) \\not\\equiv \\exists y. (\\forall x. (y > x)$"
    ]
   },
   {
@@ -1635,47 +1622,45 @@
    "source": [
     "# Werkzeuge für Logik\n",
     "    \n",
-    "* SAT Solver: Erfüllbarkeit von Aussagenlogik prüfen (miniSAT, glucose, lingeling, Sat4j,...)\n",
-    "* SMT Solver: Erfüllbarkeit von Prädikatenlogik mit Theorien (Bit-Vektoren,...): Z3 von Microsoft\n",
-    "* Beweiser: Atelier-B, Rodin, Isabelle, Coq, Vampire,...\n",
+    "* SAT Solver: Erfüllbarkeit von Aussagenlogik prüfen (miniSAT, glucose, lingeling, Sat4j, ...)\n",
+    "* SMT Solver: Erfüllbarkeit von Prädikatenlogik mit Theorien (Bit-Vektoren, ...): Z3 von Microsoft\n",
+    "* Beweiser: Atelier-B, Rodin, Isabelle, Coq, Vampire, ...\n",
     "* Model-Finder, Constraint Solver: ProB, Alloy, IDP, ...\n",
     "* Programmiersprache: Prolog\n",
     "\n",
     "Einige Anwendungen dieser Werkzeuge:  \n",
     "* Hardware Verifikation\n",
-    "* schwere Probleme lösen (Eclipse/Linux Abhängigkeiten,...)\n",
-    " * https://wiki.eclipse.org/Equinox_P2_Resolution\n",
-    "* Software Verifikation, Fehler finden (NullPointer Exception, Overflows), Windows Driver Verification (SLAM2,...)\n",
-    " * SLAM2: https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/slam-sdvrpcav2010.pdf\n",
-    " * https://www.microsoft.com/en-us/research/publication/slam-and-static-driver-verifier-technology-transfer-of-formal-methods-inside-microsoft/\n",
+    "* schwere Probleme lösen (Abhängigkeiten in Eclipse/Linux, ...)\n",
+    "    * https://wiki.eclipse.org/Equinox_P2_Resolution\n",
+    "* Software Verifikation, Fehler finden (NullPointerException, Overflows), Windows Driver Verification (SLAM2, ...)\n",
+    "    * SLAM2: https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/slam-sdvrpcav2010.pdf\n",
+    "    * https://www.microsoft.com/en-us/research/publication/slam-and-static-driver-verifier-technology-transfer-of-formal-methods-inside-microsoft/\n",
     "* Stellwerkprüfung (Prover Technologies, ...)\n",
     "* Datenvalidierung (ProB bei Siemens, Alstom, Thales; Paris L1)\n",
-    "* Software Entwicklung (AtelierB, Paris L14, L1, ....: seit 1999 kein einziger Bug !)\n",
-    "\n"
+    "* Software Entwicklung (AtelierB, Paris L14, L1, ...: seit 1999 kein einziger Bug!)"
    ]
   },
   {
    "cell_type": "markdown",
    "metadata": {},
    "source": [
-    "\n",
     "# Andere Logiken\n",
     "    \n",
     "* Aussagenlogik und Prädikatenlogik sind klassische zweiwertige Logiken\n",
     "\n",
-    "* sie sind <b>monoton</b> wenn $\\phi \\models \\psi$ dann gilt für alle $\\rho$: $\\phi \\wedge \\rho \\models \\psi$\n",
+    "* sie sind **monoton** wenn $\\phi \\models \\psi$ dann gilt für alle $\\rho$: $\\phi \\wedge \\rho \\models \\psi$\n",
     "\n",
     "* Aussagenlogik ist entscheidbar\n",
     "* Prädikatenlogik ist semi-entscheidbar: wenn $\\phi \\models \\psi$ kann man einen Beweis finden\n",
-    " * Gödelscher Vollständigkeitssatz  https://de.wikipedia.org/wiki/Gödelscher_Vollständigkeitssatz\n",
+    "    * [Gödelscher Vollständigkeitssatz](https://de.wikipedia.org/wiki/Gödelscher_Vollständigkeitssatz)\n",
     "* (Anmerkung: Wir werden später in der Vorlesung das Konzept der Entscheidbarkeit formal beschreiben)\n",
     "* reine Prädikatenlogik ist nicht ausreichend um Arithmetik zu axiomatisieren\n",
-    " * Gödelscher Unvollständigkeitssatz https://de.wikipedia.org/wiki/Gödelscher_Unvollständigkeitssatz\n",
+    "    * [Gödelscher Unvollständigkeitssatz](https://de.wikipedia.org/wiki/Gödelscher_Unvollständigkeitssatz)\n",
     "\n",
     "Nicht-klassische Logiken:\n",
-    "* es gibt Intuitionistische Logik:  Beweis durch Widerspruch dort nicht erlaubt\n",
-    "* es gibt dreiwertige Logiken ( $2/0=1 \\wedge 1=2$ )\n",
-    "* es gibt die Fuzzy Logik, modale Logiken, temporale Logiken,...\n",
+    "* es gibt Intuitionistische Logik: Beweis durch Widerspruch dort nicht erlaubt\n",
+    "* es gibt dreiwertige Logiken ($2/0=1 \\wedge 1=2$)\n",
+    "* es gibt die Fuzzy Logik, modale Logiken, temporale Logiken, ...\n",
     "* nicht-monotone Logiken"
    ]
   },
@@ -1683,7 +1668,6 @@
    "cell_type": "markdown",
    "metadata": {},
    "source": [
-    "\n",
     "# Zusammenfassung Logik\n",
     "    \n",
     "* Formeln der Aussagenlogik und Prädikatenlogik\n",
@@ -1704,14 +1688,14 @@
     "## Unterschied zwischen $\\equiv$ und $\\Leftrightarrow$\n",
     "\n",
     "* $\\Leftrightarrow$ is ein Junktor und wird verwendet um Formeln der Aussagenlogik zu erstellen\n",
-    " * wenn $\\phi$ und $\\psi$ Formeln der Aussagenlogik sind, dann ist $\\phi \\Leftrightarrow \\psi$  also auch eine Formel der Aussagenlogik\n",
+    "    * wenn $\\phi$ und $\\psi$ Formeln der Aussagenlogik sind, dann ist $\\phi \\Leftrightarrow \\psi$  also auch eine Formel der Aussagenlogik\n",
     "* $\\equiv$ is *kein* Junktor und kann *nicht* in Formeln der Aussagenlogik auftauchen\n",
     "* Mit $\\equiv$ trifft man mathematische Aussagen über zwei Formeln.\n",
     "\n",
     "Es gilt aber folgendes Theorem:\n",
     "Seien $\\phi$ und $\\psi$ beliebige Formeln der Aussagenlogik.\n",
     "Dann gilt:\n",
-    "* $\\phi \\equiv \\psi$ gdw die Formel $\\phi \\Leftrightarrow \\psi$ eine Tautologie ist.\n"
+    "* $\\phi \\equiv \\psi$ gdw die Formel $\\phi \\Leftrightarrow \\psi$ eine Tautologie ist."
    ]
   },
   {
@@ -1731,10 +1715,10 @@
       "text/markdown": [
        "|p|q|ODER|IMPL|EQUIV|\n",
        "|---|---|---|---|---|\n",
-       "|$\\mathit{FALSE}$|$\\mathit{FALSE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|\n",
-       "|$\\mathit{FALSE}$|$\\mathit{TRUE}$|$\\mathit{FALSE}$|$\\mathit{FALSE}$|$\\mathit{TRUE}$|\n",
-       "|$\\mathit{TRUE}$|$\\mathit{FALSE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|\n",
-       "|$\\mathit{TRUE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|\n"
+       "|FALSE|FALSE|TRUE|TRUE|TRUE|\n",
+       "|FALSE|TRUE|FALSE|FALSE|TRUE|\n",
+       "|TRUE|FALSE|TRUE|TRUE|TRUE|\n",
+       "|TRUE|TRUE|TRUE|TRUE|TRUE|\n"
       ],
       "text/plain": [
        "p\tq\tODER\tIMPL\tEQUIV\n",
@@ -1751,9 +1735,9 @@
    ],
    "source": [
     ":table {p,q,ODER,IMPL,EQUIV| p:BOOL & q:BOOL &\n",
-    "                            ODER=bool(p=TRUE ∨ ¬(q=TRUE)) & // 𝑝∨¬𝑞\n",
-    "                            IMPL = bool(q=TRUE ⇒ p=TRUE) &  // 𝑞⇒p\n",
-    "                            EQUIV=bool((ODER=TRUE) ⇔ (IMPL=TRUE))}"
+    "                             ODER = bool(p=TRUE ∨ ¬(q=TRUE)) & // 𝑝∨¬𝑞\n",
+    "                             IMPL = bool(q=TRUE ⇒ p=TRUE) &    // 𝑞⇒p\n",
+    "                             EQUIV = bool((ODER=TRUE) ⇔ (IMPL=TRUE))}"
    ]
   },
   {
@@ -1774,10 +1758,10 @@
       "text/markdown": [
        "|p|q|ODER|UND|EQUIV|\n",
        "|---|---|---|---|---|\n",
-       "|$\\mathit{FALSE}$|$\\mathit{FALSE}$|$\\mathit{FALSE}$|$\\mathit{FALSE}$|$\\mathit{TRUE}$|\n",
-       "|$\\mathit{FALSE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|$\\mathit{FALSE}$|$\\mathit{FALSE}$|\n",
-       "|$\\mathit{TRUE}$|$\\mathit{FALSE}$|$\\mathit{TRUE}$|$\\mathit{FALSE}$|$\\mathit{FALSE}$|\n",
-       "|$\\mathit{TRUE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|$\\mathit{TRUE}$|\n"
+       "|FALSE|FALSE|FALSE|FALSE|TRUE|\n",
+       "|FALSE|TRUE|TRUE|FALSE|FALSE|\n",
+       "|TRUE|FALSE|TRUE|FALSE|FALSE|\n",
+       "|TRUE|TRUE|TRUE|TRUE|TRUE|\n"
       ],
       "text/plain": [
        "p\tq\tODER\tUND\tEQUIV\n",
@@ -1794,9 +1778,9 @@
    ],
    "source": [
     ":table {p,q,ODER,UND,EQUIV| p:BOOL & q:BOOL &\n",
-    "                            ODER=bool(p=TRUE ∨ q=TRUE) & // 𝑝∨𝑞\n",
+    "                            ODER = bool(p=TRUE ∨ q=TRUE) & // 𝑝∨𝑞\n",
     "                            UND = bool(p=TRUE & q=TRUE) &  // p&q\n",
-    "                            EQUIV=bool((ODER=TRUE) ⇔ (UND=TRUE))}"
+    "                            EQUIV = bool((ODER=TRUE) ⇔ (UND=TRUE))}"
    ]
   },
   {
@@ -1809,23 +1793,15 @@
     "Das Gleiche gilt für diese beiden Symbole:\n",
     "\n",
     "* $\\Rightarrow$ is ein Junktor und wird verwendet um Formeln der Aussagenlogik zu erstellen\n",
-    " * wenn $\\phi$ und $\\psi$ Formeln der Aussagenlogik sind, dann ist $\\phi \\Rightarrow \\psi$  also auch eine Formel der Aussagenlogik\n",
+    "    * wenn $\\phi$ und $\\psi$ Formeln der Aussagenlogik sind, dann ist $\\phi \\Rightarrow \\psi$ also auch eine Formel der Aussagenlogik\n",
     "* $\\models$ is *kein* Junktor und kann *nicht* in Formeln der Aussagenlogik auftauchen\n",
     "* Mit $\\models$ trifft man mathematische Aussagen über zwei Formeln.\n",
     "\n",
     "Es gilt aber folgendes Theorem:\n",
     "Seien $\\phi$ und $\\psi$ beliebige Formeln der Aussagenlogik.\n",
     "Dann gilt:\n",
-    "* $\\phi \\models \\psi$ gdw die Formel $\\phi \\Rightarrow \\psi$ eine Tautologie ist.\n",
-    "\n"
+    "* $\\phi \\models \\psi$ gdw die Formel $\\phi \\Rightarrow \\psi$ eine Tautologie ist."
    ]
-  },
-  {
-   "cell_type": "code",
-   "execution_count": null,
-   "metadata": {},
-   "outputs": [],
-   "source": []
   }
  ],
  "metadata": {
@@ -1842,5 +1818,5 @@
   }
  },
  "nbformat": 4,
- "nbformat_minor": 2
+ "nbformat_minor": 4
 }
-- 
GitLab