add slide

01876a8a · Michael Leuschel · cb1b2aad · 01876a8a
Commit 01876a8a authored 5 years ago by Michael Leuschel
--- a/info4/kapitel-0/Logik.ipynb
+++ b/info4/kapitel-0/Logik.ipynb
@@ -1311,6 +1311,30 @@
    "x*x = 10000"
   ]
  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "# Logische Äquivalenz, Schlussfolgerung\n",
+    "\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",
+    "     \n",
+    "Das Konzept der Modelle ist aber in Prädikatenlogik komplizierter:\n",
+    "\n",
+    "* eine Menge an Objekten muss ausgewählt werden\n",
+    "* die Konstanten und Funktionen müssen den Objekten zugeordnet werden\n",
+    "* die Prädikate müssen Objekte auf Wahrheitswerte abbilden; Aussagen sind ein Spezialfall von Prädikaten.\n",
+    "* (manchmal sind bestimmte Symbole vordefiniert, wie $<$, $+$ oder $5$)\n",
+    "\n",
+    "Dies ist nicht Inhalt dieser Vorlesung."
+   ]
+  },
  {
   "cell_type": "markdown",
   "metadata": {},
@@ -1391,8 +1415,8 @@
   "cell_type": "markdown",
   "metadata": {},
   "source": [
-    "Auswertung der Formeln erfolgte mit\n",
-    "![ProB](../presentations/img/prob_logo.png)"
+    "Auswertung der Formeln erfolgte mit dem [Jupyter kernel](https://gitlab.cs.uni-duesseldorf.de/general/stups/prob2-jupyter-kernel) für [ProB](https://www3.hhu.de/stups/prob)\n",
+    "![ProB](img/prob_logo.png)"
   ]
  },
  {

 %% Cell type:markdown id: tags:

 # Vorlesung 0 - Teil 1 Logik

 Grundlagen der Logik und Mengentheorie sind nicht im Skript.
 Hier definieren wir einige Grundlagen und Notationen die im Skript verwendet werden.
 Ein gutes Verständnis dieser Grundlagen und Notationen ist für das Verständnis des Skripts, aber auch anderer Teile der Informatik unumgänglich.

 %% Cell type:markdown id: tags:

 # Was ist Logik?

 Quelle [https://de.wikipedia.org/wiki/Logik]:
 * vernünftiges Schlussfolgern, Denklehre
 * In der Logik wird die Struktur von Argumenten im Hinblick auf ihre Gültigkeit untersucht, unabhängig vom Inhalt der Aussagen
 * Traditionell ist die Logik ein Teil der Philosophie.
 * Seit dem 20. Jahrhundert versteht man unter Logik überwiegend symbolische Logik, die auch als grundlegende Strukturwissenschaft, z. B. innerhalb der Mathematik und der theoretischen Informatik, behandelt wird.

 %% Cell type:markdown id: tags:

 # Warum Logik studieren?

 * Hardware: logische Schaltkreise
 * Wissensdarstellung und intelligentes Denken: künstliche Intelligenz, deklarative Darstellung von Wissen, semantisches Web, ...
 * Überlegungen über Programme: Verifikation, statische Programmanalyse, Programmoptimierung,...
 * Universale Vorrichtung zur Berechnung: Datenbanken, logische Programmierung, ...
 * Grundlage der Mathematik und auch der theoretischen Informatik
 * Halpern et al. On the Unusual Effectiveness of Logic in Computer Science. https://www.cs.cmu.edu/~rwh/papers/unreasonable/basl.pdf
 * 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.```

 %% Cell type:markdown id: tags:

 # Welche Logik studieren?
 * Aussagenlogik
 * Prädikatenlogik der ersten Stufe (FOL - First Order Logic)
 * Logik höherer Stufe (HOL - Higher Order Logic)
 * eine temporale Logik
 * eine mehrwertige Logik oder gar Fuzzy Logik
 * Relevanzlogik, lineare Logik
 * eine nichtmonotone Logik

 Wir werden die klassische, zweiwertige, monotone Aussagenlogik
  und Prädikatenlogik studieren (zusammen mit Mengentheorie).

 %% Cell type:markdown id: tags:

 # Aussagenlogik

 Eine Aussage ist endweder wahr (TRUE) oder falsch (FALSE).

 Die Logik interessiert sich weniger ob Aussagen wie wahr oder falsch sind, sondern mehr um Zusammenhänge zwischen möglichen Wahrheitswerten verschiedener Aussagen und Formeln.

 Einige Aussagen haben manchmal vordefinierte Wahrheitswerte.
 Wir zum Beispiel benutzen Arithmetik und Mengetheorie in unseren logischen Formeln, ohne diese selber in Logik zu formalisieren.

 Hier sind ein paar Aussagen in Arithmetik:

 %% Cell type:code id: tags:

 ``` prob
 2>1
 ```

 %% Output

    $\mathit{TRUE}$
    TRUE

 %% Cell type:code id: tags:

 ``` prob
 1+1 = 2
 ```

 %% Output

    $\mathit{TRUE}$
    TRUE

 %% Cell type:code id: tags:

 ``` prob
 2<1
 ```

 %% Output

    $\mathit{FALSE}$
    FALSE

 %% Cell type:markdown id: tags:

 # Junktoren und Formeln

 Jede Aussage ist auch eine Formel.
 Mit den Junktoren kann man Aussagen und Formeln zu grösseren Formeln der Aussagenlogik kombinieren.

 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:

 %% Cell type:code id: tags:

 ``` prob
 ¬(2<1)
 ```

 %% Output

    $\mathit{TRUE}$
    TRUE

 %% Cell type:markdown id: tags:

 Die Konjunktion ```F ∧ G``` von zwei Formeln ist wahr gdw beide Formeln wahr sind:

 %% Cell type:code id: tags:

 ``` prob
 2>1 ∧ 1>0
 ```

 %% Output

    $\mathit{TRUE}$
    TRUE

 %% Cell type:markdown id: tags:

 Die Disjunktion ```F ∨ G``` von zwei Formeln ist wahr gdw  mindestes eine der beiden Formeln wahr sind:

 %% Cell type:code id: tags:

 ``` prob
 2>1 ∨ 1>2
 ```

 %% Output

    $\mathit{TRUE}$
    TRUE

 %% Cell type:markdown id: tags:

 Die Implikation ```F ⇒ G``` von zwei Formeln ist wahr wenn entweder beide Formeln wahr sind oder die erste Formel F falsch ist:

 %% Cell type:code id: tags:

 ``` prob
 2>1 ⇒ 3>1
 ```

 %% Output

    $\mathit{TRUE}$
    TRUE

 %% Cell type:code id: tags:

 ``` prob
 2<1 ⇒ 1+1 = 5
 ```

 %% Output

    $\mathit{TRUE}$
    TRUE

 %% Cell type:markdown id: tags:

 Die Äquivalenz ```F ⇔ G``` von zwei Formeln ist wahr wenn entweder beide Formeln wahr sind oder beide Formeln falsch sind:

 %% Cell type:code id: tags:

 ``` prob
 1=2 ⇔ 2=1
 ```

 %% Output

    $\mathit{TRUE}$
    TRUE

 %% Cell type:code id: tags:

 ``` prob
 1=3 ⇔ 1=1024
 ```

 %% Output

    $\mathit{TRUE}$
    TRUE

 %% Cell type:code id: tags:

 ``` prob
 1=1 ⇔ 2=3
 ```

 %% Output

    $\mathit{FALSE}$
    FALSE

 %% Cell type:markdown id: tags:

 ## Prioritäten

 Anmerkung: Wir nehmen an, dass $\neg$ am stärksten bindet, dann kommen $\wedge$, $\vee$, $\Rightarrow$ und schließlich ⇔.

 Die Formel $(p \vee (\neg p \wedge q)$ steht also für $(p \vee (\neg(p) \wedge q)$.

 Eine Formel kann man immer als einen Baum sehen

 %% Cell type:code id: tags:

 ``` prob
 :pref OPTIMIZE_AST=FALSE
 ```

 %% Output

    Preference changed: OPTIMIZE_AST = FALSE

 %% Cell type:code id: tags:

 ``` prob
 :dot formula_tree (2>3 ⇒ 4>1) ⇔ ¬(5<1)
 ```

 %% Output


    <Dot visualization: formula_tree [(2>3 => 4>1) <=> not(5<1)]>

 %% Cell type:markdown id: tags:

 # Wahrheitstabellen

 Die Bedeutung dieser Junktoren kann man in folgender Wahrheitstabelle zusammenfassen:

 ![ProB](./img/wahrheitstabelle.png)

 Wie berechnet man damit den Wahrheitswert einer Formel wie $(p \vee (\neg p \wedge q)$?


 Man braucht erst die Wahrheitswerte für die atomaren Aussagen $p$ und $q$.
 Diese Information nennt man eine <b>Interpretation</b> für die Formel.
 Die Formel oben hat 4 Interpretationen, da $p$ und $q$ jeweils wahr oder falsch sein können.

 Mit einer Interpretation kann man nun
 * den Wahrheitswert aller (atomaren) Aussagen berechnen
 * und mit der Wahrheitstabelle dann den Wert von immer grösseren Unterformeln berechnen.

 Beispiel:
 Sei $i$ =  $\{p\mapsto TRUE,q\mapsto FALSE\}$ eine Interpretation für die Formel $(p \vee (\neg p \wedge q)$.

 * Schritt 1: alle Aussagen berechnen: $(TRUE \vee (\neg TRUE \wedge FALSE)$
 * Schritt 2: $\neg TRUE = FALSE$: $(TRUE \vee (FALSE \wedge FALSE)$
 * Schritt 3: $FALSE \wedge FALSE = FALSE$: $(TRUE \vee FALSE)$
 * Schritt 3: $TRUE \vee FALSE = TRUE$: $TRUE$

 Unter der Interpretation $i$ ist die Formel $(p \vee (\neg p \wedge q)$ wahr.
 Man nennt so eine Interpretation ein <b>Modell</b> für die Formel.

 * eine Interpretation $i$ so dass $i(\phi)={\color{olive} TRUE}$ ist ein <b>Modell</b> für $\phi$
 * eine Formel $\phi$ die mindestens ein Modell hat heißt <b>erfüllbar</b>
 * eine Formel $\phi$ wo alle Interpretationen auch Modelle sind wird eine <b>Tautologie</b> genannt
 * eine Formel ohne Modell heißt <b>unerfüllbar</b> oder ein Widerspruch



 Die Interpretation $i'$ =  $\{p\mapsto FALSE,q\mapsto FALSE\}$ ist kein Modell von $(p \vee (\neg p \wedge q)$.
 Die Formel ist also keine Tautologie, aber erfüllbar.

 Die Formel $p \vee \neg p$ ist eine Tautologie: alle Interpretation machen die Formel wahr.
 $p \wedge \neg p$ hingegen ist ein Widerspruch und hat kein Modell.


 # Äquivalenz von Formeln

 Zwei Formeln sind <b>äquivalent</b> gdw sie die selben Modelle haben.

 $(p \vee (\neg p \wedge q)$ ist zum Beispiel äquivalent zu $p \vee q$.
 Hier stellen wir die Interpretationen und Modelle tabellarisch dar:

 %% Cell type:code id: tags:

 ``` prob
 :table {p,q,F1,F2| p:BOOL & q:BOOL &
                   F1=bool(p=TRUE ∨ (¬(p=TRUE) ∧ q=TRUE)) & // p ∨ (¬p ∧ q)
                   F2=bool(p=TRUE ∨ q=TRUE)                 // p ∨ q
                   }
 ```

 %% Output

    |p|q|F1|F2|
    |---|---|---|---|
    |$\mathit{FALSE}$|$\mathit{FALSE}$|$\mathit{FALSE}$|$\mathit{FALSE}$|
    |$\mathit{FALSE}$|$\mathit{TRUE}$|$\mathit{TRUE}$|$\mathit{TRUE}$|
    |$\mathit{TRUE}$|$\mathit{FALSE}$|$\mathit{TRUE}$|$\mathit{TRUE}$|
    |$\mathit{TRUE}$|$\mathit{TRUE}$|$\mathit{TRUE}$|$\mathit{TRUE}$|
    p	q	F1	F2
    FALSE	FALSE	FALSE	FALSE
    FALSE	TRUE	TRUE	TRUE
    TRUE	FALSE	TRUE	TRUE
    TRUE	TRUE	TRUE	TRUE

 %% Cell type:markdown id: tags:

 Wir schreiben diesen Tatbestand als $(p \vee (\neg p \wedge q) \equiv p \vee q$.

 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.

 $\equiv$ ist eine Relation zwischen logischen Formeln.
 $\equiv$ ist transitiv und kommutativ.

 # Wichtige Äquivalenzen
 Für alle Formeln $\phi, \psi$ gilt:
 * $\phi \Rightarrow \psi \equiv (\neg \phi) \vee \psi$
 * $\phi \Leftrightarrow \psi \equiv (\phi \Rightarrow \psi) \wedge (\psi \Rightarrow \phi)$
 * $\neg \neg \phi \equiv \phi$
 * $\neg(\phi \wedge \psi) \equiv (\neg \phi) \vee (\neg \psi)$  (De Morgan)
 * $\neg(\phi \vee \psi) \equiv (\neg \phi) \wedge (\neg \psi)$  (De Morgan)
 * $\phi \wedge \psi \equiv \psi \wedge \phi$
 * $\phi \vee \psi \equiv \psi \vee \phi$

 Hier illustrieren wir die Äquivalenz $\neg(\phi \vee \psi) \equiv (\neg \phi) \wedge (\neg \psi)$ als Wahrheitstabelle:

 %% Cell type:code id: tags:

 ``` prob
 :table {p,q,ODER,NODER,NUND,np,nq| p:BOOL & q:BOOL & np = bool(¬(p=TRUE)) & nq = bool(¬(q=TRUE)) &
                            ODER=bool(p=TRUE ∨ q=TRUE) &
                            NODER = bool(¬(ODER=TRUE)) &
                            NUND=bool((np=TRUE) ∧ (nq=TRUE))}
 ```

 %% Output

    |p|q|ODER|NODER|NUND|np|nq|
    |---|---|---|---|---|---|---|
    |$\mathit{FALSE}$|$\mathit{FALSE}$|$\mathit{FALSE}$|$\mathit{TRUE}$|$\mathit{TRUE}$|$\mathit{TRUE}$|$\mathit{TRUE}$|
    |$\mathit{FALSE}$|$\mathit{TRUE}$|$\mathit{TRUE}$|$\mathit{FALSE}$|$\mathit{FALSE}$|$\mathit{TRUE}$|$\mathit{FALSE}$|
    |$\mathit{TRUE}$|$\mathit{FALSE}$|$\mathit{TRUE}$|$\mathit{FALSE}$|$\mathit{FALSE}$|$\mathit{FALSE}$|$\mathit{TRUE}$|
    |$\mathit{TRUE}$|$\mathit{TRUE}$|$\mathit{TRUE}$|$\mathit{FALSE}$|$\mathit{FALSE}$|$\mathit{FALSE}$|$\mathit{FALSE}$|
    p	q	ODER	NODER	NUND	np	nq
    FALSE	FALSE	FALSE	TRUE	TRUE	TRUE	TRUE
    FALSE	TRUE	TRUE	FALSE	FALSE	TRUE	FALSE
    TRUE	FALSE	TRUE	FALSE	FALSE	FALSE	TRUE
    TRUE	TRUE	TRUE	FALSE	FALSE	FALSE	FALSE

 %% Cell type:markdown id: tags:

 # Logisches Schließen
 Wenn $p \wedge q$ gilt, dann ist $p$ eine logische Konsequenz (Schlussfolgerung) von $p\wedge q$.
 * Wir schreiben dies als $p \wedge q \models p$
 * Formal bedeutet dies, dass alle Modelle von $q \wedge p$ auch Modelle von $p$ sind.

 Die Tabelle zeigt, dass $p \Leftrightarrow q \models p \Rightarrow q$. Die Formeln sind nicht äquivalent.

 %% Cell type:code id: tags:

 ``` prob
 :table {p,q,F1,F2| p:BOOL & q:BOOL & F1=bool(p=TRUE ⇔ q=TRUE) & F2=bool(p=TRUE ⇒ q=TRUE)}
 ```

 %% Output

    |p|q|F1|F2|
    |---|---|---|---|
    |$\mathit{FALSE}$|$\mathit{FALSE}$|$\mathit{TRUE}$|$\mathit{TRUE}$|
    |$\mathit{FALSE}$|$\mathit{TRUE}$|$\mathit{FALSE}$|$\mathit{TRUE}$|
    |$\mathit{TRUE}$|$\mathit{FALSE}$|$\mathit{FALSE}$|$\mathit{FALSE}$|
    |$\mathit{TRUE}$|$\mathit{TRUE}$|$\mathit{TRUE}$|$\mathit{TRUE}$|
    p	q	F1	F2
    FALSE	FALSE	TRUE	TRUE
    FALSE	TRUE	FALSE	TRUE
    TRUE	FALSE	FALSE	FALSE
    TRUE	TRUE	TRUE	TRUE

 %% Cell type:markdown id: tags:

 Wichtige logische Schlussfolgerungen}
 Für alle Formeln $\phi, \psi$ gilt:
 * $\phi \wedge \psi \models \phi$
 * $(\phi \Rightarrow \psi) \wedge \phi \models \psi$ (Modus Ponens)
 * $(\phi \Rightarrow \psi) \wedge \neg\psi \models \neg\phi$ (Modus Tollens)
 * $(\phi \Leftrightarrow \psi) \wedge \psi \models \phi$
 * $(\phi \Leftrightarrow \psi) \wedge \neg\psi \models \neg\phi$
 * Achtung $\phi \wedge \neg \phi \models \psi$ für beliebiges $\psi$ !

 %% Cell type:markdown id: tags:

 # Smullyan  - Einfaches Puzzle}

 Raymond Smullyan beschreibt in seinen Büchern eine Insel auf der es (nur) zwei Arten von Personen gibt:
 * Ritter die immer die Wahrheit sagen, und
 * Schurken die immer lügen.

 Hier ist ein Puzzle aus einem seiner Bücher:

 * X sagt: ```Y ist ein Ritter```
 * Y sagt: ```X und ich sind von einem unterschiedlichen Typ.```

 Können wir bestimmen ob X und Y Ritter oder Schurken sind?

 Schritt 1: was sind die Aussagen?
 * $X$: die Person X ist ein Ritter
 * $Y$: die Person Y ist ein Ritter

 Schritt 2: Übersetzung der Informationen in Aussagenlogik
 * $\mathit{X} \Leftrightarrow  \mathit{Y}$ ist die Übersetzung von:
 * X sagt: ```Y ist ein Ritter```
 * $\mathit{Y} \Leftrightarrow  (\mathit{X} \Leftrightarrow  \neg (\mathit{Y}))$ ist die Übersetzung von:
 * Y sagt: ```X und ich sind von einem unterschiedlichen Typ.```


 Schritt 3: Bestimmung der Modelle:

 %% Cell type:code id: tags:

 ``` prob
 :table {x,y,S1,S2,Puzzle | x:BOOL & y:BOOL &
                   S1=bool(x=TRUE ⇔ y=TRUE) &
                   S2=bool(y=TRUE ⇔ (x=TRUE ⇔ ¬(y=TRUE))) &
                   Puzzle=bool(S1=TRUE & S2=TRUE)}
 ```

 %% Output

    |x|y|S1|S2|Puzzle|
    |---|---|---|---|---|
    |$\mathit{FALSE}$|$\mathit{FALSE}$|$\mathit{TRUE}$|$\mathit{TRUE}$|$\mathit{TRUE}$|
    |$\mathit{FALSE}$|$\mathit{TRUE}$|$\mathit{FALSE}$|$\mathit{TRUE}$|$\mathit{FALSE}$|
    |$\mathit{TRUE}$|$\mathit{FALSE}$|$\mathit{FALSE}$|$\mathit{FALSE}$|$\mathit{FALSE}$|
    |$\mathit{TRUE}$|$\mathit{TRUE}$|$\mathit{TRUE}$|$\mathit{FALSE}$|$\mathit{FALSE}$|
    x	y	S1	S2	Puzzle
    FALSE	FALSE	TRUE	TRUE	TRUE
    FALSE	TRUE	FALSE	TRUE	FALSE
    TRUE	FALSE	FALSE	FALSE	FALSE
    TRUE	TRUE	TRUE	FALSE	FALSE

 %% Cell type:markdown id: tags:

 Unser Puzzle hat nur ein einziges Modell und beide Personen sind also Schurken.


 Ein typische fehlerhafte Übersetzung des Puzzles ist diese:

 * $\mathit{X} \Rightarrow  \mathit{Y}$ ist die Übersetzung von:
 * X sagt: ```Y ist ein Ritter```
 * $\mathit{Y} \Rightarrow  (\mathit{X} \Leftrightarrow  \neg (\mathit{Y}))$ ist die Übersetzung von:
 * Y sagt: ```X und ich sind von einem unterschiedlichen Typ.```

 %% Cell type:code id: tags:

 ``` prob
 :table {x,y,S1,S2,Puzzle | x:BOOL & y:BOOL &
                   S1=bool(x=TRUE ⇒ y=TRUE) &
                   S2=bool(y=TRUE ⇒ (x=TRUE ⇔ ¬(y=TRUE))) &
                   Puzzle=bool(S1=TRUE & S2=TRUE)}
 ```

 %% Output

    |x|y|S1|S2|Puzzle|
    |---|---|---|---|---|
    |$\mathit{FALSE}$|$\mathit{FALSE}$|$\mathit{TRUE}$|$\mathit{TRUE}$|$\mathit{TRUE}$|
    |$\mathit{FALSE}$|$\mathit{TRUE}$|$\mathit{TRUE}$|$\mathit{TRUE}$|$\mathit{TRUE}$|
    |$\mathit{TRUE}$|$\mathit{FALSE}$|$\mathit{FALSE}$|$\mathit{TRUE}$|$\mathit{FALSE}$|
    |$\mathit{TRUE}$|$\mathit{TRUE}$|$\mathit{TRUE}$|$\mathit{FALSE}$|$\mathit{FALSE}$|
    x	y	S1	S2	Puzzle
    FALSE	FALSE	TRUE	TRUE	TRUE
    FALSE	TRUE	TRUE	TRUE	TRUE
    TRUE	FALSE	FALSE	TRUE	FALSE
    TRUE	TRUE	TRUE	FALSE	FALSE

 %% Cell type:markdown id: tags:


 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.

 %% Cell type:markdown id: tags:

 # Beweis durch Widerspruch

 * Theorem: $\phi \models \psi$ genau dann wenn $\phi \wedge \neg \psi$ kein Modell hat


 Beweis (ist ein Äquivalenzbeweis auf Metaebene):

 * $\phi \models \psi$
 * $\Longleftrightarrow$ alle Modelle von $\phi$ sind auch Modelle von $\psi$ (per Definition von $\models$)
 * $\Longleftrightarrow$ in allen Modellen von $\phi$ hat $\neg \psi$ den Wahrheitswert falsch (per Definition von $\neg$)
 * $\Longleftrightarrow$ alle Modelle von $\phi$ sind kein Modell von $\phi \wedge \neg \psi$ (per Definition von $\wedge$)
 * $\Longleftrightarrow$ $\phi \wedge \neg \psi$ hat kein Modell  (da auch kein Modell von $\neg \phi$ ein Modell von $\phi  \wedge \neg \psi$ sein kann)

 Anwendung auf unser Puzzle:
 * Sei $\phi$ = $(\mathit{X} \Leftrightarrow  \mathit{Y}) \wedge (\mathit{Y} \Leftrightarrow  (\mathit{X} \Leftrightarrow  \neg (\mathit{Y})))$
 * Sei $\psi$ = $\neg X \wedge \neg Y$  (X und Y sind Schurken)
 * Wir haben $\phi \models \psi$ und
 * $\phi \wedge \neg \psi$ ist ein Widerspruch:

 %% Cell type:code id: tags:

 ``` prob
 :table {x,y,S1,S2,Puzzle,WS | x:BOOL & y:BOOL &
                   S1=bool(x=TRUE ⇔ y=TRUE) &
                   S2=bool(y=TRUE ⇔ (x=TRUE ⇔ ¬(y=TRUE))) &
                   Puzzle=bool(S1=TRUE & S2=TRUE) &
                   WS=bool(Puzzle=TRUE & not( not(x=TRUE) & not(y=TRUE)))}
 ```

 %% Output

    |x|y|S1|S2|Puzzle|WS|
    |---|---|---|---|---|---|
    |$\mathit{FALSE}$|$\mathit{FALSE}$|$\mathit{TRUE}$|$\mathit{TRUE}$|$\mathit{TRUE}$|$\mathit{FALSE}$|
    |$\mathit{FALSE}$|$\mathit{TRUE}$|$\mathit{FALSE}$|$\mathit{TRUE}$|$\mathit{FALSE}$|$\mathit{FALSE}$|
    |$\mathit{TRUE}$|$\mathit{FALSE}$|$\mathit{FALSE}$|$\mathit{FALSE}$|$\mathit{FALSE}$|$\mathit{FALSE}$|
    |$\mathit{TRUE}$|$\mathit{TRUE}$|$\mathit{TRUE}$|$\mathit{FALSE}$|$\mathit{FALSE}$|$\mathit{FALSE}$|
    x	y	S1	S2	Puzzle	WS
    FALSE	FALSE	TRUE	TRUE	TRUE	FALSE
    FALSE	TRUE	FALSE	TRUE	FALSE	FALSE
    TRUE	FALSE	FALSE	FALSE	FALSE	FALSE
    TRUE	TRUE	TRUE	FALSE	FALSE	FALSE

 %% Cell type:markdown id: tags:

 Widerspruchsbeweise werden wir oft im Verlauf der Vorlesung verwenden.

 Es gibt zwei andere Arten von Beweisen: Äquivalenzbeweise und Deduktionsbeweise.

 # Äquivalenzbeweis

 Hier schreiben wir die Schritte des Beweises oft in folgender Form auf:
 * $\phi_1$
 * $\Longleftrightarrow$ $\phi_2$
 * ...
 * $\Longleftrightarrow$ $\phi_k$

 wobei immer gilt $\phi_i \equiv \phi_{i+1}$.

 Wir haben per Transitivität von $\equiv$, dass $\phi_1 \equiv \phi_k$.
 Da $\equiv$ auch kommutativ ist, gilt der Beweis auch in die andere Richtung: $\phi_k \equiv \phi_1$.
 Wir haben sowohl $\phi_1 \models \phi_k$ als auch $\phi_k \models \phi_1$.

 Als kleines Beispiel beweisen wir, dass $\neg b \Rightarrow a \equiv a \vee b$:
 * $\neg b \Rightarrow a$
 * $\Longleftrightarrow$ $\neg \neg b \vee a$  (Regel: $\phi \Rightarrow \psi \equiv \neg \phi \vee \psi$)
 * $\Longleftrightarrow$ $b \vee a$ (Regel: $\neg \neg \phi \equiv \phi$))
 * $\Longleftrightarrow$ $a \vee b$ (Kommutativität von $\vee$)

 Anmerkung: im Skript verwenden wir $\Longleftrightarrow$ für Äquivalenzbeweise; die "präzise" logische Schreibweise wäre $\equiv$.

 %% Cell type:markdown id: tags:

 # Deduktiver Beweis

 Hier schreiben wir die Schritte des Beweises oft in folgender Form auf:
 * $\phi_1$
 * $\phi_2$
 *  ...
 * $\phi_k$

 wobei immer gilt $\phi_1 \wedge ...\phi_i \models \phi_{i+1}$.

 Wir haben per Transitiviät von $\models$, dass $\phi_1 \models \phi_k$.
 Aber im Gegensatz zum Äquivalenzbeweis gilt hier generell nicht $\phi_k \models phi_1$!
 Dieser Beweis kann nicht umgekehrt werden.

 Wir illustrieren dies Art der Beweisführung mit einem anderen kleinen Puzzle von unserer Insel der Ritter und Schurken:
 * A sagt: ``B ist ein Ritter''
 * B sagt: ``1+1=3''

 * $\phi_1$ = $A \Leftrightarrow B$ $\wedge$  $B \Leftrightarrow FALSE$
 * $\neg B$  (nach der zweiten Aussage $B \Leftrightarrow FALSE$ muss B ein Schurke sein)
 * $\neg A$  (nach der ersten Aussage $A \Leftrightarrow B$ muss A demnach auch ein Schurke sein)

 Wir haben per Transitiviät, dass $\phi_1 \models \neg A$, d.h. es folgt aus dem Puzzle, dass A ein Schurke ist.

 %% Cell type:markdown id: tags:

 # Aristoteles: Anfänge der Logik
 Syllogistik, einer Vorform der Prädikatenlogik
 * Alle Menschen sind sterblich.
 * Einige Menschen sind sterblich.
 * Alle Menschen sind unsterblich.
 * Einige Menschen sind unsterblich.

 Zusammenhang unter der Annahme, daß es mindestens einen Mensch gibt.
 (In die Aussagenlogik sind alle vier Aussagen unabhängig.)

 %% Cell type:markdown id: tags:

 # Prädikatenlogik

 Im Vergleich zur Aussagenlogik mit den Wahrheitswerten und Aussagen, gibt es in der Prädikatenlogik:
 * Objekte
 * <b>Konstanten</b> und <b>Variablen</b> die Objekte darstellen,
 * <b>Funktionen</b> die Objekte auf Objekte abbilden,
 * <b>Prädikate</b> die Objekte oder Objekt-kombinationen auf einen Wahrheitswert abbilden,
 * <b>Quantoren</b> mit denen man Variablen einführt und Aussagen über alle Objekte machen kann, oder die Existenz eines Objekts zusichert

 Erläuterung:
 * ```2+2 < 5``` ist eine Aussage
 * ```2``` und ```5``` sind Konstanten: sie stellen keinen Wahrheitswert dar, sondern ein Objekt (hier eine Zahl)
 * ```+``` ist eine Funktion: sie bekommt Objekte als Parameter und stellt ein Objekt dar. ```2+2``` stellt die Zahl ```4``` dar.
 *  ```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
 * ```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
 * Prädikate sind parametrisierte Aussagen

 Weitere Beispiele:
 * ```<``` 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:

 %% Cell type:code id: tags:

 ``` prob
 :table {x,y,res | x:1..2 & y:1..3 & res=bool(x<y)}
 ```

 %% Output

    |x|y|res|
    |---|---|---|
    |$1$|$1$|$\mathit{FALSE}$|
    |$1$|$2$|$\mathit{TRUE}$|
    |$1$|$3$|$\mathit{TRUE}$|
    |$2$|$1$|$\mathit{FALSE}$|
    |$2$|$2$|$\mathit{FALSE}$|
    |$2$|$3$|$\mathit{TRUE}$|
    x	y	res
    1	1	FALSE
    1	2	TRUE
    1	3	TRUE
    2	1	FALSE
    2	2	FALSE
    2	3	TRUE

 %% Cell type:markdown id: tags:

 # Freie Variablen
 Die Formel ```x<5``` besteht formal gesehen aus:
 * einer logischen Variable $x$,
 * der Konstante $5$ die für die Zahl $5$ steht,
 * 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.)


 Innerhalb von ```x<5``` ist $x$ eine freie Variable.

 In einer <b>geschlossenen</b> Formel der Prädikatenlogik müssen alle Variablen durch Quantoren gebunden werden.

 %% Cell type:markdown id: tags:

 # Quantoren
 In der Prädikatenlogik gibt es zwei Quantoren:

 * den <b>Existenzquantor</b> $\exists$

 $\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

 * den <b>Allquantor</b> $\forall$ (auch Universalquantor genannt)

 $\forall x. P$ ist wahr wenn die Formel $P$ für alle möglichen Ersetzungen von $x$ durch ein Objekt $o$ wahr ist

 * $\exists x. x<5$ ist eine geschlossene Formel (aka eine Aussage). Mit der Standardinterpretation von $<$ und $5$ ist diese Formel wahr; eine Lösung ist $x=4$.

 * $\forall x. x<5$ ist auch eine geschlossene Formel.
 Mit der Standardinterpretation von $<$ und $5$ ist diese Formel falsch. Ein Gegenbeispiel ist $x=5$.

 %% Cell type:code id: tags:

 ``` prob
 ∃x.(x<5)
 ```

 %% Output

    $\mathit{TRUE}$
    TRUE

 %% Cell type:markdown id: tags:

 In diesem Jupyter Notebook werden automatisch Existenzquantoren für alle offenen Variablen einegfügt:

 %% Cell type:code id: tags:

 ``` prob
 x<5
 ```

 %% Output

    $\mathit{TRUE}$
    
    **Solution:**
    * $\mathit{x} = 0$
    TRUE
    
    Solution:
    	x = 0

 %% Cell type:code id: tags:

 ``` prob
 x+20 = 30
 ```

 %% Output

    $\mathit{TRUE}$
    
    **Solution:**
    * $\mathit{x} = 10$
    TRUE
    
    Solution:
    	x = 10

 %% Cell type:code id: tags:

 ``` prob
 x*x = 10000
 ```

 %% Output

    $\mathit{TRUE}$
    
    **Solution:**
    * $\mathit{x} = -100$
    TRUE
    
    Solution:
    	x = −100

 %% Cell type:markdown id: tags:

+# Logische Äquivalenz, Schlussfolgerung
+
+Diese beiden Definitionen übernehmen wir wortwörtlich aus der Aussagenlogik:
+
+* Zwei Formeln $\phi$ und $\psi$ sind <b>äquivalent</b> gdw sie die selben Modelle haben.
+ * Wir schreiben dies als $\phi \equiv \psi$.
+
+* Eine Formel $\psi$ ist eine <b>logische Schlussfolgerung</b> von $\phi$, wenn alle Modelle von $\phi$ auch Modelle von $\psi$ sind.
+ * Wir schreiben dies als $\phi \models \psi$.
+
+Das Konzept der Modelle ist aber in Prädikatenlogik komplizierter:
+
+* eine Menge an Objekten muss ausgewählt werden
+* die Konstanten und Funktionen müssen den Objekten zugeordnet werden
+* die Prädikate müssen Objekte auf Wahrheitswerte abbilden; Aussagen sind ein Spezialfall von Prädikaten.
+* (manchmal sind bestimmte Symbole vordefiniert, wie $<$, $+$ oder $5$)
+
+Dies ist nicht Inhalt dieser Vorlesung.
+
+%% Cell type:markdown id: tags:
+
 # Quantoren: Einige Gesetze
 * $\neg \exists x. P  \equiv \forall x. \neg P$
 * $\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)$

 * $\neg \forall x. P  \equiv \exists x. \neg P$

 * $\forall x.( \forall y. P)  \equiv \forall y.( \forall x. P)$
 * $\forall x. (\forall y. (x \leq y \vee x>y)) \equiv \forall y. (\forall x. (x \leq y \vee x>y))$

 * $\forall x.( \exists y. P)  \not\equiv \exists y.( \forall x. P)$
 * $\forall x. (\exists y. (y > x)) \not\equiv \exists y. (\forall x. (y > x)$
 * $\exists x.( \exists y. P)  \equiv \exists y.( \exists x. P)$

 %% Cell type:code id: tags:

 ``` prob
 ```

 %% Cell type:markdown id: tags:

 # Werkzeuge für Logik

 * SAT Solver: Erfüllbarkeit von Aussagenlogik prüfen (miniSAT, glucose, lingeling, Sat4j,...)
 * SMT Solver: Erfüllbarkeit von Prädikatenlogik mit Theorien (Bit-Vektoren,...): Z3 von Microsoft
 * Beweiser: Atelier-B, Rodin, Isabelle, Coq, Vampire,...
 * Model-Finder, Constraint Solver: ProB, Alloy, IDP, ...
 * Programmiersprache: Prolog

 Einige Anwendungen dieser Werkzeuge:
 * Hardware Verifikation
 * schwere Probleme lösen (Eclipse/Linux Abhängigkeiten,...)
 * https://wiki.eclipse.org/Equinox_P2_Resolution
 * Software Verifikation, Fehler finden (NullPointer Exception, Overflows), Windows Driver Verification (SLAM2,...)
 * SLAM2: https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/slam-sdvrpcav2010.pdf
 * https://www.microsoft.com/en-us/research/publication/slam-and-static-driver-verifier-technology-transfer-of-formal-methods-inside-microsoft/
 * Stellwerkprüfung (Prover Technologies, ...)
 * Datenvalidierung (ProB bei Siemens, Alstom, Thales; Paris L1)
 * Software Entwicklung (AtelierB, Paris L14, L1, ....: seit 1999 kein einziger Bug !)

 # Andere Logiken

 * Aussagenlogik und Prädikatenlogik sind klassische zweiwertige Logiken

 * sie sind <b>monoton</b> wenn $\phi \models \psi$ dann gilt für alle $\rho$: $\phi \wedge \rho \models \psi$

 * Aussagenlogik ist entscheidbar
 * Prädikatenlogik ist semi-entscheidbar: wenn $\phi \models \psi$ kann man einen Beweis finden
 * Gödelscher Vollständigkeitssatz  https://de.wikipedia.org/wiki/Gödelscher_Vollständigkeitssatz
 * reine Prädikatenlogik ist nicht ausreichend um Arithmetik zu axiomatisieren
 * Gödelscher Unvollständigkeitssatz https://de.wikipedia.org/wiki/Gödelscher_Unvollständigkeitssatz

 Nicht-klassische Logiken:
 * es gibt Intuitionistische Logik:  Beweis durch Widerspruch dort nicht erlaubt
 * es gibt dreiwertige Logiken ( $2/0=1 \wedge 1=2$ )
 * es gibt die Fuzzy Logik, modale Logiken, temporale Logiken,...
 * nicht-monotone Logiken

 # Zusammenfassung Logik

 * Aussagenlogik und Prädikatenlogik
 * Interpretation, Modell, Äquivalenz ($\equiv$), logisches Schließen ($\models$)
 * Deduktiver Beweis, Äquivalenzbeweis
 * Beweis durch Widerspruch
 * Äquivalenzen (Kommutativität, de Morgan, ...)
 * logische Formeln verstehen und erstellen können

 %% Cell type:markdown id: tags:

-Auswertung der Formeln erfolgte mit
-![ProB](../presentations/img/prob_logo.png)
+Auswertung der Formeln erfolgte mit dem [Jupyter kernel](https://gitlab.cs.uni-duesseldorf.de/general/stups/prob2-jupyter-kernel) für [ProB](https://www3.hhu.de/stups/prob)
+![ProB](img/prob_logo.png)

 %% Cell type:code id: tags:

 ``` prob
 ```