Post on 05-Feb-2018
Vorlesung
Logik für Informatiker
1. Einführung
Bernhard Beckert
Universität Koblenz-Landau
Sommersemester 2006Logik für Informatiker, SS ’06 – p.1
Formale Logik
Ziel
Formalisierung und Automatisierung rationalen Denkens
Rational richtige Ableitung von neuem Wissen aus gegebenem
Rolle der Logik in der Informatik
Anwendung innerhalb der InformatikSpezifikation, Programmentwicklung, Programmverifikation
Werkzeug für Anwendungen außerhalb der InformatikKünstliche Intelligenz, Wissensrepräsentation
Logik für Informatiker, SS ’06 – p.2
Formale Logik
Ziel
Formalisierung und Automatisierung rationalen Denkens
Rational richtige Ableitung von neuem Wissen aus gegebenem
Rolle der Logik in der Informatik
Anwendung innerhalb der InformatikSpezifikation, Programmentwicklung, Programmverifikation
Werkzeug für Anwendungen außerhalb der InformatikKünstliche Intelligenz, Wissensrepräsentation
Logik für Informatiker, SS ’06 – p.2
Modellierung
Logik für Informatiker, SS ’06 – p.3
Modellierung
?
?
Abstraktion
Logik für Informatiker, SS ’06 – p.4
Modellierung: Adäquatheit des Modells
Adäquatheit
Wenn formulierbare Aussage wahr im Modell,dann entsprechende Aussage wahr in Wirklichkeit
Logik für Informatiker, SS ’06 – p.5
Modellierung: Beispiel Aufzug
oben
mitte
unten
Logik für Informatiker, SS ’06 – p.6
Modellierung: Beispiel Aufzug
Modellierung derstatischen
Eigenschaften
oben
mitte
unten
Logik für Informatiker, SS ’06 – p.6
Modellierung: Beispiel Aufzug
Modellierung derstatischen
Eigenschaften
m
mitte
oben
unten
u
o
oben
mitte
unten
Logik für Informatiker, SS ’06 – p.6
Modellierung: Strukturen
m m m m
mitte
oben
unten
u
mitte
oben
unten
u
o
mitte
oben
unten
u
o
mitte
oben
unten
u
oo
mm
mitte
oben
unten
u
o
m
mitte
oben
unten
u
o
m
mitte
oben
unten
u
o
mitte
oben
unten
u
o
Aussagen beziehen sich auf Strukturen
(Formale) Aussagen sind in jeder einzelnen Struktur zuwahr oder falsch auswertbar
Logik für Informatiker, SS ’06 – p.7
Modellierung: Strukturen
mm
mitte
oben
unten
u
o
m
mitte
oben
unten
u
o
m
mitte
oben
unten
u
o
mitte
oben
unten
u
o
Aussagen beziehen sich auf Strukturen
(Formale) Aussagen sind in jeder einzelnen Struktur zuwahr oder falsch auswertbar
Logik für Informatiker, SS ’06 – p.7
Modellierung: Strukturen
mm
mitte
oben
unten
u
o
m
mitte
oben
unten
u
o
m
mitte
oben
unten
u
o
mitte
oben
unten
u
o
Aussagen beziehen sich auf Strukturen
(Formale) Aussagen sind in jeder einzelnen Struktur zuwahr oder falsch auswertbar
Logik für Informatiker, SS ’06 – p.7
Formale Logik
Logik für Informatiker, SS ’06 – p.8
Formale Logik
I Syntax – Welche Formeln?
I Semantik – Wann ist eine Formel wahr(in einer Struktur)?
I Deduktionsmechanismus – Ableitung neuer wahrer Formeln
Logik für Informatiker, SS ’06 – p.9
Formale Logik
I Syntax – Welche Formeln?
I Semantik – Wann ist eine Formel wahr(in einer Struktur)?
I Deduktionsmechanismus – Ableitung neuer wahrer Formeln
Logik für Informatiker, SS ’06 – p.9
Formale Logik
I Syntax – Welche Formeln?
I Semantik – Wann ist eine Formel wahr(in einer Struktur)?
I Deduktionsmechanismus – Ableitung neuer wahrer Formeln
Logik für Informatiker, SS ’06 – p.9
Aussagenlogik: Syntax
Atomare Aussagen
Aufzug ist oben
aufzugOben
Innen mittlerer Knopf gedrückt
innenMitteGedruckt
Verknüpft mit logischen Operatoren
und
∧
oder
∨
impliziert
→
nicht
¬
Logik für Informatiker, SS ’06 – p.10
Aussagenlogik: Syntax
Atomare Aussagen
Aufzug ist oben
aufzugOben
Innen mittlerer Knopf gedrückt
innenMitteGedruckt
Verknüpft mit logischen Operatoren
und
∧
oder
∨
impliziert
→
nicht
¬
Logik für Informatiker, SS ’06 – p.10
Aussagenlogik: Syntax
Komplexe Aussagen
Wenn innen mittlerer Knopf gedrückt
innenMitteGedruckt
, dann
→
Aufzug nicht in der Mitte
¬aufzugMitte
Der Aufzug ist oben
aufzugOben
und
∧
der Aufzug ist nicht unten
¬aufzugUnten
Logik für Informatiker, SS ’06 – p.11
Aussagenlogik: Syntax
Komplexe Aussagen
Wenn innen mittlerer Knopf gedrückt
innenMitteGedruckt
, dann
→
Aufzug nicht in der Mitte
¬aufzugMitte
Der Aufzug ist oben
aufzugOben
und
∧
der Aufzug ist nicht unten
¬aufzugUnten
Logik für Informatiker, SS ’06 – p.11
Aussagenlogik: Semantik
Der Aufzug ist oben
aufzugOben
und
∧
der Aufzug ist nicht unten
¬aufzugUnten
ist wahr in
m
mitte
oben
unten
u
o
Logik für Informatiker, SS ’06 – p.12
Aussagenlogik: Deduktionsmechanismus
Syllogismen
P → ¬QQ
¬P
aufzugOben → ¬aufzugUnten
aufzugUnten
¬aufzugOben
Logik für Informatiker, SS ’06 – p.13
Aussagenlogik: Deduktionsmechanismus
Syllogismen
P → ¬QQ
¬P
aufzugOben → ¬aufzugUnten
aufzugUnten
¬aufzugOben
Logik für Informatiker, SS ’06 – p.13
Deduktionsmechanismus
Deduktionsmechanismus im allgemeinen
Kalkül
In dieser Vorlesung
• Wahrheitstafeln
• Logische Umformung
• Resolutionskalkül
• Tableaukalkül
Logik für Informatiker, SS ’06 – p.14
Deduktionsmechanismus
Deduktionsmechanismus im allgemeinen
Kalkül
In dieser Vorlesung
• Wahrheitstafeln
• Logische Umformung
• Resolutionskalkül
• Tableaukalkül
Logik für Informatiker, SS ’06 – p.14
The Whole Picture
Diskurs in natürlicher SpracheMathematische ProblemeProgramm + Spezifikation
Syntax
AussagenlogikPrädikatenlogik
GültigeFormeln
BeweisbareFormeln
Formalisierung
Semantik
Ableitung
Kalkül
Vollständigkeit
KorrektheitLogik für Informatiker, SS ’06 – p.15
The Whole Picture
Diskurs in natürlicher SpracheMathematische ProblemeProgramm + Spezifikation
Syntax
AussagenlogikPrädikatenlogik
GültigeFormeln
BeweisbareFormeln
Formalisierung
Semantik
Ableitung
Kalkül
Vollständigkeit
Korrektheit
Modellierung
Logik für Informatiker, SS ’06 – p.16
The Whole Picture
Diskurs in natürlicher SpracheMathematische ProblemeProgramm + Spezifikation
Syntax
AussagenlogikPrädikatenlogik
GültigeFormeln
BeweisbareFormeln
Formalisierung
Semantik
Ableitung
Kalkül
Vollständigkeit
Korrektheit
Deduktion
(automatische)
Logik für Informatiker, SS ’06 – p.17
Inhalt der Vorlesung
1. Einführung
2. Aussagenlogik
Syntax und Semantik
Resolution, Vollständigkeits- und Korrektheitsbeweise
Analytische Tableaus
3. Prädikatenlogik
Syntax und Semantik
Resolution, Vollständigkeits- und Korrektheitsbeweise
Analytische Tableaus
Logik für Informatiker, SS ’06 – p.18
Inhalt der Vorlesung
1. Einführung
2. Aussagenlogik
Syntax und Semantik
Resolution, Vollständigkeits- und Korrektheitsbeweise
Analytische Tableaus
3. Prädikatenlogik
Syntax und Semantik
Resolution, Vollständigkeits- und Korrektheitsbeweise
Analytische Tableaus
Logik für Informatiker, SS ’06 – p.18
Inhalt der Vorlesung
1. Einführung
2. Aussagenlogik
Syntax und Semantik
Resolution, Vollständigkeits- und Korrektheitsbeweise
Analytische Tableaus
3. Prädikatenlogik
Syntax und Semantik
Resolution, Vollständigkeits- und Korrektheitsbeweise
Analytische Tableaus
Logik für Informatiker, SS ’06 – p.18
Das 8-Damen Problem
Man plaziere acht Damen so auf einem Schachbrett,dass sie sich gegenseitig nicht bedrohen.
Logik für Informatiker, SS ’06 – p.19
Das 8-Damen Problem
Man plaziere acht Damen so auf einem Schachbrett,dass sie sich gegenseitig nicht bedrohen.
Logik für Informatiker, SS ’06 – p.19
Das 8-Damen Problem
Aussagenlogische Beschreibung des Problems
Für jedes Feld des Schachbretts eine aussagenlogische Variable
Di, j
Mit der Vorstellung, dass Di, j den Wert wahr hat,wenn auf dem Feld (i, j) eine Dame steht.
Wir benutzen kartesische Koordinaten zur Notation von Positionen.
Logik für Informatiker, SS ’06 – p.20
Das 8-Damen Problem
Aussagenlogische Beschreibung des Problems
Für jedes Feld des Schachbretts eine aussagenlogische Variable
Di, j
Mit der Vorstellung, dass Di, j den Wert wahr hat,wenn auf dem Feld (i, j) eine Dame steht.
Wir benutzen kartesische Koordinaten zur Notation von Positionen.
Logik für Informatiker, SS ’06 – p.20
Das 8-Damen Problem
Beispiel: Auf dem Feld (5, 7) steht eine Dame
Einschränkungen pro Feld
FE5,7 ≡
D5,7 → ¬D5,8 ∧ ¬D5,6 ∧ ¬D5,5 ∧ ¬D5,4 ∧ ¬D5,3 ∧ ¬D5,2 ∧ ¬D5,1
D5,7 → ¬D4,7 ∧ ¬D3,7 ∧ ¬D2,7 ∧ ¬D1,7 ∧ ¬D6,7 ∧ ¬D7,7 ∧ ¬D8,7
D5,7 → ¬D6,8 ∧ ¬D4,6 ∧ ¬D3,5 ∧ ¬D2,4 ∧ ¬D1,3
D5,7 → ¬D4,8 ∧ ¬D6,6 ∧ ¬D7,5 ∧ ¬D8,4
Logik für Informatiker, SS ’06 – p.21
Das 8-Damen Problem
Beispiel: Auf dem Feld (5, 7) steht eine Dame
Einschränkungen pro Feld
FE5,7 ≡
D5,7 → ¬D5,8 ∧ ¬D5,6 ∧ ¬D5,5 ∧ ¬D5,4 ∧ ¬D5,3 ∧ ¬D5,2 ∧ ¬D5,1
D5,7 → ¬D4,7 ∧ ¬D3,7 ∧ ¬D2,7 ∧ ¬D1,7 ∧ ¬D6,7 ∧ ¬D7,7 ∧ ¬D8,7
D5,7 → ¬D6,8 ∧ ¬D4,6 ∧ ¬D3,5 ∧ ¬D2,4 ∧ ¬D1,3
D5,7 → ¬D4,8 ∧ ¬D6,6 ∧ ¬D7,5 ∧ ¬D8,4
Logik für Informatiker, SS ’06 – p.21
Das 8-Damen Problem
Globale Einschränkungen
Für jedes k mit 1 ≤ k ≤ 8:
D1,k ∨ D2,k ∨ D3,k ∨ D4,k ∨ D5,k ∨ D6,k ∨ D7,k ∨ D8,k
Logik für Informatiker, SS ’06 – p.22
Das 8-Damen Problem
Eine aussagenlogische Struktur beschreibt eine Lösung des Acht-
Damen-Problems genau dann, wenn sie ein Modell der Formeln
Fi, j für alle 1 ≤ i, j ≤ 8
Rk für alle 1 ≤ k ≤ 8
ist
Logik für Informatiker, SS ’06 – p.23
Einführung: Zusammenfassung
• Ziel und Rolle der Formalen Logik in der Informatik
• Modellierung, Adäquatheit der Modellierung
• Wesentliche Komponenten für jede Logik:Syntax, Semantik, Deduktionsmeachanismus (Kalkül)
• Beispiel Aussagenlogik: Syntax, Sematik, Syllogismen
• The Whole Picture:
• Formel in der “wahren Welt” / (semantisch) gültige Formel,gültige Formel / ableitbare Formel
• Vollständigkeit und Korrektheit von Kalkülen
• Beispiel für (nicht-triviale) aussagelogische Modellierung:Acht-Damen-Problem
Logik für Informatiker, SS ’06 – p.31
Einführung: Zusammenfassung
• Ziel und Rolle der Formalen Logik in der Informatik
• Modellierung, Adäquatheit der Modellierung
• Wesentliche Komponenten für jede Logik:Syntax, Semantik, Deduktionsmeachanismus (Kalkül)
• Beispiel Aussagenlogik: Syntax, Sematik, Syllogismen
• The Whole Picture:
• Formel in der “wahren Welt” / (semantisch) gültige Formel,gültige Formel / ableitbare Formel
• Vollständigkeit und Korrektheit von Kalkülen
• Beispiel für (nicht-triviale) aussagelogische Modellierung:Acht-Damen-Problem
Logik für Informatiker, SS ’06 – p.31
Einführung: Zusammenfassung
• Ziel und Rolle der Formalen Logik in der Informatik
• Modellierung, Adäquatheit der Modellierung
• Wesentliche Komponenten für jede Logik:Syntax, Semantik, Deduktionsmeachanismus (Kalkül)
• Beispiel Aussagenlogik: Syntax, Sematik, Syllogismen
• The Whole Picture:
• Formel in der “wahren Welt” / (semantisch) gültige Formel,gültige Formel / ableitbare Formel
• Vollständigkeit und Korrektheit von Kalkülen
• Beispiel für (nicht-triviale) aussagelogische Modellierung:Acht-Damen-Problem
Logik für Informatiker, SS ’06 – p.31
Einführung: Zusammenfassung
• Ziel und Rolle der Formalen Logik in der Informatik
• Modellierung, Adäquatheit der Modellierung
• Wesentliche Komponenten für jede Logik:Syntax, Semantik, Deduktionsmeachanismus (Kalkül)
• Beispiel Aussagenlogik: Syntax, Sematik, Syllogismen
• The Whole Picture:
• Formel in der “wahren Welt” / (semantisch) gültige Formel,gültige Formel / ableitbare Formel
• Vollständigkeit und Korrektheit von Kalkülen
• Beispiel für (nicht-triviale) aussagelogische Modellierung:Acht-Damen-Problem
Logik für Informatiker, SS ’06 – p.31
Einführung: Zusammenfassung
• Ziel und Rolle der Formalen Logik in der Informatik
• Modellierung, Adäquatheit der Modellierung
• Wesentliche Komponenten für jede Logik:Syntax, Semantik, Deduktionsmeachanismus (Kalkül)
• Beispiel Aussagenlogik: Syntax, Sematik, Syllogismen
• The Whole Picture:
• Formel in der “wahren Welt” / (semantisch) gültige Formel,gültige Formel / ableitbare Formel
• Vollständigkeit und Korrektheit von Kalkülen
• Beispiel für (nicht-triviale) aussagelogische Modellierung:Acht-Damen-Problem
Logik für Informatiker, SS ’06 – p.31
Einführung: Zusammenfassung
• Ziel und Rolle der Formalen Logik in der Informatik
• Modellierung, Adäquatheit der Modellierung
• Wesentliche Komponenten für jede Logik:Syntax, Semantik, Deduktionsmeachanismus (Kalkül)
• Beispiel Aussagenlogik: Syntax, Sematik, Syllogismen
• The Whole Picture:
• Formel in der “wahren Welt” / (semantisch) gültige Formel,gültige Formel / ableitbare Formel
• Vollständigkeit und Korrektheit von Kalkülen
• Beispiel für (nicht-triviale) aussagelogische Modellierung:Acht-Damen-Problem
Logik für Informatiker, SS ’06 – p.31
Einführung: Zusammenfassung
• Ziel und Rolle der Formalen Logik in der Informatik
• Modellierung, Adäquatheit der Modellierung
• Wesentliche Komponenten für jede Logik:Syntax, Semantik, Deduktionsmeachanismus (Kalkül)
• Beispiel Aussagenlogik: Syntax, Sematik, Syllogismen
• The Whole Picture:
• Formel in der “wahren Welt” / (semantisch) gültige Formel,gültige Formel / ableitbare Formel
• Vollständigkeit und Korrektheit von Kalkülen
• Beispiel für (nicht-triviale) aussagelogische Modellierung:Acht-Damen-Problem
Logik für Informatiker, SS ’06 – p.31
Einführung: Zusammenfassung
• Ziel und Rolle der Formalen Logik in der Informatik
• Modellierung, Adäquatheit der Modellierung
• Wesentliche Komponenten für jede Logik:Syntax, Semantik, Deduktionsmeachanismus (Kalkül)
• Beispiel Aussagenlogik: Syntax, Sematik, Syllogismen
• The Whole Picture:
• Formel in der “wahren Welt” / (semantisch) gültige Formel,gültige Formel / ableitbare Formel
• Vollständigkeit und Korrektheit von Kalkülen
• Beispiel für (nicht-triviale) aussagelogische Modellierung:Acht-Damen-Problem
Logik für Informatiker, SS ’06 – p.31