Folien - Grundbegriffe der Informatik

Grundbegriffe der Informatik
Kapitel 5: Aussagenlogik
Thomas Worsch
KIT, Institut für Theoretische Informatik
Wintersemester 2015/2016
GBI — Grundbegriffe der Informatik
KIT, Institut für Theoretische Informatik
1 / 44
Wo sind wir?
Informelles
Syntax aussagenlogischer Formeln
Boolesche Funktionen
Semantik aussagenlogischer Formeln
Beweisbarkeit
GBI — Grundbegriffe der Informatik
KIT, Institut für Theoretische Informatik
2 / 44
Aussagen — „objektiv“ wahr oder falsch
Beispielaussagen
„Die Abbildung U : AU → N0 ist injektiv.“
„Die Abbildung U : AU → N0 ist surjektiv.“
GBI — Grundbegriffe der Informatik
KIT, Institut für Theoretische Informatik
3 / 44
Aussagen — „objektiv“ wahr oder falsch
Beispielaussagen
„Die Abbildung U : AU → N0 ist injektiv.“
„Die Abbildung U : AU → N0 ist surjektiv.“
GBI — Grundbegriffe der Informatik
wahr
KIT, Institut für Theoretische Informatik
3 / 44
Aussagen — „objektiv“ wahr oder falsch
Beispielaussagen
„Die Abbildung U : AU → N0 ist injektiv.“
„Die Abbildung U : AU → N0 ist surjektiv.“
GBI — Grundbegriffe der Informatik
wahr
falsch
KIT, Institut für Theoretische Informatik
3 / 44
Aussagen — „objektiv“ wahr oder falsch
Beispielaussagen
„Die Abbildung U : AU → N0 ist injektiv.“
„Die Abbildung U : AU → N0 ist surjektiv.“
wahr
falsch
Manches ist keine Aussage, sondern sinnlos
„Ein Barbier ist ein Mann,
der genau alle diejenigen Männer rasiert,
die sich nicht selbst rasieren.“
GBI — Grundbegriffe der Informatik
KIT, Institut für Theoretische Informatik
3 / 44
Aussagen — „objektiv“ wahr oder falsch
Beispielaussagen
„Die Abbildung U : AU → N0 ist injektiv.“
„Die Abbildung U : AU → N0 ist surjektiv.“
wahr
falsch
Manches ist keine Aussage, sondern sinnlos
„Ein Barbier ist ein Mann,
der genau alle diejenigen Männer rasiert,
die sich nicht selbst rasieren.“
Rasiert er sich selbst?
GBI — Grundbegriffe der Informatik
KIT, Institut für Theoretische Informatik
3 / 44
Komplizierte Aussagen —
aus einfacheren zusammengesetzt
Es seien P und Q zwei Aussagen.
Dann erlauben wir diese Konstruktionen:
Negation: „Nicht P“
logisches Und: „P und Q“
logisches Oder: „P oder Q“
logische Folgerung: „P impliziert Q“
„Wenn P, dann Q“
GBI — Grundbegriffe der Informatik
KIT, Institut für Theoretische Informatik
4 / 44
Grundlagen der klassischen Aussagenlogik
Zweiwertigkeit
Jede Aussage ist entweder falsch oder wahr.
Wahrheitswert zusammengesetzter Aussagen
durch Wahrheitswerte der Teilaussagen
eindeutig festgelegt
keine Abhängigkeit vom konkreten Inhalt der Aussagen
auch nicht beim „Wenn . . . , dann . . . “
GBI — Grundbegriffe der Informatik
KIT, Institut für Theoretische Informatik
5 / 44
Grundlagen der klassischen Aussagenlogik
Zweiwertigkeit
Jede Aussage ist entweder falsch oder wahr.
Wahrheitswert zusammengesetzter Aussagen
durch Wahrheitswerte der Teilaussagen
eindeutig festgelegt
keine Abhängigkeit vom konkreten Inhalt der Aussagen
auch nicht beim „Wenn . . . , dann . . . “
Beispiel
P: „2014 in Japan etwa 4.7 Mio. PkW neu zugelassen.“
Q: „1999 es in Deutschland etwa 11.2 Mio. Internet-Nutzer“
„Wenn P, dann Q“
GBI — Grundbegriffe der Informatik
KIT, Institut für Theoretische Informatik
5 / 44
Grundlagen der klassischen Aussagenlogik
Zweiwertigkeit
Jede Aussage ist entweder falsch oder wahr.
Wahrheitswert zusammengesetzter Aussagen
durch Wahrheitswerte der Teilaussagen
eindeutig festgelegt
keine Abhängigkeit vom konkreten Inhalt der Aussagen
auch nicht beim „Wenn . . . , dann . . . “
Beispiel
P: „2014 in Japan etwa 4.7 Mio. PkW neu zugelassen.“
Q: „1999 es in Deutschland etwa 11.2 Mio. Internet-Nutzer“
„Wenn P, dann Q“
tatsächlich eine Aussage
und zwar wahr
Kausalität irrelavant
GBI — Grundbegriffe der Informatik
KIT, Institut für Theoretische Informatik
5 / 44
Wo sind wir?
Informelles
Syntax aussagenlogischer Formeln
Boolesche Funktionen
Semantik aussagenlogischer Formeln
Beweisbarkeit
GBI — Grundbegriffe der Informatik
KIT, Institut für Theoretische Informatik
6 / 44
Alphabet der Aussagenlogik
Aussagevariable: P0 , P1 , P2 , P3 . . .
Var AL ⊆ {Pi | i ∈ N0 }
kurz P, Q, R, S
>
<
aussagenlogische Konnektive: , , ,
Alphabet
>
<
AAL = { (, ), , , ,
GBI — Grundbegriffe der Informatik
} ∪ Var AL .
KIT, Institut für Theoretische Informatik
7 / 44
Konstruktionsabbildungen
<
f
f
× A∗AL
× A∗AL
× A∗AL
→
→
→
A∗AL
A∗AL
A∗AL
sinnvolles Beispiel:
f ( (P Q) , R ) = ((P
:(G, H ) 7→ (G
:(G, H ) 7→ (G
H)
H)
H)
>
) R )
>
<
:(G, H ) 7→ (G
Q) R)
>
>
auch ein Beispiel:
f (
), R ) = (
G 7→ ( G)
>
:A∗AL
:A∗AL
:A∗AL
<
>
f
A∗AL → A∗AL :
<
f :
jede Abbildung vergrößert die Anzahl Konnektive
GBI — Grundbegriffe der Informatik
KIT, Institut für Theoretische Informatik
8 / 44
Lesarten
G)
H)
H)
H)
< >
(
(G
(G
(G
GBI — Grundbegriffe der Informatik
„nicht G“
„G und H “
„G oder H “
„G impliziert H “
(oder „aus G folgt H “)
KIT, Institut für Theoretische Informatik
9 / 44
Syntax — Konstruktion immer größerer Formeln
induktiv
M 0 = Var AL
für jedes n ∈ N0 : Mn+1 = Mn ∪ f (Mn )
>
∪f (Mn × Mn )
<
∪f (Mn × Mn )
∪f (Mn × Mn )
die Formeln: alle zusammen
For AL =
[
Mi
i ∈N0
GBI — Grundbegriffe der Informatik
KIT, Institut für Theoretische Informatik
10 / 44
Konstruktion — ein Beispiel
Es sei Var AL = {P, Q}.
M 0 = {P, Q}
GBI — Grundbegriffe der Informatik
KIT, Institut für Theoretische Informatik
11 / 44
Konstruktion — ein Beispiel
Es sei Var AL = {P, Q}.
M 0 = {P, Q}
f (M 0 ) = {( P),( Q)}
>
>
>
>
>
f (M 0 × M 0 ) = {(P P),(P Q),(Q P),(Q Q)}
f (M 0 × M 0 ) = {(P
GBI — Grundbegriffe der Informatik
P),(P
Q),(Q
<
<
<
<
<
f (M 0 × M 0 ) = {(P P),(P Q),(Q P),(Q Q)}
P),(Q
Q)}
KIT, Institut für Theoretische Informatik
11 / 44
Konstruktion — ein Beispiel
Es sei Var AL = {P, Q}.
M 0 = {P, Q}
f (M 0 ) = {( P),( Q)}
>
>
>
>
>
f (M 0 × M 0 ) = {(P P),(P Q),(Q P),(Q Q)}
f (M 0 × M 0 ) = {(P
P),(P
<
<
<
<
<
f (M 0 × M 0 ) = {(P P),(P Q),(Q P),(Q Q)}
Q),(Q
P),(Q
Q)}
also M 1 = {P, Q,
( P),( Q),
>
>
>
>
(P P),(P Q),(Q P),(Q Q),
(P
GBI — Grundbegriffe der Informatik
P),(P
Q),(Q
<
<
<
<
(P P),(P Q),(Q P),(Q Q),
P),(Q
Q)}
KIT, Institut für Theoretische Informatik
11 / 44
Konstruktion aussagenlogischer Formeln
M 2 enthält zum Beispiel
<
>
( ( P))
((P Q) (Q P))
aber zum Beispiel auch
GBI — Grundbegriffe der Informatik
>
< <
(Q ( Q))
((P Q) P)
(P (Q P))
KIT, Institut für Theoretische Informatik
12 / 44
Konstruktion aussagenlogischer Formeln
M 2 enthält zum Beispiel
<
>
( ( P))
((P Q) (Q P))
aber zum Beispiel auch
>
< <
(Q ( Q))
((P Q) P)
(P (Q P))
für jede Formel G und H noch eine Abkürzung
GBI — Grundbegriffe der Informatik
H)
statt ((G
H ) (H
>
(G
G))
KIT, Institut für Theoretische Informatik
12 / 44
Regeln zur Einsparung von Klammern
Abkürzungen — „offizielle“ Syntax bleibt gleich
Äußere Klammern darf man weglassen.
P
statt
Q
(P
Q)
statt
((P
Q) R)
>
R
>
Q
>
P
>
mehrfach gleiches Konnektiv: „implizite Linksklammerung“
< >
verschiedene Konnektive ohne Klammern —
verschiedene „Bindungsstärken“:
bindet am stärksten
bindet am zweitstärksten
bindet am drittstärksten
bindet am viertstärksten
bindet am schwächsten
GBI — Grundbegriffe der Informatik
statt
von((P
R) (( Q) R))
>
Q R
<
R
>
P
<
Beispiel
KIT, Institut für Theoretische Informatik
13 / 44
Wo sind wir?
Informelles
Syntax aussagenlogischer Formeln
Boolesche Funktionen
Semantik aussagenlogischer Formeln
Beweisbarkeit
GBI — Grundbegriffe der Informatik
KIT, Institut für Theoretische Informatik
14 / 44
George Boole
George Boole (2.11.1815 – 8.12.1864)
englischer Mathematiker und Philosoph
Professor in Cork (Irland)
Buch (1854):
An Investigation of the Laws of Thought
on Which are Founded the Mathematical Theories
of Logic and Probabilities
GBI — Grundbegriffe der Informatik
KIT, Institut für Theoretische Informatik
15 / 44
Boolesche Funktionen
„Wahrheitswerte“: B = {w, f}
boolesche Funktionen f : Bk → B
Beispiele, die gleich verwendet werden:
b (x 1 )
b (x 1 , x 2 )
b (x 1 , x 2 )
b (x 1 , x 2 )
f
f
w
w
f
w
f
w
w
w
f
f
f
f
f
w
f
w
w
w
w
w
f
w
GBI — Grundbegriffe der Informatik
<
x2
>
x1
KIT, Institut für Theoretische Informatik
16 / 44
Übliche Notation für boolesche Funktionen
< >
b (x )
b (x, y)
b (x, y)
b (x, y)
¬x
x ∧y
x ∨y
x̄
x ·y
x +y
Negation bzw. Nicht
Und
Oder
Implikation
bei Verwendung von +, · und ¯
meist auch 0 statt f und 1 statt w
GBI — Grundbegriffe der Informatik
KIT, Institut für Theoretische Informatik
17 / 44
Man kann die meisten booleschen Funktionen
aus wenigen „zusammensetzen“
Beispiel
B2 → B : (x, y) 7→ (¬x ) ∨ x
Abbildung, die konstant w ist
für jedes x ∈ B und y ∈ B
b (x, y) = (¬x ) ∨ y
x
y
¬x
(¬x ) ∨ y
b (x, y)
f
f
w
w
f
w
f
w
w
w
f
f
w
w
f
w
w
w
f
w
GBI — Grundbegriffe der Informatik
KIT, Institut für Theoretische Informatik
18 / 44
Wo sind wir?
Informelles
Syntax aussagenlogischer Formeln
Boolesche Funktionen
Semantik aussagenlogischer Formeln
Beweisbarkeit
GBI — Grundbegriffe der Informatik
KIT, Institut für Theoretische Informatik
19 / 44
Ziel: Bedeutung einer aussagenlogischen Formel —
eine boolesche Funktion
Es sei V eine Menge von Aussagevariablen
Interpretation I : V → B
BV Menge aller Intepretationen
als Tabelle z. B.
GBI — Grundbegriffe der Informatik
P1
P2
P3
f
f
f
f
w
w
w
w
f
f
w
w
f
f
w
w
f
w
f
w
f
w
f
w
KIT, Institut für Theoretische Informatik
20 / 44
Auswertung von Formeln
Es sei I : V → B eine Interpretation.
für jede aussagenlogische Formel F definiere val I (F ) so:
für jedes X ∈ V und jede G, H ∈ For AL sei
val I (X ) = I (X )
val I ( G) = b (val I (G))
val I (G
GBI — Grundbegriffe der Informatik
>
>
H ) = b (val I (G)val I (H ))
<
val I (G
H ) = b (val I (G), val I (H ))
<
val I (G
H ) = b (val I (G), val I (H ))
KIT, Institut für Theoretische Informatik
21 / 44
Auswertung von Formeln — ein Beispiel
Interpretation I mit I (P) = w und I (Q) = f
>
Formel (P Q)
berechne val I (G) durch schrittweise Anwendung der
Definition:
>
>
val I ( (P Q)) = b (val I (P Q))
> > >
= b (b (val I (P), val I (Q)))
= b (b (I (P), I (Q))
= b (b (w, f))
= b (f)
=w
GBI — Grundbegriffe der Informatik
KIT, Institut für Theoretische Informatik
22 / 44
Auswertung einer Formel für alle Interpretationen
oft in Tabellenform
P
Q
f
f
w
w
f
w
f
w
w
w
f
f
w
f
w
f
P
w
w
w
f
Q
P Q
f
f
f
w
(P Q)
>
Q
>
P
<
Beispiel
w
w
w
f
vergleiche drittletzte und letzte Spalte
GBI — Grundbegriffe der Informatik
KIT, Institut für Theoretische Informatik
23 / 44
Äquivalente Formeln
zwei Formeln G und H heißen äquivalent
wenn für jede Interpretation I gilt: val I (G) = val I (H ).
geschrieben G ≡ H
Beispiele
>
<
P
Q und (P Q)
P und P
Q und( P) Q
<
P
informelle Überlegung zum letzten Fall
Q)
Q)
< <
> >
„Gegenteil“ von P Q: (P
also P Q äquivalent zu (P
äquivalent zu( P) (
Q)
äquivalent zu( P) Q
GBI — Grundbegriffe der Informatik
KIT, Institut für Theoretische Informatik
24 / 44
Kleine Randbemerkung —
Auffassung einer Formel als Abbildung
val I (G) definiert für jedes I und jedes G
wir haben
P0 und H = P2
>
Konsequenz: G = P0
>
BV → B : I 7→ val I (G) .
P2 nicht äquivalent
betrachte Interpretation I mit I (P0 ) = w und I (P2 ) = f
val I (G) = w, aber val I (H ) = f.
GBI — Grundbegriffe der Informatik
KIT, Institut für Theoretische Informatik
25 / 44
Kleine Randbemerkung —
Auffassung einer Formel als Abbildung
val I (G) definiert für jedes I und jedes G
wir haben
P0 und H = P2
>
Konsequenz: G = P0
>
BV → B : I 7→ val I (G) .
P2 nicht äquivalent
betrachte Interpretation I mit I (P0 ) = w und I (P2 ) = f
val I (G) = w, aber val I (H ) = f.
wollen die „Namen“ der Aussagevariablen „vergessen“
Bk → B : x 7→ val Ix (G) .
GBI — Grundbegriffe der Informatik
KIT, Institut für Theoretische Informatik
25 / 44
Kleine Randbemerkung —
Auffassung einer Formel als Abbildung
val I (G) definiert für jedes I und jedes G
wir haben
P0 und H = P2
>
Konsequenz: G = P0
>
BV → B : I 7→ val I (G) .
P2 nicht äquivalent
betrachte Interpretation I mit I (P0 ) = w und I (P2 ) = f
val I (G) = w, aber val I (H ) = f.
sei V = {Pi 1 , . . . , Pi k } mit i 1 < i 2 < · · · < x k
definiere für jedes x = (x 1 , . . . , x k ) ∈ Bk
I x : Pi j 7→ x j .
GBI — Grundbegriffe der Informatik
KIT, Institut für Theoretische Informatik
25 / 44
Kleine Randbemerkung —
Auffassung einer Formel als Abbildung
val I (G) definiert für jedes I und jedes G
wir haben
P0 und H = P2
>
Konsequenz: G = P0
>
BV → B : I 7→ val I (G) .
P2 nicht äquivalent
betrachte Interpretation I mit I (P0 ) = w und I (P2 ) = f
val I (G) = w, aber val I (H ) = f.
sei V = {Pi 1 , . . . , Pi k } mit i 1 < i 2 < · · · < x k
definiere für jedes x = (x 1 , . . . , xm ) ∈ Bm mit m ≥ k
I x : Pi j 7→ x j .
GBI — Grundbegriffe der Informatik
KIT, Institut für Theoretische Informatik
25 / 44
Modelle
Interpretation I Modell einer Formel G,
wenn val I (G) = w ist.
Interpretation I Modell für Formelmenge Γ,
wenn I Modell jeder Formel G ∈ Γ ist.
Γ |= G: jedes Modell von Γ auch Modell von G
H |= G statt {H } |= G
|= G statt {} |= G
G für alle Interpretationen wahr
GBI — Grundbegriffe der Informatik
KIT, Institut für Theoretische Informatik
26 / 44
Wichtige Spezialfälle aussagenlogischer Formeln
|= G
z. B. P
z. B. P
<
Formel G Tautologie oder allgemeingültig,
wenn jede Interpretation Modell
P
(Q
P)
Formel G erfüllbar, wenn für mindestens ein I wahr
< >
Q) ( P
Q) ( P
> <
(P
(P
< >
in einigen Anwendungen wichtig
für manche Formeln einfach, für andere anscheinend nicht
R)
R)
mehr in „Theoretische Grundlagen der Informatik“
GBI — Grundbegriffe der Informatik
KIT, Institut für Theoretische Informatik
27 / 44
Tautologien — viele Beispiele auf ein Mal
H
Abkürzung für G
H
H
>
betrachte G
G
für jedes I ist
H
G) = b (val I (G
> >
H
>
val I (G
H ), val I (H
G))
= b (b (val I (G), val I (H )),
b (val I (H ), val I (G)))
wenn G ≡ H , also val I (G) = val I (H ) für jedes I
H ) = b (b (val I (G), val I (G)),
>
dann val I (G
b (val I (G), val I (G)))
>
= b (w, w) = w
GBI — Grundbegriffe der Informatik
KIT, Institut für Theoretische Informatik
28 / 44
zwei Äquivalenz„begriffe“ die zusammenpassen
eben überlegt
Lemma
Wenn G ≡ H ist, dann ist G
GBI — Grundbegriffe der Informatik
H Tautologie.
KIT, Institut für Theoretische Informatik
29 / 44
zwei Äquivalenz„begriffe“ die zusammenpassen
eben überlegt
Lemma
Wenn G ≡ H ist, dann ist G
H Tautologie.
umgekehrt gilt auch
Lemma
Wenn G
H Tautologie ist, dann ist G ≡ H
hier zahlt es sich aus, dass wir „wenn“ und „dann“ sagen
und dafür nicht auch noch Pfeile malen . . .
GBI — Grundbegriffe der Informatik
KIT, Institut für Theoretische Informatik
29 / 44
Tautologien — konkrete Beispiele
G
G (H
H
>
<
>
( G
H)
H)
G
K)und(G
H) K
G (H
KIT, Institut für Theoretische Informatik
K)
<
H
H)
( G
<
G und G
>
>
H) K
G
>
H
H )und (G
G
H)
<
>
H
>
G und G
>
(G
GBI — Grundbegriffe der Informatik
G
>
G
( G
H )und(G
<
H)
(G
G
( G
>
H)
>
(G
G)
<
( H
<
H)
<
(G
H)
<
( G
<
H)
<
(G
<
G
30 / 44
Tautologien anderer Bauart
für G, H , K ∈ For AL sind z. B. auch
G
G
G (H G)
(G (H K)) ((G
( H
G) (( H
G
<
G
H ) (G
G) H )
K))
alles Tautologien
GBI — Grundbegriffe der Informatik
KIT, Institut für Theoretische Informatik
31 / 44
Wo sind wir?
Informelles
Syntax aussagenlogischer Formeln
Boolesche Funktionen
Semantik aussagenlogischer Formeln
Beweisbarkeit
GBI — Grundbegriffe der Informatik
KIT, Institut für Theoretische Informatik
32 / 44
Kalkül — ein System für Beweise
allgemein
Alphabet A
syntaktisch korrekte Formeln For ⊆ A∗
Axiome Ax ⊆ For,
Schlussregeln R ⊆ For kAL
Aussagenkalkül für Aussagenlogik
Alphabet AAL
syntaktisch korrekte Formeln For AL ⊆ A∗AL
Axiome Ax AL ⊆ AAL ,
3
Schlussregel Modus Ponens MP ⊆ For AL
GBI — Grundbegriffe der Informatik
KIT, Institut für Theoretische Informatik
33 / 44
Aussagenkalkül
Axiome
(
)
Ax AL = (G (H G)) G, H ∈ For AL
)
(
∪ (G (H K)) ((G H ) (G K)) G, H , K ∈ For AL
(
)
∪( H
G) (( H G) H ) G, H ∈ For AL
kurz Ax AL 1 , Ax AL 2 und Ax AL 3 für die drei Teilmengen
3
Modus Ponens MP ⊆ For AL
MP = {(G H, G, H ) | G, H ∈ For AL }
G
G H
MP :
H
GBI — Grundbegriffe der Informatik
KIT, Institut für Theoretische Informatik
34 / 44
Ableitungen — formal gefasst
Ableitungen nutzen Prämissen, Axiome und Schlussregeln
Γ ⊆ For AL Hypothesen oder Prämissen und
G eine Formel
Ableitung von G aus Γ
endliche Folge (G 1 , . . . , G n ) von Formeln mit
G n = G (oder weiter vorne) und
für jedes G i trifft einer der folgenden Fälle zu:
Axiom G i ∈ Ax AL ,
Prämisse G i ∈ Γ
oder es gibt Indizes i 1 und i 2 echt kleiner i, für die gilt:
(Gi 1 , G i 2 , G i ) ∈ MP.
geschrieben Γ ` G
GBI — Grundbegriffe der Informatik
KIT, Institut für Theoretische Informatik
35 / 44
Beweis — formal gefasst
Beweis von G: Ableitung aus Γ = {}
geschrieben ` G
G heißt Theorem des Kalküls
GBI — Grundbegriffe der Informatik
KIT, Institut für Theoretische Informatik
36 / 44
Beweis — erstes Beispiel P
1. (P ((P P) P)) ((P
2. P ((P P) P)
3. (P (P P)) (P P)
4. P (P P)
5. P P
(P
P
P)) (P
P)) Ax AL 2
Ax AL 1
MP (1, 2)
Ax AL 1
MP (3, 4)
analog für jede Formel G
ein Beweis„schema“
GBI — Grundbegriffe der Informatik
KIT, Institut für Theoretische Informatik
37 / 44
Beweis — zweites Beispiel( P
1. ( P
2. ( P
3. ( P
P) (( P
P)
P) P
P)
P
P) Ax AL 3
Beispiel von eben
MP (1, 2)
P)
genaugenommen statt Zeile 2 die fünf Zeilen von eben
Auch Beweise strukturiert man!
GBI — Grundbegriffe der Informatik
KIT, Institut für Theoretische Informatik
38 / 44
Modus Ponens „erhält Allgemeingültigkeit“
Lemma
Wenn sowohl G H als auch G Tautologien sind, dann ist
auch H eine Tautologie.
Beweis
wenn G
H Tautologie, dann gilt für jedes I :
w = val I (G
H ) = b (val I (G), val I (H )) .
da G Tautologie, ist val I (G) = w und folglich
b (val I (G), val I (H )) = b (w, val I (H )) = val I (H )
also für jede Bewertung I : w = val I (H )
also ist H Tautologie
GBI — Grundbegriffe der Informatik
KIT, Institut für Theoretische Informatik
39 / 44
Alle Theorem des Aussagenkalküls sind Tautologien
alle Axiome sind Tautologien
Modus Ponens erhält Allgemeingültigkeit
GBI — Grundbegriffe der Informatik
KIT, Institut für Theoretische Informatik
40 / 44
die umgekehrte Richtung gilt auch
schwieriger zu beweisen:
Lemma
Jede Tautologie ist im Aussagenkalkül beweisbar.
insgesamt
Theorem
Für jede Formel G ∈ For AL
gilt |= G genau dann, wenn ` G gilt.
GBI — Grundbegriffe der Informatik
KIT, Institut für Theoretische Informatik
41 / 44
Ein Beispiel für die Nützlichkeit des Kalküls
Theorem
Für jedes G ∈ For AL und jedes H ∈ For AL
gilt G ` H genau dann, wenn ` (G H ).
einfache Richtung:
wenn ` (G H ), dann G ` H
es sei (G 1 , . . . , G n ) ein Beweis für ` (G
mit G n = (G H )
Ableitung für G ` H ?
verlängere die Folge um zwei Formeln
G n+1 = G
G n+2 = H
H)
Prämisse
MP aus G n und G n+1
umgekehrte Richtung: auf der nächsten Folie
GBI — Grundbegriffe der Informatik
KIT, Institut für Theoretische Informatik
42 / 44
Fortsetzung des Beweises
Zeige: Wenn G ` H dann ` (G
H ).
es sei (G 1 , . . . , G n ) ein Ableitung für G ` H
konstruieren Beweis (H 1 , . . . , Hm ) für ` (G
Ziel: für jedes G i ist ein Hi 0 = (G
H)
Gi )
wenn G i Axiom, drei Formeln
(G i (G G i )) Ax AL 1
G i Axiom
MP aus diesen beiden Formeln
wenn G i = G, Formeln für Beweis der Tautologie
(G i
Gi )
dritter Fall . . .
GBI — Grundbegriffe der Informatik
KIT, Institut für Theoretische Informatik
43 / 44
Fortsetzung des Beweises
Zeige: Wenn G ` H dann ` (G
H ).
es sei (G 1 , . . . , G n ) ein Ableitung für G ` H
konstruieren Beweis (H 1 , . . . , Hm ) für ` (G
Ziel: für jedes G i ist ein Hi 0 = (G
Gi )
wenn G i = K 2 durch MP aus G i 1 = K 1
K 2 und G i 2 = K 1
dann schon abgeleitet
G Gi1
G Gi2
(G (K 1 K 2 )) ((G K 1 ) (G K 2 ))
= (G G i 1 ) ((G G i 2 ) (G G i ))
zweimal MP liefert G G i
GBI — Grundbegriffe der Informatik
H)
Ax AL 3
KIT, Institut für Theoretische Informatik
43 / 44
Was ist wichtig
Das sollten Sie mitnehmen:
aussagenlogische Formeln haben
Syntax
Semantik
boolesche Funktionen
Formalisierung von Beweisbarkeit in Kalkülen
Zusammenhang mit Allgemeingültigkeit
Das sollten Sie üben:
Rechnen mit booleschen Funktionen
Überprüfen von Formeln auf Erfüllbarkeit und
Allgemeingültigkeit
präzises Argumentieren wie bei Beweisen in Kalkülen
GBI — Grundbegriffe der Informatik
KIT, Institut für Theoretische Informatik
44 / 44

Download Report