informatika · informatika prof.dr.norbert fuhr [email protected] auf basis des skripts von...
TRANSCRIPT
Informatik A
Prof. Dr. Norbert Fuhr
auf Basis des Skripts von
Prof. Dr. Wolfram Luther und der Folien von Peter
Fankhauser
1
Teil I
Logik
2
Geschichte
• R. Descartes (17. Jhdt): klassische Euklidische Geometrie mit al-
gebraischen Methoden
• G.W. Leibnitz (17. Jhdt): lingua characteristica, calculus rationa-
tor
• Gottlob Frege (1879): Begriffsschrift Pradikatenlogik erster Stufe
• Skolem (1920): Beweisverfahren
• D. Hilbert, W. Ackermann (1928): Entscheidbarkeitsproblem
• Herbrand (1930): Entscheidbarkeit fur korrekten mathematischen
Satz
• Alan Turing, Alonzo Church (1936): Unentscheidbarkeit PL1
• Robinson (1954): automatisches Beweisverfahren (Resolutions-
prinzip)
• Kowalski, Colmerauer (1972): Prolog
3
Teil I.1
Aussagenlogik
4
Aussagenlogik
Grundlagen
• Aussage (atomare Formel):
Satz der entweder wahr oder falsch ist
abgekurzt mit Großbuchstaben (A, B, ...)
• Beispiel: Heute ist Sonntag
• Interpretation: Zuordnung eines Wahrheitswertes (w oder f)
• Operation: Verknupfung von Aussagen
• Beispiel: Heute ist Sonntag und es ist kalt.
5
Verknupfungen
• Negation: einstellige Operation: ¬A oder A
w f
¬ f w
• Konjunktion: zweistellige Operation: A ∧B
∧ w f
w w ff f f
• Disjunktion: zweistellige Operation: A ∨B
∨ w f
w w wf w f
6
Formeln
Rekursive Konstruktion:
Literal L ::= A Aussage
| ¬A Negierte Aussage
Formel F ::= L Literal
| ¬F Negation
| F ∧ F Konjunktion
| F ∨ F Disjunktion
| (F ) Klammerung
Beispiel
A . . . Heute ist Montag.
B . . . Heute ist Feiertag.
C . . . Heute ist Vorlesung.
¬(A ∧ ¬B) ∨ C
7
Weitere Verkupfungen
• Subjunktion: A→ B ≡ ¬A ∨B
→ w f
w w ff w w
• Bijunktion: A←→ B ≡ (A ∧B) ∨ (¬A ∧ ¬B)
←→ w f
w w ff f w
• Antivalenz (xor): A⊕B ≡ (A ∧ ¬B) ∨ (¬A ∧B)
⊕ w f
w f wf w f
8
Klauseln
Klausel K ::= L Literal| K ∨K Disjunktion
Konjunktive Form KF ::= (K) Klausel| (K) ∧KF Konjunktion von Klauseln
Konjunktion D ::= L Literal| D ∧D Konjunktion
Disjunktive Form DF ::= (D) Konjunktion| (D) ∨DF Disjunktion von
Konjunktionen
Beispiele:
¬A ∨B ∨ C . . . KF und DF
(¬A ∨B ∨ C) ∧ (¬B ∨ ¬C) . . . KF
(¬A ∧ ¬B) ∨ (¬A ∧ ¬C) ∨ (B ∧ ¬C) ∨ (¬B ∧ C) . . . DF
9
Beweisverfahren
Begriffe
• Modell: Interpretation unter der eine Formel F wahr ist.
• Unerfullbare Formel: Formel F , fur die es kein Modell gibt.
• Tautologie: Formel F , fur die jede Interpretationen ein Modell ist.
` F
Beweis uber Wahrheitstafeln
• Durchrechnen fur alle Interpretationen
Axiomatische Verfahren
• Umformen bis zum Wahrheitswert w oder auf konjunktive Form
mit mindestens einer Aussage P ∨ ¬P in jeder Klausel
10
Wahrheitstafel
Zu zeigen: ` ((P → Q) ∧ P )→ Q
P Q P → Q (P → Q) ∧ P ((P → Q) ∧ P )→ Qf f w f wf w w f ww f f f ww w w w w
11
Syntaktische Umformung
Aquivalent sind die folgenden Formeln:
((P → Q) ∧ P )→ Q
¬ ((¬P ∨Q) ∧ P ) ∨Q
((P ∧ ¬Q) ∨ ¬P ) ∨Q
((P ∨ ¬P ) ∧ (¬Q ∨ ¬P )) ∨Q
(w ∧ (¬P ∨ ¬Q)) ∨Q
(¬P ∨ ¬Q) ∨Q
¬P ∨ ww
12
Uberfuhrung in konjunktive Form
((P → Q) ∧ P )→ Q
¬ ((¬P ∨Q) ∧ P ) ∨Q
((P ∧ ¬Q) ∨ ¬P ) ∨Q
((P ∨ ¬P ) ∧ (¬Q ∨ ¬P )) ∨Q
((P ∨ ¬P ∨Q) ∧ (¬Q ∨Q ∨ ¬P ))
13
Aquivalenzregeln
Zwei Formeln F, G sind aquivalent; F ≡ G, wenn gilt: ` F ←→ G
(F ∧ F ) ≡ F, (F ∨ F ) ≡ F Idempotenz
(F ∧G) ≡ (G ∧ F ) ,(F ∨G) ≡ (G ∨ F ) Kommutativitat
((F ∧G) ∧H) ≡ (F ∧ (G ∧H)) ,((F ∨G) ∨H) ≡ (F ∨ (G ∨H)) Assoziativitat
(F ∧ (F ∨G)) ≡ F, (F ∨ (F ∧G)) ≡ F Absorption
(F ∧ (G ∨H)) ≡ ((F ∧G) ∨ (F ∧H)) ,(F ∨ (G ∧H)) ≡ ((F ∨G) ∧ (F ∨H)) Distributivitat
¬¬F ≡ F Doppelnegation¬ (F ∨G) ≡ (¬F ∧ ¬G) ,¬ (F ∧G) ≡ (¬F ∨ ¬G) de Morgansche Regeln
F → G ≡ ¬F ∨G bedingte EliminierungF ∧G ≡ F, F ∨G ≡ G, falls F unerfullbarF ∧G ≡ G, F ∨G ≡ F, falls F Tautologie
14
Logisches Schließen
• Fur S eine Menge von Formeln F1, . . . , Fk und F eine Formel, ist
F eine logische Konsequenz von S, in Zeichen S ` F , wenn jede
Interpretation von S, die ein Modell von S ist, auch ein Modell
von F ist.
• Regeln:
F ` F ∨GF ` G→ F
F ∧G ` FF ∧G ` G↔ F
(F → G) ∧ (G→ H) ` F → H TransitivitatG ∧ (G→ F ) ` F Modus Ponens (Schlussregel)¬F ∧ (G→ F ) ` ¬G Modus Tollens
15
Beispiel: Transitivitat
A: (a ist eine gerade Zahl und b ist eine gerade Zahl)
B: (a+ b ist eine gerade Zahl)
B1: (a = 2n und b = 2m, n, m ganze Zahlen)
B2: (a+ b = 2k, k ganze Zahl)
A a und b sind gerade ZahlenA→ B1 Dann gibt es Zahlen n, m mit a = 2n und b = 2mB1 → B2 Aus a = 2n und b = 2m folgt a+ b = 2(n+m) = 2kB2 → B Aus a+ b = 2k folgt a+ b ist eine gerade ZahlB Mit der Transitivitat gilt B
16
Axiomensysteme
• Theorie: Menge von Axiomen + Menge von Formeln
• Korrektheit: Jede Formel F , die aus einer Theorie T mit Hilfe von
Axiomen AS abgeleitet wird (T `AS) ist eine logische Konsequenz
aus T (T ` F ).
• Vollstandigkeit: Jede Formel F , die eine logische Konsequenz aus
T ist, ist auch tatschlich mit Hilfe von AS ableitbar.
• Konsistenz: Es ist nicht sowohl F als auch ¬F ableitbar.
• Unabhangigkeit: Kein Axiom ist die logische Konsequenz anderer
Axiome.
• Entscheidbarkeit: Fur alle Formeln gilt T `AS F oder T `AS ¬F .
• Aussagenlogik ist entscheidbar und besitzt konsistente, vollstandi-
ge und unabhangige Axiomensysteme.
17
Hilberts Axiomensystem der Aussagenlogik
• AS1: A ∨A→ A
• AS2: A→ (A ∨B)
• AS3: (A ∨B)→ (B ∨A)
• AS4: (A→ B)→ ((C ∨A)→ (C ∨B))
• Definition: A→ B ≡ ¬A ∨B
• Modus Ponens: A ∧ (A→ B) ` B
• Ersetzungsregel: F [A/G] in der Formel F ersetze einige (alle) Vor-
kommen der Aussagenvariablen A durch die Formel G
18
Beispiel
Zeige: ` (F ∨ F )←→ F
Beweis:
(F ∨ F ) → F AS1.
F → (F ∨G) AS2,
F → (F ∨ F ) Ersetzungsregel ((F ∨G)[G/F ]).
19
Automatisches Beweisen
Resolution
• Modus Ponens:
PP → BB
• Verallgemeinerung: P → B ≡ ¬P ∨B
P ∨A1 ∨A2 ∨ . . . ∨An
¬P ∨B1 ∨B2 ∨ . . . ∨Bm
A1 ∨A2 ∨ . . . ∨An ∨B1 ∨B2 ∨ . . . ∨Bm Resolvente
• Um die Aussage A zu beweisen fuge die Negation der Aussage ¬A
zu den Formeln der Theorie und versuche, durch Resolution die
leere Klausel herzuleiten.
20
Beispiel
T = A ∨B, A→ ¬B,¬A
Um B herzuleiten, fugen wir ¬B zur Theorie dazu, und formen A→ ¬B
um.
Das ergibt:
T ′ = A ∨B,¬A ∨ ¬B,¬A,¬B
In Klauselform:
T ′ = (A, B), (¬A,¬B),¬A,¬B
B ist ein Resolvent von (A, B) und ¬A. Der Resolvent von B und ¬B
ist die leere Menge, daher ist T ′ unerfullbar, daher folgt aus T B.
21
Teil I.2
Pradikatenlogik
22
Pradikatenlogik
Erweiterung der Aussagenlogik
• Konstante: a, b, c
• Variablen: x, y, z
• Funktionen: f(a1, . . . , ak)
• Pradikate: P (a1, . . . , ak)
• Quantoren: Allquantor (∀xF ), Existenzquantor (∃xF )
23
Semantik
Interpretation:
Abbildung auf Domane zur Zuordnung eines Wahrheitswertes
Beispiel
F : ∀xP (f(x, a), x).
• Domane: naturliche Zahlen IN := {1,2,3, . . .}
• Konstante a ::= 1
• f(x, a) ::= x ∗ a
• P (x, y) ::= x = y
• Interpretation: Fur alle naturlichen Zahlen x ∈ IN gilt x · 1 = x.
24
Weitere Schlussregeln und Aquivalenzen
∀xF ` ∃xF fur eine nichtleere Domane
∀xF ∨ ∀xG ` ∀x(F ∨G)
∃x(F ∧G) ` ∃xF ∧ ∃xG
¬∀xF ≡ ∃x¬F
¬∃xF ≡ ∀x¬F
∀x∀yF ≡ ∀y∀xF
∃x∃yF ≡ ∃y∃xF
∀x(F ∧G) ≡ ∀xF ∧ ∀xG
∃x(F ∨G) ≡ ∃xF ∨ ∃xG
25
Entscheidbarkeit von PL1
• Die Wahrheitstafelmethode ist nicht ubertragbar
• Erfullbarkeit und Allgemeingultigkeit ist nicht entscheidbar
• PL1 ist halbentscheidbar: Unerfullbare Formeln werden nach end-
licher Zeit erkannt.
26
Beispiel: Peano-Axiome
1. P (1)
2. ∀x (P (x)→ ∃y (P (y) ∧Q(x, y))) .
3. ¬∃x(P (x) ∧Q(x,1)
4.∀x1∀x2∀y1∀y2 (P (x1) ∧ P (x2) ∧Q(x1, y1) ∧Q(x2, y2)∧
¬(x1 = x2)→ ¬(y1 = y2)).
5. ∀M (M(1) ∧ ∀x∀y (P (x) ∧ P (y) ∧M(x) ∧Q(x, y)→M(y))→ (M ≡ P )) .
Interpretation
• P (x) . . . x ist eine naturliche Zahl
• Q(x, y) . . . y = x+1; y ist Nachfolger von x• M . . . Pradikatenvariable (nicht moglich in PL1)
27