Skip to content
Snippets Groups Projects
Commit d0d78fb9 authored by Michael Leuschel's avatar Michael Leuschel
Browse files

fix typos

parent d8434b9b
No related branches found
No related tags found
No related merge requests found
%% Cell type:markdown id: tags:
# Theoretische Informatik - Vorlesung 0 - Teil 1 Logik
* April 2020
* Michael Leuschel
* Lehrstuhl Softwaretechnik und Programmiersprachen
* Heinrich-Heine Universität Düsseldorf
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.
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.
%% Cell type:markdown id: tags:
## Was ist ein Notebook?
* Dokument mit Text und ausführbaren Code-Abschnitten
* Code kann interaktiv ausgeführt werden
* Ergebnisse erscheinen im Notebook unter dem jeweiligem Code
* Ähnlich wie eine REPL (read-eval-print-loop), mit einigen Unterschieden:
* Ausgaben können formatierten Text und Grafiken enthalten
* Speicherbar als Datei
* Code kann später neu ausgeführt werden
* Weitergabe an andere Nutzer möglich
* Implementierungen: Mathematica, Maple, Jupyter, u. a.
%% Cell type:markdown id: tags:
## Jupyter Notebook
* Browserbasierte Notebook-Oberfläche
* Open Source und plattformübergreifend
* Stammt aus der Python-Community, in Python implementiert
* ACM System Software Award 2017
* Jupyter-Notebooks verschiedene Programmiersprachen verwenden
* Ein sprachspezifischer **Kernel** stellt die Sprache dem Jupyter Frontend zur Verfügung
%% Cell type:markdown id: tags:
## [ProB](https://www3.hhu.de/stups/prob) Kernel
![ProB](img/prob_logo.png)
* [ProB](https://www3.hhu.de/stups/prob) ist ein Werkzeug zur Animation, Verifikation und Visualisierung formaler Spezifikationen
* Unterstützt B-Spezifikationen für sicherheitskritsche Anwendungen
* Entwicklung am STUPS Lehrstuhl
* Grundlage: Solver für Prädikatenlogik, Mengentheorie mit Relationen, Funktionen und Arithmetik.
* Eignet sich aber auch für mathematische Ausführungen
* 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
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.
Man kann aber auch die Notebooks vom Browser aus mit Binder starten (das dauert besonders beim ersten Mal etwas länger):
[![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/master)
Damit Jupyter formattierte Ausgabe für Formeln und Tabellen zulässt muss rechts oben in der Menuleiste auf "Not Trusted" drücken. Wenn das Notebook als "Trusted" markiert ist wird JavaScript aktiviert und die Ausgabe wird besser ausgegeben.
%% Cell type:markdown id: tags:
# Was ist Logik?
Quelle [Wikipedia](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).
Hier sind vier Aussagen:
1. Siegfried ist ein Ritter
2. Alle Ritter sagen die Wahrheit
3. Siegfried sagt "Ich habe den Drachen getötet"
4. Siegfried hat den Drachen getötet.
Die Logik interessiert sich weniger ob Aussagen wahr oder falsch sind, sondern mehr um Zusammenhänge zwischen möglichen Wahrheitswerten verschiedener Aussagen und Formeln.
Zum Beispiel, wenn wir die Aussagen 1,2 und 3 als wahr annehmen, dann müssen wir auch die Aussage 4 als wahr annehmen.
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 der Aussagenlogik.
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:code id: tags:
``` prob
¬(1+1=2)
```
%% Output
$\mathit{FALSE}$
FALSE
%% Cell type:markdown id: tags:
In diesen Notebooks muss der Inhalt der Negation immer geklammert werden. Im Skript ist das nicht immer nötig.
%% 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:code id: tags:
``` prob
2>1 ∧ 1>2
```
%% Output
$\mathit{FALSE}$
FALSE
%% 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
1>1 ∨ 1>2
```
%% Output
$\mathit{FALSE}$
FALSE
%% Cell type:code id: tags:
``` prob
2>1 ∨ 3>1
```
%% 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:code id: tags:
``` prob
2>1 ⇒ 1+1=5
```
%% Output
$\mathit{FALSE}$
FALSE
%% 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 der Junktoren der Aussagenlogik kann man in folgender Wahrheitstabelle zusammenfassen:
<img src="./img/wahrheitstabelle.png" width="600">
Wie berechnet man damit den Wahrheitswert einer Formel wie $(p \vee (\neg p \wedge q))$?
%% Cell type:markdown id: tags:
## Interpretationen
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)$.
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$
* 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.
%% Cell type:markdown id: tags:
## Modelle
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 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.
%% Cell type:markdown id: tags:
# Ä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.
%% Cell type:markdown id: tags:
# Wichtige Äquivalenzen
Für alle Formeln $\phi, \psi$ der Aussagenlogik gilt:
* $\phi \wedge \psi \equiv \psi \wedge \phi$ (Kommutativität)
* $\phi \vee \psi \equiv \psi \vee \phi$ (Kommutativität)
Mit diesen Regeln kann man $\Rightarrow$ und $\Leftrightarrow$ umwandeln:
* $\phi \Rightarrow \psi \equiv (\neg \phi) \vee \psi$
* $\phi \Leftrightarrow \psi \equiv (\phi \Rightarrow \psi) \wedge (\psi \Rightarrow \phi)$
Mit diesen Regeln kann man die Negation zu den atomaren Aussagen verschieben:
* $\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)
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:
## Kontraposition
$\neg \psi \Rightarrow \neg \phi$ ist die Kontraposition von $\phi \Rightarrow \psi$.
Ist diese Form äquivalent?
Zur Prüfung kann man die komplette Wahrheitstabelle aufbauen, mit allen möglichen Werten für die "offenen" Formeln $\phi$, $\psi$
%% Cell type:code id: tags:
``` prob
:table {p,q,IMPL,KONT,np,nq| p:BOOL & q:BOOL & np = bool(¬(p=TRUE)) & nq = bool(¬(q=TRUE)) &
IMPL=bool(p=TRUE => q=TRUE) &
KONT=bool((nq=TRUE) => (np=TRUE))}
```
%% Output
|p|q|IMPL|KONT|np|nq|
|---|---|---|---|---|---|
|$\mathit{FALSE}$|$\mathit{FALSE}$|$\mathit{TRUE}$|$\mathit{TRUE}$|$\mathit{TRUE}$|$\mathit{TRUE}$|
|$\mathit{FALSE}$|$\mathit{TRUE}$|$\mathit{TRUE}$|$\mathit{TRUE}$|$\mathit{TRUE}$|$\mathit{FALSE}$|
|$\mathit{TRUE}$|$\mathit{FALSE}$|$\mathit{FALSE}$|$\mathit{FALSE}$|$\mathit{FALSE}$|$\mathit{TRUE}$|
|$\mathit{TRUE}$|$\mathit{TRUE}$|$\mathit{TRUE}$|$\mathit{TRUE}$|$\mathit{FALSE}$|$\mathit{FALSE}$|
p q IMPL KONT np nq
FALSE FALSE TRUE TRUE TRUE TRUE
FALSE TRUE TRUE TRUE TRUE FALSE
TRUE FALSE FALSE FALSE FALSE TRUE
TRUE TRUE TRUE TRUE FALSE FALSE
%% Cell type:markdown id: tags:
Es gilt also:
$\phi \Rightarrow \psi$ $\equiv$ $\neg \psi \Rightarrow \neg \phi$ .
%% 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 $p \wedge q$ auch Modelle von $p$ sind.
Die Tabelle zeigt, dass $p \Leftrightarrow q \models p \Rightarrow q$.
Die beiden 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)
Beispiel: $\phi$ = "Es regnet", $\psi$ = "Die Straße wird nass".
* $(\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$ !
Also:
* $1>2 \models 1+1=100$
%% 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?
%% Cell type:markdown id: tags:
## Lösen des Puzzles
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)
%% Cell type:markdown id: tags:
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$.
%% Cell type:markdown id: tags:
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.
%% Cell type:markdown id: tags:
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
Die [Syllogistik](https://de.wikipedia.org/wiki/Syllogismus), einer Vorform der Prädikatenlogik, geht auf Aristoteles zurück.
Was ist der Zusammenhang zwischen folgenden vier Aussagen, unter der Annahme, daß es mindestens einen Mensch gibt?
(In die Aussagenlogik sind alle vier Aussagen unabhängig.)
1. Alle Menschen sind sterblich.
2. Einige Menschen sind sterblich.
3. Alle Menschen sind unsterblich.
4. Einige Menschen sind unsterblich.
%% 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
%% Cell type:markdown id: tags:
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}$
**Solution:**
* $\mathit{x} = 0$
TRUE
Solution:
x = 0
%% 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$.
%% Cell type:markdown id: tags:
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 der Prädikatenlogik
Mit diesen beiden Gesetzen kann man die Negation zu den atomaren Aussagen und Prädikaten verschieben:
* $\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$
Diese Gesetze erlauben es einem Quantoren zu vertauschen:
* $\forall x.( \forall y. P) \equiv \forall y.( \forall x. P)$
* Beispiel: $\forall x. (\forall y. (x \leq y \vee x>y)) \equiv \forall y. (\forall x. (x \leq y \vee x>y))$
* $\exists x.( \exists y. P) \equiv \exists y.( \exists x. P)$
* Beispiel: $\exists x. (\exists y. (x+y=0)) \equiv \exists y. (\exists x. (x+y=0))$
%% Cell type:markdown id: tags:
Aber Achtung:
* $\forall x.( \exists y. P) \not\equiv \exists y.( \forall x. P)$
* Beispiel: $\forall x. (\exists y. (y > x)) \not\equiv \exists y. (\forall x. (y > x)$
%% 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 !)
%% Cell type:markdown id: tags:
# 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
* (Anmerkung: Wir werden gegen später in der Vorlesung das Konzept der Entscheidbarkeit formal beschreiben)
* 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
%% Cell type:markdown id: tags:
# Zusammenfassung Logik
* Formeln der Aussagenlogik und Prädikatenlogik
* Interpretation, Modell, Äquivalenz ($\equiv$), logisches Schließen ($\models$)
* Deduktiver Beweis, Äquivalenzbeweis
* Beweis durch Widerspruch
* Äquivalenzen (Kommutativität, de Morgan, ...)
* Ziel: logische Formeln verstehen und erstellen können
* Nächste Vorlesung: Grundlagen der Mengentheorie
%% Cell type:code id: tags:
``` prob
```
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment