VioricaSofronie-Stokkermans...

Logik fur Informatiker

Viorica Sofronie-Stokkermans

e-mail: [email protected]

1

Literatur zur Vorlesung

Skriptum von U. Furbach

Ulrich Furbach

Logic for Computer Scientists

http://userpages.uni-koblenz.de/∼obermaie/script.htm

Buch von U. Schoning

Uwe Schoning

Logik fur Informatiker

5. Auflage, Spektrum Akademischer Verlag

Buch von M. Fitting

Melvin Fitting

First-Order Logic and Automated Theorem Proving

2. Auflage, Springer-Verlag

2

Logik in der Informatik

Was ist Logik?

• Mathematisch?

ja

• Unverstandlich?

hoffentlich nein

• Reine Theorie ohne praktischen Nutzen?

nein: Verifikation von Hardware, Software, Protokollen

Sprachverarbeitung und Wissensreprasentation

Abfragensprachen fur Datenbanken; ...

3

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 Informatik

Spezifikation, Programmentwicklung, Programmverifikation

• Werkzeug fur Anwendungen außerhalb der Informatik

Kunstliche Intelligenz, Wissensreprasentation

4

Modellierung

Abstraktion

5

Modellierung

Adaquatheit des Modells

Wenn formulierbare Aussage wahr im Modell, dann entsprechende Aussage

wahr in Wirklichkeit

6

Modellierung: Strukturen

Aufzug oben Aufzug oben

Aufzug mitte

oben

mitte

unten

Mitte gedruckt

F.nach unten

oben

mitte

unten

oben

mitte

unten

Mitte gedruckt

F.nach unten

F.nach unten

Unten gedruckt

v(AufzugOben) = wahr v(AufzugMitte) = wahr v(AufzugOben) = wahr

v(AufzugMitte) = wahr

v(MitteGedruckt) = wahr v(UntenGedruckt) = wahr v(MitteGedruckt) = wahr

v(FahrtNachUnten) = wahr v(FahrtNachUnten) = wahr v(FahrtNachUnten) = wahr

7



Aufzug mitteAufzug mitte

oben

mitte

unten

Mitte gedruckt

F.nach unten

oben

mitte

unten

Mitte gedruckt

F.nach unten

oben

mitte

unten

F.nach unten

Unten gedruckt

v(AufzugOben) = wahr v(AufzugMitte) = wahr v(AufzugOben) = wahr

v(AufzugMitte) = wahr

v(MitteGedruckt) = wahr v(UntenGedruckt) = wahr v(MitteGedruckt) = wahr

v(FahrtNachUnten) = wahr v(FahrtNachUnten) = wahr v(FahrtNachUnten) = wahr

8



Aufzug mitteAufzug mitte

oben

mitte

unten

Mitte gedruckt

F.nach unten

oben

mitte

unten

Mitte gedruckt

F.nach unten

oben

mitte

unten

F.nach unten

Unten gedruckt

Aussagen beziehen sich auf Strukturen

(Formale) Aussagen sind in jeder einzelnen Struktur zu wahr oder falsch

auswertbar

9

Formale Logik

• Syntax

welche Formeln?

• Semantik

Modelle (Strukturen)

Wann ist eine Formel wahr (in einer Struktur)?

• Deduktionsmechanismus

Ableitung neuer wahrer Formeln

10

Aussagenlogik: Syntax

Die Welt besteht aus Fakten

Bausteine: Atomare Aussagen

Beispiele: Aufzug ist oben:

AufzugOben

Mittlerer Knopf gedruckt:

MitteGedruckt

Verknupft mit logischen Operatoren

und oder impliziert nicht

(“wenn, dann”)

∧ ∨ → ¬

11

Aussagenlogik: Syntax

Komplexe Aussagen:

Beispiele:

Wenn mittlerer Knopf gedruckt, dann Aufzug nicht in der Mitte

MitteGedruckt → ¬AufzugMitte

Der Aufzug ist oben und der Aufzug ist nicht unten

AufzugOben ∧ ¬AufzugUnten

12

Aussagenlogik: Semantik



wahr in: Aufzug oben oben

mitte

unten

Mitte gedruckt

F.nach unten

13

Aussagenlogik: Semantik



falsch in:

Aufzug mitte

oben

mitte

unten

F.nach unten

Unten gedruckt

14

Aussagenlogik: Deduktionsmechanismus



Syllogismen:

P P → Q

Q

AufzugUnten AufzugUnten → ¬AufzugOben

¬AufzugOben

15

Aussagenlogik: Deduktionsmechanismus

Deduktionsmechanismus im allgemeinen

Kalkul

In dieser Vorlesung:

• Wahrheitstafeln

• Logische Umformung

• Resolutionskalkul

• Tableaukalkul

16

Pradikatenlogik

Aussagenlogik: Die Welt besteht aus Fakten

... aber: Aussagenlogik hat nur beschrankte Ausdruckskraft

Beispiele:

• Die Aussage “Alle Menschen sind sterblich” erfordert eine Formel fur

jeden Mensch.

• Die Aussage “Jede naturliche Zahl ist entweder gerade oder ungerade”

erfordert eine Formel fur jede Zahl.

17

Pradikatenlogik

Reichere Struktur

• Objekte (Elemente)

Leute, Hauser, Zahlen, Theorien, Farben, Jahre, ...

• Relationen/Eigenschaften

rot, rund, gerade, ungerade, prim, mehrstockig, ...

ist Bruder von, ist großer als, ist Teil von, hat Farbe, besitzt, ..

=, ≥, ...

• Funktionen

+, Mitte von, Vater von, Anfang von, ...

18

Beispiel 1

Objekte (Elemente): Zahlen

Funktionen: +, *

Terme: 2 + 3, 3 ∗ (5 + 6), x , x + 2, x ∗ (2− y)

Relationen/Eigenschaften: gerade, ungerade

Formel:

gerade(2), ungerade(5), gerade(100), ungerade(100)

gerade(2)∧ ungerade(5)

gerade(x) → gerade(x + 1)

Quantoren:

A

(fur alle);

E

(es gibt)

Formeln mit Quantoren:

A

x gerade(x)∨ gerade(x + 1)

E

x ungerade(x)

19

Beispiel 2:

• Objekte (Elemente): Menschen

• Funktionen: Vater, Mutter, Jan, Anna

x Jan Anna

Vater(x) Vater(Jan) Vater(Anna)

Mutter(x) Mutter(Jan) Mutter(Anna)

Vater(Mutter(x)) Vater(Mutter(Jan)) ...

• Eigenschaften: ist-Bruder-von; Mann; Frau

Mann(x) Mann(Jan) Mann(Anna)

Mann(Vater(x)) Frau(Vater(Jan)) Mann(Vater(Jan))

ist-Bruder-von(x , y) ist-Bruder-von(x , Jan) ist-Bruder-von(x ,Anna)

ist-Bruder-von(Jan,Anna)

20

Beispiel 2:

Formel:

Mann(Vater(Jan))

Mann(Vater(Jan)) ∧ Frau(Mutter(Jan))

Mann(Mutter(Anna))

Mann(Vater(Jan))∧ ist-Bruder-von(Jan,Anna)

Quantoren

A

: fur alle

E

: es gibt

Formeln mit Quantoren:

A

x Mann(Vater(x))

A

x Mann(Mutter(x))

A

x , y (ist-Bruder-von(x , y) → Mann(x))

21

Beispiel 3

“Alle, die in Koblenz studieren, sind schlau”


• Funktionen: koblenz

• Eigenschaften: studiertIn, schlau

Ax(studiertIn(x , koblenz) → schlau(x))

“Es gibt jemand, der in Landau studiert und schlau ist”


• Funktionen: landau

• Eigenschaften: studiertIn, schlau

E

x(studiertIn(x , landau) ∧ schlau(x))

22

Pradikatenlogik: Deduktionsmechanismus



Syllogismen:

Ax(P(x) → Q(x))

Ax(Q(x) → R(x))

A

x(P(x) → R(x))

A

x(studiertIn(x , koblenz) → schlau(x))

A

x(schlau(x) → gute-noten(x))

A

x(studiertIn(x , koblenz) → gute-noten(x))

23




Syllogismen:

Q(a)Ax(Q(x) → R(x))

R(a)

Beispiel:

studiertIn(Jan, koblenz)

A

x(studiertIn(x , koblenz) → schlau(x))

schlau(Jan)

24


In dieser Vorlesung:

• Resolutionskalkul

• Tableaukalkul

25

Das Prinzip

z.B. naturliche Sprache

Problem Losung

LosungFormeln

prazise Beschreibung

26

Anwendungesbeispiel: Sicherheitsprotokole

Ziel: zwei Personen (Alice und Bob) wollen miteinander kommunizieren

• uber ein unsicheres Daten- oder Telefonnetz,

• sicher, d. h., ohne daß ein Eindringling (Charlie) mithoren oder sich als

Alice oder Bob ausgeben kann.

Hilfsmittel: Verschlusselung

• Alice und Bob vereinbaren einen gemeinsamen Schlussel

und nutzen ihn, um ihr Gesprach zu verschlusseln.

• Nur wer den Schlussel kennt, kann das Gesprach entschlusseln.

27

Beispiel: Sicherheitsprotokolle

Problem: wie kommen die Gesprachspartner an den gemeinsamen Schlussel?

• Personliche Ubergabe kommt nicht immer in Frage.

• Wird der gemeinsame Schlussel uber das Netz

unverschlusselt verschickt, konnte Charlie ihn abfangen oder

austauschen.

• Annahme: es gibt eine sichere Schlusselzentrale, mit der Alice und Bob

jeweils einen gemeinsamen Schlussel vereinbart haben.

28


Das folgende Schlusselaustauschverfahren wurde 1993 von den beiden Kryp-

tographen Neuman und Stubblebine vorgeschlagen:

Schritt 1:

Alice schickt (offen) Identifikation und Zufallszahl an Bob.

29


Schritt 2:

Bob leitet Nachricht weiter an Schlusselzentrale (”Trust“).

30


Schritt 3:

Trust schickt Nachricht an Alice. Darin: ein neuer gemeinsamer Schlussel,

einmal fur Alice und einmal fur Bob verschlusselt.

31


Schritt 4:

Alice leitet den neuen gemeinsamen Schlussel weiter an Bob.

32


Schritt 5:

Alice und Bob konnen nun mit dem gemeinsamen Schlussel kommunizieren.

33


Ist das Verfahren sicher?

Wir ubersetzen das Problem in Formeln und lassen sie von einem

Theorembeweiser untersuchen.

34


Zuerst formalisieren wir die Eigenschaften des Protokolls:

• Wenn Alice/Bob/Trust eine Nachricht in einem bestimmten Format

bekommt, dann schickt er/sie eine andere Nachricht ab.

Dann formalisieren wir die Eigenschaften des Angreifers:

• Wenn eine Nachricht ubermittelt wird, kann Charlie sie mithoren.

• Wenn Charlie eine verschlusselte Nachricht bekommt und den

passenden Schlussel hat, kann er sie entschlusseln.

• Wenn Charlie eine Nachricht hat, dann kann er sie an Alice/Bob/Trust

abschicken.

. . .

35

Formalisierung

Zum Schluss mussen wir noch formalisieren was es bedeutet, dass der

Angreifer Erfolg hat.

Dies ist dann der Fall, wenn er einen Schlussel zur Kommunikation mit Bob

hat, von dem Bob glaubt, es sei ein Schlussel fur Alice.E

x[Ik(key(x , b)) ∧ Bk(key(x , a))]

36

Automatische Analyse

Die Formalisierung des Protokolls, Formeln (1)-(8) zusammen mit den

Angreiferformeln (9)-(20) und der Erfolgsbedingung fur den Angreifer kann

man nun in einen Theorembeweiser eingeben.

Der Theorembeweiser beweist dann automatisch, dass der Angreifer das

Protokoll brechen kann.

37

Das ganze Bild

Probleme (Beschreibung in natürlicher Sprache)

Formalisierung

Logik

Gültige Formel Beweisbare Formel

Kalkül

Logische Sprache: Syntax

Aussagenlogik /

Formel

Modelle: Semantik

Vollständigkeit

Korrektheit

Prädikatenlogik

38

Das ganze Bild

Modellierung


Formalisierung

Logik


Kalkül


Aussagenlogik / Prädikatenlogik

Formel

Modelle: Semantik

Vollständigkeit

Korrektheit

39

Das ganze Bild

(automatische)

Deduktion


Formalisierung

Logik


Kalkül


Aussagenlogik /

Formel

Modelle: Semantik

Vollständigkeit

Korrektheit

Prädikatenlogik

40

Inhalt der Vorlesung

• 1. Einfuhrung: Motivation, Beweisstrategien (insb. Induktion)

• 2. Aussagenlogik

– Syntax und Semantik

– Deduktionsmechanismen:

- Resolution, Vollstandigkeits- und Korrektheitsbeweise

- Analytische Tableaux

• 3. Pradikatenlogik

– Syntax und Semantik

– Deduktionsmechanismen:

- Resolution, Vollstandigkeits- und Korrektheitsbeweise

- Analytische Tableaux

• 4. Weitere Aussichten

- Nichtklassische Logiken; Logiken hoherer Stufe

- Anwendungen: z.B. Datenbanken oder Verifikation

41

Einfuhrung: Zusammenfassung

• Ziel und Rolle der Formalen Logik in der Informatik

• Modellierung, Adaquatheit der Modellierung

• Wesentliche Komponenten fur jede Logik: Syntax, Semantik,

Deduktionsmechanismus (Kalkul)

• Beispiel Aussagenlogik: Syntax, Semantik, Syllogismen

• Beispiel Pradikatenlogik: Syntax, Semantik, Syllogismen

• The Whole Picture:

– Formel in der “wahren Welt” / (semantisch) gultige Formel,

gultige Formel / ableitbare Formel

– Vollstandigkeit und Korrektheit von Kalkulen

42

1. Grundlegende Beweisstrategien

43

Mathematisches Beweisen

Mathematische Aussagen

- haben oft die Form: Wenn A, dann B.

- als Formel: A → B

Mathematischer Beweis

- bzgl. eines vorgegebenen Axiomensystems

- mit Hilfe von Inferenzregeln

44

Grundlegende Beweisstrategien

Mathematische Aussagen der Form A → B (Wenn A, dann B)

- Direkter Beweis:

Annahme: A gilt. Benutze A, Axiome, und Inferenzregeln

um B zu beweisen.

Behauptung: Das Quadrat einer ungeraden naturlichen Zahl n ist stets ungerade.

Beweis: Es sei n eine ungerade naturliche Zahl. Dann lasst sich n als n = 2k + 1

darstellen, wobei k ∈ N. Daraus folgt mit Hilfe der ersten binomischen Formel,

dass:

n2= (2k + 1)

2= 4k

2+ 4k + 1 = 2 · (2k2

+ 2k) + 1.

Aus der Moglichkeit, n2 so darzustellen folgt, dass n2 ungerade ist.

45


Mathematische Aussagen der Form A → B (Wenn A, dann B)

- Beweis durch Kontraposition:

Beweis von ¬B → ¬A.

- Beweis durch Widerspruch:

Beweise dass A ∧ ¬B → falsch

Behauptung: Ist die Wurzel aus einer geraden naturlichen Zahl n eine naturliche

Zahl, so ist diese gerade.

Beweis: Angenommen,√n = k ware ungerade. Dann ist wegen der bereits be-

wiesenen Behauptung auch k2 = n ungerade, und das ist ein Widerspruch zu der

Voraussetzung, dass n gerade ist.

Also ist die getroffene Annahme falsch, d.h.,√n ist gerade.

46


Mathematische Aussagen, die nicht die Form A → B haben

- Aquivalenzbeweis (A ⇔ B) (A genau dann, wenn B)

Beweise dass A → B und dass B → A.

(Wenn A, dann B, und wenn B, dann A.)

47


- Beweis durch Widerspruch

Um A zu beweisen:

Annahme: A ist falsch (die Negation von A ist wahr)

Zeige, dass dies zu einem Widerspruch fuhrt.

Behauptung:√2 6∈ Q.

Beweis: Wir nehmen an dass√2 ∈ Q und somit

√2 = p

qwobei der Bruch p/q in gekurzter

Form vorliegt (d.h. p und q teilerfremde ganze Zahlen sind). Dann(

pq

)2= 2, d.h: p2 = 2q2.

Da 2q2 eine gerade Zahl ist, ist auch p2 gerade. Daraus folgt, dass auch p gerade ist, d.h.

p = 2r (wobei r ∈ Z). Damit erhalt man mit obiger Gleichung: 2q2 = p2 = (2r)2 = 4r2,

und hieraus nach Division durch 2: q2 = 2r2. Mit der gleichen Argumentation wie zuvor folgt,

dass q2 und damit auch q eine gerade Zahl ist. Da p und q durch 2 teilbar sind, erhalten

wir einen Widerspruch zur Teilerfremdheit von p und q. Dieser Widerspruch zeigt, dass die

Annahme,√2 sei eine rationale Zahl, falsch ist und daher das Gegenteil gelten muss. Damit

ist die Behauptung, dass√2 irrational ist, bewiesen.

48


- Beweis durch Fallunterscheidung

Um B zu beweisen, beweise dass A1 → B, . . . ,An → B,

wobei A1 ∨ · · · ∨ An ≡ wahr

Behauptung: Jede Primzahl p≥3 hat die Form p = 4·k + 1 oder p = 4·k − 1 mit k ∈ N.

Beweis: Man unterscheidet folgende vier Falle fur p, von denen immer genau einer eintritt:

Fall 1: p = 4kFall 2: p = 4k + 1Fall 3: p = 4k + 2Fall 4: p = 4k + 3 = 4(k + 1) − 1

Im ersten dieser Falle ist p durch 4 teilbar und damit keine Primzahl,

im dritten Fall ist p durch 2 teilbar und somit ebenfalls keine Primzahl.

Also muss einer der Falle zwei oder vier eintreten, das heißt p hat die Form p = 4 · k + 1

oder p = 4 · k − 1 mit k ∈ N.

49


- Beweis durch Fallunterscheidung

Um B zu beweisen, beweise dass A1 → B, . . . ,An → B,

wobei A1 ∨ · · · ∨ An ≡ wahr

Es sei angemerkt, dass die Fallunterscheidung zwar vollstandig sein

muss, aber die untersuchten Falle sich nicht gegenseitig ausschließen

mussen.

50


Aussagen mit Quantoren

A

x ∈ U : (p(x) → q(x))

Wahle a beliebig aus U.

Beweise, dass p(a) → q(a).

Da a beliebig gewahlt werden kann, folgtA

x ∈ U : p(x) → q(x)

Behauptung:

A

n ∈ N : (n ist gerade und√n ist eine naturliche Zahl

︸︷︷︸

p(n)

→√n ist gerade

︸︷︷︸

q(n)

).

Beweis: Sei n beliebig aus N.

Wir zeigen, dass wenn n gerade ist und√n eine naturliche Zahl ist, dann

√n gerade ist.

(Dies wurde auf Seite 46 bewiesen.)

51



E

x ∈ U A(x)

Sei a ein geeignetes Element aus U.

Beweise, dass A(a) wahr ist. Damit folgt

E

x ∈ U : A(x).

Behauptung:

E

x ∈ N : x2 − 2x + 1 = 0

Beweis: A(x) : x2 − 2x + 1 = 0

Sei a = 1. Wir zeigen, dass A(a) wahr ist: a2 − 2a + 1 = 12 − 2 + 1 = 0.

Damit folgt

E

x ∈ N : A(x)

52



E

x ∈ U A(x)


Beweise, dass A(a) wahr ist. Damit folgt

E

x ∈ U : A(x).E

x ∈ U (p(x) → q(x))


Beweis der Implikation p(a) → q(a).

Damit folgt

E

x ∈ U : p(x) → q(x).

53


Beweise mittels Vollstandiger Induktion

54

Induktion

Wesentliches Beweisprinzip in Mathematik und Logik

Einfache Version

Induktion uber die naturlichen Zahlen N

(natural induction)

Generalization

Noethersche Induktion

(noetherian induction/

induction over well-founded partially ordered sets)

Hier: Strukturelle Induktion

55

Induktion uber die naturlichen Zahlen

Idee: Definition der naturlichen Zahlen

(A1) 0 ist eine naturliche Zahl

(A2) Jede naturliche Zahl n hat einen Nachfolger S(n)

(A3) Aus S(n) = S(m) folgt n = m

(A4) 0 ist nicht Nachfolger einer naturlichen Zahl

(A5) Jede Menge X , die 0 und mit jeder naturlichen Zahl n

auch deren Nachfolger S(n) enthalt, umfasst alle

naturlichen Zahlen.

56


(A5) Jede Menge X , die 0 und mit jeder naturlichen Zahl n

auch deren Nachfolger S(n) enthalt, umfasst alle

naturlichen Zahlen.

A

X Menge: Falls 0 ∈ X , und

A

n ∈ N : n ∈ X → n + 1 ∈ X

so

A

n ∈ N : n ∈ X

Induktionssatz

Gelten die beiden Aussagen:

- p(0) und Induktionsbasis

-

A

n ∈ N : p(n) → p(n + 1), Induktionsschritt

dann gilt auch

A

n ∈ N : p(n).

57


Struktur eines Induktionsbeweises

(1) Induktionsbasis: Beweise p(0)

(2) Induktionsschritt: Beweise p(n) → p(n + 1)

fur ein beliebiges n ∈ N

58


Struktur eines Induktionsbeweises

(1) Induktionsbasis: Beweise p(0)

(2) Induktionsvoraussetzung: Fur ein beliebig gewahltes

n ∈ N gilt p(n)

(3) Induktionsschluss: Folgere p(n + 1) aus der

Induktionsvoraussetzung p(n)

0 1 2 3

59

Beispiel

Behauptung: Die Summe der ersten n ungeraden Zahlen ist n2.

Fur alle n ∈ N,

n−1∑

i=0

(2i + 1) = n2.

p(n) :

n−1∑

i=0

(2i + 1) = n2

(1) Induktionsbasis: Beweise p(0) OK

(2) Induktionsvoraussetzung: Fur ein beliebig gewahltes

n ∈ N gilt p(n):

n−1∑

i=0

(2i + 1) = n2

(3) Induktionsschluss: Folgere p(n + 1) aus p(n)

p(n + 1) :

n∑

i=0

(2i + 1) = (n + 1)2.

Beweis:

n∑

i=0

(2i + 1) = (

n−1∑

i=0

(2i + 1)) + (2n + 1)p(n)= n

2+ (2n + 1) = (n + 1)

2.

60

Wohlfundierte (Noethersche) Induktion

Verallgemeinerte vollstandige Induktion


p(0) und

A

n ∈ N : p(0) ∧ p(1) ∧ · · · ∧ p(n) → p(n + 1)

dann gilt die Aussage

A

n ∈ N : p(n).

Aquivalent


p(0) und

A

n ∈ N : (

A

k ∈ N : (k < n + 1 → p(k)) → p(n + 1))


A

n ∈ N : p(n).

61


Verallgemeinerte vollstandige Induktion


p(0) und

A

n ∈ N : p(0) ∧ p(1) ∧ · · · ∧ p(n) → p(n + 1)


A

n ∈ N : p(n).

Aquivalent

Gilt die Aussage:

A

n ∈ N : (

A

k ∈ N : (k < n → p(k)) → p(n))


A

n ∈ N : p(n).

62

Vollstandige Induktion

Zu zeigen:

A

n ≥ n0 : P(n)

Sei n ∈ N, n ≥ n0.

Induktionsvoraussetzung: p(k) gilt fur alle k < n

Induktionsschluss: Folgere p(n) aus der Induktionsvoraussetzung.

63


Theorem:

Falls

A

n ∈ N : (

A

k ∈ N : (k < n → p(k)) → p(n)) P

dann gilt

A

n ∈ N : p(n) Q

Beweis: Zu zeigen: P → Q

Kontrapositionsbeweis: Wir zeigen, dass ¬Q → ¬P

Annahme: ¬Q := ¬(

A

n ∈ N : p(n)) ≡

E

n ∈ N : ¬p(n).

> wohlfundierte Ordnung auf N: es gibt keine unendliche Folge

x1, . . . , xn, . . . mit x1 > x2 > · · · > xn > . . . .

Sei Y = {n ∈ N | ¬p(n)} 6= ∅. Dann hat Y ein minimales Element m, d.h.

E

m(m ∈ Y ∧ (

A

k ∈ N : (k < m → k 6∈ Y ))) = ¬P.

64


Theorem:

Falls

A

n ∈ N : (

A

k ∈ N : (k < n → p(k)) → p(n)) P

dann gilt

A

n ∈ N : p(n) Q

Beweis: Zu zeigen: P → Q

Kontrapositionsbeweis: Wir zeigen, dass ¬Q → ¬P

Annahme: ¬Q := ¬(

A

n ∈ N : p(n)) ≡

E

n ∈ N : ¬p(n).

> wohlfundierte Ordnung auf N: es gibt keine unendliche Folge

x1, . . . , xn, . . . mit x1 > x2 > · · · > xn > . . . .

Sei Y = {n ∈ N | ¬p(n)} 6= ∅. Dann hat Y ein minimales Element m, d.h.

E

m(m ∈ Y ∧ (

A

k ∈ N : (k < m → k 6∈ Y ))) = ¬P.

65


Theorem:

Falls

A

n ∈ N : (

A

k ∈ N : (k < n → p(k)) → p(n)) P

dann gilt

A

n ∈ N : p(n) Q

Verallgemeinerung

- beliebige Menge A statt N

- < Ordnung auf A

- < wohlfundiert (es gibt keine unendliche Folge x1, . . . , xn, . . . mit

x1 > x2 > · · · > xn > . . . )

66

Beispiel

Satz: Jede naturliche Zahl n ≥ 2 lasst sich als Produkt von Primzahlen darstellen.

p(n): n ≥ 2 → n lasst sich als Produkt von Primzahlen darstellen.

Beweis: Sei n ∈ N, n ≥ 2, beliebig gewahlt.

Induktionsvoraussetzung: p(k) gilt fur alle k < n

Induktionsschluss: Folgere p(n) aus der Induktionsvoraussetzung.

Fallunterscheidung:

Fall 1: n Primzahl. Dann lasst sich n als Produkt von Primzahlen

darstellen (n = n)

Fall 2: n keine Primzahl. Dann n = k1 · k2, mit k1, k2 ∈ N, k1, k2 ≥ 2.

Da aber ki < n, i = 1, 2 ist nach Induktionsvoraussetzung bereits eine

Darstellung als Produkt von Primzahlen fur ki bekannt.

Multipliziert man diese beiden Produkte miteinander, so erhalt man

eine Darstellung fur n.

67

Fehlerquellen

Haufige Fehler bei Induktionsbeweisen

• es gibt unendliche absteigende Ketten x1 > x2 > . . .

• Induktionsanfang inkorrekt

• Bei Induktionsschritt die Grenzfalle nicht bedacht

68

Fehlerquellen

Was ist hier falsch?

Behauptung: Alle Menschen haben die gleiche Haarfarbe

p(n) : In einer Menge von n Menschen haben alle die gleiche Haarfarbe

Induktionbasis: n = 1

Fur eine Menge mit nur einem Menschen gilt die Behauptung trivial

69

Fehlerquellen




Induktionsvoraussetzung: p(n) wahr.

Induktionsschritt: Beweise, dass aus p(n), p(n + 1) folgt.

n + 1 Menschen werden in eine Reihe gestellt.

Der Mensch links außen wird rausgeschickt. Es bleiben nur n Menschen.

Nun kann die Induktionsbehauptung angewendet werden und alle

verbliebenen haben die gleiche Haarfarbe (mit dem rechts außen).

70

Fehlerquellen




Induktionsvoraussetzung: p(n) wahr.

Induktionsschritt: Beweise, dass aus p(n), p(n + 1) folgt.

n + 1 Menschen werden in eine Reihe gestellt.

Der Mensch rechts außen wird rausgeschickt. Es bleiben nur n Menschen.

Die Induktionsbehauptung kann angewendet werden und alle

verbliebenen haben die gleiche Haarfarbe (mit dem links außen).

Also haben die beiden außen die gleiche Haarfarbe, wie die in

der Mitte, und die haben auch alle die gleiche Haarfarbe

Also haben alle n + 1 Menschen die gleiche Haarfarbe.

71

Strukturelle Induktion

Bei der vollstandigen Induktion werden Eigenschaften der naturlichen

Zahlen bewiesen.

Bei der strukturellen Induktion werden Eigenschaften fur Mengen bewiesen,

deren Elemente aus Grundelementen durch eine endliche Anzahl von

Konstruktionsschritten (unter Verwendung bereits konstruierter Elemente)

bzw. mittels eines Erzeugungssystems entstehen.

72

Induktive Definitionen

Induktive Definition von Mengen:

Induktive Definition einer Menge M aus einer Basismenge B mit

“Konstruktoren” in Σ.

(Konstruktoren sind Funktionssymbole; fur f ∈ Σ, a(f ) ∈ N ist die

Stelligkeit von f .)

Basismenge: B

Erzeugungsregel: Wenn f ∈ Σ mit Stelligkeit n und

e1, . . . , en ∈ M, dann gilt f (e1, . . . , en) ∈ M.

M ist die kleinste Menge,• die die Basismenge B enthalt,

• mit der Eigenschaft, dass fur alle f ∈ Σ mit Stelligkeit n und alle

e1, . . . , en ∈ M: f (e1, . . . , en) ∈ M.

73

Induktive Definitionen: Beispiele

(1) Menge N aller naturlichen Zahlen

Basismenge: 0

Erzeugungsregel: Wenn n ∈ N, dann gilt n + 1 ∈ N

N ist die kleinste aller Mengen A mit folgenden Eigenschaften:

(1) A enthalt 0;

(2) fur alle Elemente n, falls n ∈ A so n + 1 ∈ A.

Das bedeutet, dass:

(1) 0 ∈ N

(2) Falls n ∈ N so n + 1 ∈ N.

(3) Fur jede Menge A mit Eigenschaften (1) und (2) gilt: N ⊆ A.

74


(2) Menge Σ∗ aller Worter uber ein Alphabet Σ

Basismenge: Das leere Wort ǫ ∈ Σ∗

Erzeugungsregel: Wenn w ∈ Σ∗ und a ∈ Σ,

dann gilt wa ∈ Σ∗

Σ∗ ist die kleinste aller Mengen A mit folgenden Eigenschaften:

(1) A enthalt das leere Wort ǫ

(2) fur alle Elemente w , falls w ∈ A und a ∈ Σ, so wa ∈ A.

Das bedeutet, dass:

(1) ǫ ∈ Σ∗

(2) Falls w ∈ Σ∗ und a ∈ Σ so wa ∈ Σ∗.

(3) Fur jede Menge A mit Eigenschaften (1) und (2) gilt: Σ∗ ⊆ A.

75


(3) Bin : die Menge aller (vollstandigen) binaren Baume

Basismenge: ◦ Baum mit nur einem Knoten.

Erzeugungsregel: Wenn B1,B2 ∈ Bin, dann ist auch

Tree(B1,B2) ∈ Bin.

B B1 2

Tree(B , B )1 2

Beispiele:

= Tree( , ) = Tree( , ) = Tree( , )

76


(3) Bin : die Menge aller (vollstandigen) binaren Baume




Bin ist die kleinste aller Mengen A mit folgenden Eigenschaften:

(1) A enthalt der Baum mit nur einem Knoten ◦.(2) fur alle Elemente B1,B2, falls B1,B2 ∈ A so Tree(B1,B2) ∈ A.

Das bedeutet, dass:

(1) ◦ ∈ Bin

(2) Falls B1,B2 ∈ Bin so Tree(B1,B2) ∈ Bin.

(3) Fur jede Menge A mit Eigenschaften (1) und (2) gilt: Bin ⊆ A.

77


(4) Menge aller aussagenlogischen Formeln

Basismenge: ⊥ (falsch), ⊤ (wahr), P0,P1,P2, . . . sind

aussagenlogische Formeln (atomare Formeln)

Erzeugungsregel: Wenn F1, F2 aussagenlogische Formeln sind,

dann sind auch ¬F1, F1 ∧ F2, F1 ∨ F2,

F1 → F2, F1 ↔ F2 aussagenlogische Formeln

78

Induktive DefinitionenInduktive Definition von Mengen:

Induktive Definition einer Menge M aus einer Basismenge B mit Operationssymbole

(“Konstruktoren”) Σ (wobei a(f ) Stelligkeit von f fur f ∈ Σ).

Basismenge: B

Erzeugungsregel: Wenn f ∈ Σ mit Stelligkeit n und

e1, . . . , en ∈ M, dann gilt f (e1, . . . , en) ∈ M.

M ist die kleinste aller Mengen A mit folgenden Eigenschaften:

(1) A enthalt die Basismenge B

(2) fur alle Elemente e1, . . . , en ∈ A, und alle f ∈ Σ (mit Stelligkeit n), ist auch

f (e1, . . . , en) in A.

Dass bedeutet, dass:

(1) B ⊆ M

(2) Falls e1, . . . , en ∈ M und f ∈ Σ (mit Stelligkeit n), so f (e1, . . . , en) ∈ M.

(3) Fur jede Menge A mit Eigenschaften (1) und (2) gilt: M ⊆ A.

79


Zu zeigen:

A

x ∈ M : P(x)

(1) Induktionsbasis: Beweise, dass fur alle b ∈ B, P(b) gilt.

(2) Sei e ∈ M, e 6∈ B.

Dann e = f (e1, . . . , en), mit f ∈ Σ und e1, . . . , en ∈ M.

Induktionsvoraussetzung: Wir nehmen an, dass P(e1), . . . ,P(en) gelten.

Induktionsschluss: Folgere, dass P(e) gilt.

80


Satz. Falls:

(1) bewiesen werden kann, dass fur alle b ∈ B, P(b) gilt. (Induktionsbasis)

(2) falls e = f (e1, . . . , en) mit f ∈ Σ

unter der Annahme dass P(e1), . . . ,P(en) gelten (Induktionsvoraussetzung)

wir beweisen konnen, dass auch P(e) gilt (Induktionsschritt)

Dann gilt P(m) fur alle m ∈ M.

Beweis: Sei A = {e | P(e) wahr }.(1) Da bewiesen werden kann, dass fur alle b ∈ B, P(b) gilt, wissen wir, dass A die

Basismenge B enthalt.

(2) Da wir, aus der Annahme dass P(e1), . . . ,P(en) wahr sind, beweisen konnen,

dass auch P(e) wahr ist, wissen wir, dass

falls e1, . . . , en ∈ A, und f ∈ Σ (mit Stelligkeit n), so f (e1, . . . , en) in A.

Da M die kleinste aller Mengen mit Eigenschaften (1) und (2) ist, folgt, dass

M ⊆ A = {e | P(e) wahr }, d.h. A

m ∈ M,P(m) wahr.

81

Beispiel

Σ∗ : die Menge aller Worter uber ein Alphabet Σ

Basismenge: Das leere Wort ǫ ∈ Σ∗

Erzeugungsregel: Wenn w ∈ Σ∗ und a ∈ Σ,

dann gilt wa ∈ Σ∗

Sei die Umkehrung (Reverse) eines Wortes wie folgt definiert:

rev(ǫ) = ǫ

rev(wa) = a rev(w) mit w ∈ Σ∗ und a ∈ Σ.

82

Beispiel

Zu zeigen:

A

w1,w2 ∈ Σ∗, rev(w1w2) = rev(w2)rev(w1)

Sei w1 ∈ Σ∗, beliebig.

Zu zeigen:

A

w2 ∈ Σ∗, p(w2) wobei: p(w2) : rev(w1w2) = rev(w2)rev(w1)

Induktion uber die Struktur von w2.

(1) Induktionsbasis: Wir zeigen, dass die Eigenschaft gilt fur w2 = ǫ

(d.h. dass P(ǫ) : rev(w1ǫ) = rev(ǫ)rev(w1) wahr ist).

Beweis: rev(w1ǫ) = rev(w1) = ǫrev(w1) = rev(ǫ)rev(w1).

83

Beispiel

Zu zeigen:

A

w1,w2 ∈ Σ, rev(w1w2) = rev(w2)rev(w1)

Sei w1 ∈ Σ∗, beliebig.

Zu zeigen:

A

w2 ∈ Σ, p(w2) wobei: p(w2) : rev(w1w2) = rev(w2)rev(w1)

(2) Sei w2 ∈ Σ∗, w2 6= ǫ. Dann w2 = wa.

Induktionsvoraussetzung: Wir nehmen an, dass p(w) gilt,

d.h. dass rev(w1w) = rev(w)rev(w1).

Induktionsschluss: Wir beweisen, dass dann p(w2) gilt.

rev(w1w2) = rev(w1(wa)) = rev((w1w)a) = a rev(w1w) (Definition von rev)

= a rev(w)rev(w1) (Induktionsvoraussetzung)

= (a rev(w))rev(w1) = rev(wa)rev(w1) (Definition von rev)

= rev(w2)rev(w1)

84

Beispiel 2

Bin : Menge allen (vollstandigen) binaren Baume




B B1 2

Tree(B , B )1 2

85

Beispiel 2

Behauptung:

Fur alle B ∈ Bin, falls B n Blatter hat, so besitzt B genau n − 1 innere Knoten.

P(B) : Falls B n ≥ 1 Blatter hat,

dann besitzt B genau n − 1 innere Knoten.

(1) Induktionsbasis: Wir zeigen, dass P(B) gilt wenn B nur aus einem Knoten ◦besteht.

Beweis: Sei B Baum, der nur aus einem Knoten besteht.

Dann besteht T nur aus einem Blatt, und B hat keinen inneren Knoten. d.h.

P(B) gilt.

86

Beispiel 2 ... ctd.

(2) Sei B ∈ Bin, B nicht in der Basismenge, d.h. B = Tree(B1,B2).

Induktionsvoraussetzung: Wir nehmen an, dass P(B1),P(B2) gelten.

Induktionsschluss: Wir beweisen, dass P(B) gilt.

Beweis: Sei B = Tree(B1,B2). Dann gilt:

• n = n1 + n2, wobei n, n1, n2 Anzahl der Blatter von B,B1 bzw. B2 sind.

• mit m,m1,m2 als Anzahl innerer Knoten von B,B1 bzw. B2:

m = 1 + m1 + m2 nach Definition von B = Tree(B1,B2)

= 1 + (n1 − 1) + (n2 − 1) nach Induktionsvoraussetzung

= (n1 + n2) − 1 = n − 1.

Somit ist es bewiesen, dass

A

B ∈ Bin,P(B) gilt.

87

Zusammenfassung

• Grundlegende Beweisstrategien

• Induktion uber die naturlichen Zahlen

• Fehlerquellen

• Strukturelle Induktion

88

2. Aussagenlogik

Teil 1

23.04.2013

89

Beispiel: Das 8-Damen Problem

Man platziere acht Damen so auf einem Schachbrett, dass sie sich

gegenseitig nicht bedrohen.

90


Beschreibung des Problems

Fur jedes Feld des Schachbretts eine aussagenlogische Variable

Dij

Mit der Vorstellung, dass Dij den Wert wahr hat, wenn auf dem Feld (i , j)

eine Dame steht.

Wir benutzen kartesische Koordinaten zur Notation von Positionen

91


Beispiel: Auf dem Feld (5, 7) steht eine Dame 7→ D57 wahr.

Einschrankungen pro Feld: Fij

Falls auf dem Feld (5, 7) eine Dame steht:

• keine andere Dame auf Feld(5,8), (5,6), (5,5), (5,4),(5,3), (5,2), (5,1)

D57 → ¬D58 ∧ ¬D5,6 ∧ ¬D5,5 ∧ ¬D5,4 ∧ ¬D5,3 ∧ ¬D5,2 ∧ ¬D5,1

• keine andere Dame auf Feld(1,7), (2,7), (3,7), (4,7),(6,7), (7,7), (8,7)

D57 → ¬D17 ∧ ¬D2,7 ∧ ¬D3,7 ∧ ¬D4,7 ∧ ¬D6,7 ∧ ¬D7,7 ∧ ¬D87

• keine andere Dame auf Feld (6,8), (4,6), (3,5), (2,4),(1,3)

D57 → ¬D68 ∧ ¬D4,6 ∧ ¬D3,5 ∧ ¬D2,4 ∧ ¬D1,3

• keine andere Dame auf Feld (4,8), (6,6), (7,5), (8,4)

D57 → ¬D48 ∧ ¬D6,6 ∧ ¬D7,5 ∧ ¬D8,4

92


Beispiel: Auf dem Feld (5, 7) steht eine Dame 7→ D57 wahr.

Einschrankungen pro Feld: Fij

D57 → ¬D58 ∧ ¬D5,6 ∧ ¬D5,5 ∧ ¬D5,4 ∧ ¬D5,3 ∧ ¬D5,2 ∧ ¬D5,1

D57 → ¬D17 ∧ ¬D2,7 ∧ ¬D3,7 ∧ ¬D4,7 ∧ ¬D6,7 ∧ ¬D7,7 ∧ ¬D87

D57 → ¬D68 ∧ ¬D4,6 ∧ ¬D3,5 ∧ ¬D2,4 ∧ ¬D1,3

D57 → ¬D48 ∧ ¬D6,6 ∧ ¬D7,5 ∧ ¬D8,4

︸︷︷︸

F57

Globale Einschrankungen

Fur jedes k mit 1 ≤ k ≤ 8:

Rk := D1,k ∨ D2,k ∨ D3,k ∨ D4,k ∨ D5,k ∨ D6,k ∨ D7,k ∨ D8,k

93


Struktur: Wahrheitswerte fur die atomaren Aussagen Dij

Modell fur Fij (Rk): Wahrheitswerte fur die atomaren Aussagen Dij so dass

Fij wahr (bzw. Rk wahr).

Losung des 8-Damen Problems:

Eine aussagenlogische Struktur beschreibt eine Losung des 8-Damen-

Problems genau dann, wenn sie ein Modell der Formeln

• Fij fur alle 1 ≤ i , j ≤ 8

• Rk fur alle 1 ≤ k ≤ 8

ist.

94

Formale Logik

• Syntax

welche Formeln?

• Semantik

Modelle (Strukturen)

Wann ist eine Formel wahr (in einer Struktur)?



95

Syntax der Aussagenlogik: Logische Zeichen

⊤ Symbol fur die Formel “wahr”

⊥ Symbol fur die Formel “falsch”

¬ Negationssymbol (“nicht”)

∧ Konjunktionssymbol (“und”)

∨ Disjunktionssymbol (“oder”)

→ Implikationssymbol (“wenn . . . dann”)

↔ Symbol fur Aquivalenz (“genau dann, wenn”)

( ) die beiden Klammern

96

Vokabular der Aussagenlogik

Abzahlbare Menge von Symbolen, etwa

Π = {P0, . . . ,Pn}

oder

Π = {P0,P1, . . . }

Bezeichnungen fur Symbole in Π

• atomare Aussagen

• Atome

• Aussagenvariablen

97

Formeln der Aussagenlogik

Definition: Menge ForΠ der Formeln uber Π:

Die kleinste Menge mit:

• ⊤ ∈ ForΠ und ⊥∈ ForΠ

• Π ⊆ ForΠ

• Wenn F ,G ∈ ForΠ, dann auch

¬F , (F ∧ G), (F ∨ G), (F → G), (F ↔ G)

Elemente von ForΠ.

98

Konventionen zur Notation

• Klammereinsparungen werden nach folgenden Regeln vorgenommen:

– ¬ >p ∧ >p ∨ >p → >p ↔ (Prazedenzen),

– ∨ und ∧ sind assoziativ und kommutativ,

100

Konventionen zur Notation

• Klammereinsparungen werden nach folgenden Regeln vorgenommen:

– ¬ >p ∧ >p ∨ >p → >p ↔ (Prazedenzen),

– ∨ und ∧ sind assoziativ und kommutativ,

Beispiele: Π = {P,Q,R}

⊥, P, ¬Q, P ∧ ¬Q, (P ∨ (¬R ∧ ⊤)) sind Formeln

Wir schreiben P ∧ Q ∧ R statt (P ∧ Q) ∧ R.

101

Beispiel: 8-Damenproblem

Aussagenlogische Variablen

Di ,j bedeutet: Auf dem Feld (i , j) steht eine Dame.

Formeln

“Wenn auf dem Feld (5, 7) eine Dame steht, kann keine Dame auf Feld

(5,8), (5,6), (5,5), (5,4),(5,3), (5,2), (5,1) stehen”:

D57 → ¬D58 ∧ ¬D5,6 ∧ ¬D5,5 ∧ ¬D5,4 ∧ ¬D5,3 ∧ ¬D5,2 ∧ ¬D5,1

102

Beispiel 1

Wenn ich kein Bier zu einer Mahlzeit trinke, dann habe ich immer Fisch.

◮ ¬B→F

Immer wenn ich Fisch und Bier zur selben Mahlzeit habe, verzichte ich

auf Eiscreme.

◮ F∧B→ ¬E

Wenn ich Eiscreme habe oder Bier meide, dann ruhre ich Fisch nicht an.

◮ E∨¬B→ ¬F

103

Beispiel 1

◮ ¬B→F

◮ F∧B→ ¬E

◮ E∨¬B→ ¬F

Wir mochten wissen, welche Menus solche Diatregeln erfullen.

z.B.: Formalisierung:

• kein Bier, Fisch und Eiscreme B 7→ falsch,F 7→ wahr,E 7→ wahr

erfullt 3. Diatregel nicht!

• Bier, Fisch, keine Eiscreme B 7→ wahr,F 7→ wahr,E 7→ falsch

erfullt alle Diatregeln

104

Beispiel 1

◮ ¬B→F

◮ F∧B→ ¬E

◮ E∨¬B→ ¬F

Wir mochten wissen, welche Menus solche Diatregeln erfullen.

z.B.: Formalisierung:

0:falsch, 1:wahr A : {B,F ,E} → {0, 1}

• kein Bier, Fisch und Eiscreme A(B) = 0,A(F ) = 1,A(E) = 1

erfullt 3. Diatregel nicht!

• Bier, Fisch, keine Eiscreme A(B) = 1,A(F ) = 1,A(E) = 0

erfullt alle Diatregeln

105

Semantik der Aussagenlogik

Π eine aussagenlogische Signatur

Aussagenvariablen fur sich haben keine Bedeutung.

Hierfur mussen Wertebelegungen (Valuationen) explizit oder implizit aus

dem Kontext zur Verfugung stehen.

Eine Valuation (Wertebelegung) ist eine Abbildung

A : Π → {0, 1}

Wir werden Wertebelegungen auch Aussagenlogische Strukturen,

Aussagenlogische Modelle oder Interpretationen nennen.

106


Π eine aussagenlogische Signatur

Aussagenvariablen fur sich haben keine Bedeutung.

Hierfur mussen Wertebelegungen (Valuationen) explizit oder implizit aus

dem Kontext zur Verfugung stehen.

Eine Wertebelegung ist eine Abbildung

A : Π → {0, 1}

Beispiel:

A B C

0 1 0(Bei drei Symbolen gibt es 8 mogliche Modelle)

107


Auswertung von Formeln

Sei A : Π → {0, 1} eine Wertebelegung.

A∗ : ForΠ → {0, 1} wird wie folgt definiert:

A∗(⊥) = 0

A∗(⊤) = 1

A∗(P) = A(P)

108





A∗(¬F ) =

0 falls A∗(F ) = 1

1 falls A∗(F ) = 0

109





A∗(F1 ∧ F2) =

0 falls A∗(F1) = 0 oder A∗(F2) = 0

1 falls A∗(F1) = A∗(F2) = 1

110





A∗(F1 ∧ F2) =

0 falls A∗(F1) = 0 oder A∗(F2) = 0

1 falls A∗(F1) = A∗(F2) = 1

A∗(F1 ∨ F2) =

0 falls A∗(F1) = A∗(F2) = 0

1 falls A∗(F1) = 1 oder A∗(F2) = 1

111





A∗(F1 → F2) =

1 falls A∗(F1) = 0 oder A∗(F2) = 1

0 falls A∗(F1) = 1 und A∗(F2) = 0

A∗(F1 ↔ F2) =

1 falls A∗(F1) = A∗(F2)

0 sonst

112

Wahrheitstafel fur die logischen Operatoren

P ¬P

0 1

1 0

∧ 0 1

0 0 0

1 0 1

∨ 0 1

0 0 1

1 1 1

→ 0 1

0 1 1

1 0 1

↔ 0 1

0 1 0

1 0 1

113



Sei A : Π → {0, 1} eine Π-Valuation.

A∗ : ForΠ → {0, 1} wird induktiv uber Aufbau von F wie folgt definiert:

A∗(⊥) = 0

A∗(⊤) = 1

A∗(P) = A(P)

A∗(¬F ) = 1−A∗(F )

A∗(FρG) = Bρ(A∗(F ),A∗(G))

Bρ(x , y) berechnet entschpr. der Wahrheitstafel fur ρ

z.B. : B∨(0, 1) = (0 ∨ 1) = 1; B→(1, 0) = (1 → 0) = 0

Wir schreiben normalerweise A statt A∗.

114

Beispiel

Sei A : {P,Q,R} → {0, 1} mit A(P) = 1,A(Q) = 0,A(R) = 1.

A∗((P ∧ (Q ∨ ¬P)) → R) = A∗(P ∧ (Q ∨ ¬P) → A∗(R)

= (A∗(P) ∧ A∗(Q ∨ ¬P)) → A∗(R)

= (A(P) ∧ (A(Q) ∨ ¬A(P))) → A(R)

= (1 ∧ (0 ∨ ¬1)) → 1

= 1

115

Wahrheitstabellen: Beispiel

F = (A ∨ C) ∧ (B ∨ ¬C)

A B C (A ∨ C) ¬C (B ∨ ¬C) (A ∨ C) ∧ (B ∨ ¬C)

0 0 0 0 1 1 0

0 0 1 1 0 0 0

0 1 0 0 1 1 0

0 1 1 1 0 1 1

1 0 0 1 1 1 1

1 0 1 1 0 0 0

1 1 0 1 1 1 1

1 1 1 1 0 1 1

116

Modell einer Formel(menge)

Definition: Interpretation A ist Modell einer Formel F ∈ ForΠ, falls

A∗(F ) = 1.

Definition: Interpretation A ist Modell einer Formelmenge M ⊆ ForΠ, falls

A∗(F ) = 1 fur alle F ∈ M

Notation:

A |= F

A |= M

117

Beispiel

F = (A ∨ C) ∧ (B ∨ ¬C)

A B C (A ∨ C) ¬C (B ∨ ¬C) (A ∨ C) ∧ (B ∨ ¬C)

0 0 0 0 1 1 0

0 0 1 1 0 0 0

0 1 0 0 1 1 0

0 1 1 1 0 1 1

1 0 0 1 1 1 1

1 0 1 1 0 0 0

1 1 0 1 1 1 1

1 1 1 1 0 1 1

Sei A : {P,Q,R} → {0, 1} mit A(P) = 0,A(Q) = 1,A(R) = 1.

A |= (A ∨ C) ∧ (B ∨ ¬C)

A |= {(A ∨ C), (B ∨ ¬C)}

118

Gultigkeit und Erfullbarkeit

Definition: F gilt in A (oder A ist Modell von F ) gdw. A(F ) = 1.

Notation: A |= F

Definition: F ist (allgemein-) gultig (oder eine Tautologie) gdw.: A |=

F , fur alle A : Π → {0, 1}

Notation: |= F

Definition: F heißt erfullbar gdw. es A : Π → {0, 1} gibt, so dass A |= F .

Sonst heißt F unerfullbar (oder eine Kontradiktion).

119

Beispiel

F = (A ∨ C) ∧ (B ∨ ¬C)

A B C (A ∨ C) ¬C (B ∨ ¬C) (A ∨ C) ∧ (B ∨ ¬C)

0 0 0 0 1 1 0

0 0 1 1 0 0 0

0 1 0 0 1 1 0

0 1 1 1 0 1 1

1 0 0 1 1 1 1

1 0 1 1 0 0 0

1 1 0 1 1 1 1

1 1 1 1 0 1 1

F ist nicht allgemeingultig:

A1(F ) = 0 fur A1 : {P,Q,R} → {0, 1} mit A(P) = A(Q) = A(R) = 0.

F ist erfullbar (also ist F nicht unerfullbar):

A2(F ) = 1 fur A : {P,Q,R} → {0, 1} mit A(P) = 0,A(Q) = 1,A(R) = 1.

120

Tautologien und Kontradiktionen

Tautologien: Formel, die stets wahr sind.

Beispiele: p ∨ (¬p) (Prinzip vom ausgeschlossenen Dritten)

(Tertium non datur)

p ↔ ¬¬p (Prinzip der doppelten Negation)

Kontradiktionen: Formel, die stets falsch sind.

Beispiel: p ∧ ¬p

• Die Negation einer Tautologie ist eine Kontradiktion

• Die Negation einer Kontradiktion ist eine Tautologie

121

Beispiele

Die folgenden Formeln sind Tautologien:

(1) (p → ¬p) → (¬p)

(2) (p ∧ (p → q)) → q

(3) (p ∧ q) → p

(p ∧ q) → q

(4) p → (p ∨ q)

q → (p ∨ q)

(5) (p → q) → [(q → r) → (p → r)]

(6) (((p → q) ∧ (q → r)) ∧ p) → r

122

Folgerung und Aquivalenz

Definition: F impliziert G (oder G folgt aus F ),

gdw.: fur alle A : Π → {0, 1} gilt: Wenn A |= F , dann A |= G .

Notation: F |= G

Definition: F und G sind aquivalent

gdw.: fur alle A : Π → {0, 1} gilt: A |= F gdw. A |= G .

Notation: F ≡ G .

Erweiterung auf Formelmengen N in naturlicher Weise, z.B.:

N |= G gdw.: fur alle A : Π → {0, 1} gilt:

falls A |= F , fur alle F ∈ N,

so A |= G .

123

Beispiel

F = (A ∨ C) ∧ (B ∨ ¬C) G = (A ∨ B)

Uberprufe, ob F |= G : Ja, F |= G

A B C (A ∨ C) (B ∨ ¬C) (A ∨ C) ∧ (B ∨ ¬C) (A ∨ B)

0 0 1 1 0 0 0

0 0 0 0 1 0 0

0 1 1 1 1 1 1

0 1 0 0 1 0 1

1 0 1 1 0 0 1

1 0 0 1 1 1 1

1 1 1 1 1 1 1

1 1 0 1 1 1 1

124

Beispiel

F = (A ∨ C) ∧ (B ∨ ¬C) G = (A ∨ B)

Uberprufe, ob F |= G : Ja, F |= G

.... aber es ist nicht wahr dass G |= F (Notation: G 6|= F )

A B C (A ∨ C) (B ∨ ¬C) (A ∨ C) ∧ (B ∨ ¬C) (A ∨ B)

0 0 1 1 0 0 0

0 0 0 0 1 0 0

0 1 1 1 1 1 1

0 1 0 0 1 0 1

1 0 1 1 0 0 1

1 0 0 1 1 1 1

1 1 1 1 1 1 1

1 1 0 1 1 1 1

125

Zusammenfassung

• Syntax (Formeln)

• Semantik

Wertebelegungen (Valuationen, Modelle)

Wahrheitstafel fur die logischen Operatoren

Auswertung von Formeln / Wahrheitstabellen

Modell einer Formel(menge)

Gultigkeit und Erfullbarkeit


Folgerung und Aquivalenz

126

2. Aussagenlogik

Teil 2

30.04.2012

127


Tautologien, allgemeingultige Formeln:

Formeln, die stets wahr sind.

Kontradiktionen, unerfullbare Formeln:

Formel, die stets falsch sind.

• Die Negation einer Tautologie ist eine Kontradiktion

• Die Negation einer Kontradiktion ist eine Tautologie

Theorem. F ist allgemeingultig gdw. ¬F ist unerfullbar.

Beweis 1: Aus der Wahrheitstafel.

Beweis 2: F allgemeingultig gdw. A(F )=1 fur alle A:Π→{0, 1}

gdw. A(¬F )=0 fur alle A:Π→{0, 1} gdw. ¬F unerfullbar

128

Erster Kalkul: Wahrheitstafelmethode

Erfullbarkeitstest:

Jede Formel F enthalt endlich viele Aussagenvariablen.

A(F ) ist nur von den Werten dieser Aussagenvariablen abhangig.

F enthalt n Aussagenvariablen:

⇒ 2n Wertbelegungen notwendig um zu uberprufen,

ob F erfullbar ist oder nicht.

⇒ Wahrheitstafel

⇒ Das Erfullbarkeitsproblem ist entscheidbar

(Cook’s Theorem: NP-vollstandig)

Es existieren viel bessere Methoden als Wahrheitstafeltests um die

Erfullbarkeit einer Formel zu uberprufen.

129

Folgerung

Definition: F impliziert G (oder G folgt aus F ),

gdw.: fur alle A : Π → {0, 1} gilt: Wenn A |= F , dann A |= G .

Notation: F |= G

Erweiterung auf Formelmengen N in naturlicher Weise, z.B.:

N |= G gdw.: fur alle A : Π → {0, 1} gilt:

falls A |= F , fur alle F ∈ N,

so A |= G .

130

Aquivalenz

Definition: F und G sind aquivalent

gdw.: fur alle A : Π → {0, 1} gilt: A |= F gdw. A |= G .

Notation: F ≡ G .

Zwei Formeln sind logisch aquivalent, wenn sie in den gleichen Modellen

wahr sind

Beispiel:

(P → Q) ≡ (¬Q → ¬P) (Kontraposition)

131

Wichtige Aquivalenzen

Die folgenden Aquivalenzen sind fur alle Formeln F ,G ,H gultig:

(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)

132



(¬¬F ) ≡ F (Doppelte Negation)

¬(F ∧ G) ≡ (¬F ∨ ¬G)

¬(F ∨ G) ≡ (¬F ∧ ¬G) (De Morgan’s Regeln)

(F → G) ≡ (¬G → ¬F ) (Kontraposition)

(F → G) ≡ (¬F ∨ G) (Elimination Implikation)

F ↔ G ≡ (F → G) ∧ (G → F ) (Elimination Aquivalenz)

133



(F ∧ G) ≡ F , falls G Tautologie

(F ∨ G) ≡ ⊤, falls G Tautologie (Tautologieregeln)

(F ∧ G) ≡ ⊥, falls G unerfullbar

(F ∨ G) ≡ F , falls G unerfullbar (Tautologieregeln)

134

Wichtige Aquivalenzen mit ⊤/⊥

(A ∧ ¬A) ≡ ⊥

(A ∨ ¬A) ≡ ⊤ (Tertium non datur)

(A ∧ ⊤) ≡ A

(A ∧ ⊥) ≡ ⊥

135

Wichtige Aquivalenzen (Zusammengefasst)

(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 (Doppelte Negation)

¬(F ∧ G) ≡ (¬F ∨ ¬G)

¬(F ∨ G) ≡ (¬F ∧ ¬G) (De Morgan’s Regeln)

(F → G) ≡ (¬G → ¬F ) (Kontraposition)

(F → G) ≡ (¬F ∨ G) (Elimination Implikation)

F ↔ G ≡ (F → G) ∧ (G → F ) (Elimination Aquivalenz)

136

Terminologie

Eine Formel F , die als Teil einer Formel G auftritt,

heißt Teilformel von G .

• F ist eine Teilformel von F

• F = ¬G und

H Teilformel von G

→ H Teilformel von F

• F = F1 ρ F2

(wo ρ ∈ {∨,∧,⇒,⇔})

H Teilformel von F1 oder F2

→ H Teilformel von F

137

Substitutionstheorem

Theorem.

Seien F und G aquivalente Formeln. Sei H eine Formel mit (mindestens)

einem Vorkommen der Teilformel F .

Dann ist H aquivalent zu H′, wobei H′ aus H hervorgeht, indem (irgend)

ein Vorkommen von F in H durch G ersetzt wird.

Beispiel:

A ∨ B ≡ B ∨ A

impliziert

(C ∧ (A ∨ B)) ≡ (C ∧ (B ∨ A))

138


Theorem.

Seien F und G aquivalente Formeln. Sei H eine Formel mit (mindestens)

einem Vorkommen der Teilformel F .

Dann ist H aquivalent zu H′, wobei H′ aus H hervorgeht, indem (irgend)

ein Vorkommen von F in H durch G ersetzt wird. p(H)

Beweis: Strukturelle Induktion.

Induktionsbasis: Beweisen, dass p(H) fur alle Formeln H in {⊥,⊤} ∪ Π gilt.

Beweis: Falls H∈{⊥,⊤}∪Π und F Teilformel von H, so muss F = H sein.

Dann ist die Formel H′, die aus H hervorgeht, indem F (= die ganze

Formel H) durch G ersetzt wird, gleich G .

Aber dann: H = F ≡ G = H′.

139


Beweis: (Fortsetzung)

Sei H eine Formel, H 6∈ {⊥,⊤} ∪ Π. Sei F eine Teilformel von H.

Fall 1: F = H. Dann H′ = G (wie vorher), so H = F ≡ G = H′.

Fall 2: F 6= H.

Induktionsvoraussetzung: Annahme: p(H′) gilt fur alle dir. Teilformeln H′ von H.

Induktionsschritt: Beweis, dass p(H) gilt (durch Fallunterscheidung):

Fall 2.1: H = ¬H1. Da F 6= H, ist F eine Teilformel von H1.

Induktionvoraussetzung: p(H1) gilt, d.h. H1 ≡ H′

1 , wobei H′

1 aus H1 hervorgeht,

indem (irgend) ein Vorkommen von F in H1 durch G ersetzt wird.

Da H = ¬H1, ist H′ = ¬H′

1 .

Dann fur alleA : Π → {0, 1}:A(H)=A(¬H1)=¬A(H1)I .V .= ¬A(H′

1 )=A(¬H′

1)=A(H′).

Somit ist bewiesen, dass H ≡ H′.

140


Beweis: (Fortsetzung)

Induktionsschritt: Beweis, dass p(H) gilt (durch Fallunterscheidung):

Fall 2.2: H = H1 op H2. Da F 6= H, ist F Teilformel von H1 oder von H2.

Fall 2.2.1 F ist eine Teilformel von H1.

Induktionvoraussetzung: p(H1) gilt, d.h. H1 ≡ H′

1 , wobei H′

1 aus H1 hervorgeht,

indem (irgend) ein Vorkommen von F in H1 durch G ersetzt wird.

Da H = H1 op H2, und F in H1 vorkommt, so H′ = H′

1 op H2.

Dann fur alle A : Π → {0, 1}: A(H)=A(H1 op H2)=A(H1) op A(H2)I .V .=

A(H′

1) op A(H2)=A(H′

1 op H2) = A(H′).

Somit ist bewiesen, dass H ≡ H′.

Fall 2.2.2 F ist eine Teilformel von H2. Analog.

141

Ein zweiter Kalkul: Logische Umformung

Definition: Aquivalenzumformung

• (Wiederholte) Ersetzung einer (Unter-)Formel durch aquivalente

Formel

• Anwendung des Substitutionstheorems

Theorem

Aquivalenzumformung bildet mit den aufgelisteten wichtigen Aquivalen-

zen einen vollstandigen Kalkul:

Wenn F und G logisch aquivalent sind, kann F in G umgeformt werden.

142

Beispiel

(P → Q) ∧ ¬((Q → R) → (P → R))

≡ (¬P ∨ Q) ∧ ¬((¬Q ∨ R) → (¬P ∨ R)) (Elimination Implikation)

≡ (¬P ∨ Q) ∧ ¬(¬(¬Q ∨ R) ∨ (¬P ∨ R)) (Elimination Implikation)

≡ (¬P ∨ Q) ∧ (¬¬(¬Q ∨ R) ∧ ¬(¬P ∨ R)) (De Morgan’s Regel,∨)

≡ (¬P ∨ Q) ∧ ((¬Q ∨ R) ∧ (¬¬P ∧ ¬R)) (Doppelte Negation, De Morgan, ∨)

≡ (¬P ∨ Q) ∧ ((¬Q ∨ R) ∧ (P ∧ ¬R)) (Doppelte Negation)

≡ (¬P ∨ Q) ∧ ((¬Q ∧ P ∧ ¬R) ∨ (R ∧ P ∧ ¬R)) (Distributivitat)

≡ (¬P ∨ Q) ∧ ((¬Q ∧ P ∧ ¬R) ∨ (R ∧ ¬R ∧ P)) (Kommutativitat)

≡ (¬P ∨ Q) ∧ ((¬Q ∧ P ∧ ¬R) ∨ ⊥) (Aquivalenzen mit ⊥)

≡ (¬P ∨ Q) ∧ (¬Q ∧ P ∧ ¬R) (Aquivalenzen mit ⊥)

≡ (¬P ∧ ¬Q ∧ P ∧ ¬R) ∨ (Q ∧ ¬Q ∧ P ∧ ¬R) (Distributivitat)

≡ (¬P ∧ P ∧ ¬Q ∧ ¬R) ∨ (Q ∧ ¬Q ∧ P ∧ ¬R) (Kommutativitat)

≡ ((¬P ∧ P) ∧ ¬Q ∧ ¬R) ∨ ((Q ∧ ¬Q) ∧ P ∧ ¬R) (Assoziativitat)

≡ ⊥ ∨ ⊥≡⊥ (Aquivalenzen mit ⊥)

143

Allgemeingultigkeit/Folgerung

F ,G Formeln

Theorem. F |= G gdw. |= F → G .

Beweis:

F |= G g.d.w. fur alle A : Π → {0, 1}, falls A(F ) = 1 so A(G) = 1

g.d.w. fur alle A : Π → {0, 1}, (A(F ) → A(G)) = 1

g.d.w. fur alle A : Π → {0, 1}, A(F → G) = 1

g.d.w. |= F → G

144


F ,G Formeln; N Formelmenge.

Theorem. N ∪ {F} |= G gdw. N |= F → G .

Beweis: “⇒”

Annahme: N ∪ {F} |= G d.h. fur alle A:Π→{0, 1},

falls [A(H)=1 fur alle Formeln H∈N∪{F}] so A(G)=1.

Wir beweisen, dass N |= F → G , d.h. fur alle A : Π → {0, 1}

falls [A(H) = 1 fur alle Formeln H ∈ N] so A(F → G) = 1.

Sei A : Π → {0, 1} mit A(H) = 1 fur alle Formeln H ∈ N.

Fall 1: A(F ) = 0. Dann A(F → G) = 1.

Fall 2: A(F ) = 1, d.h. [A(H) = 1 fur alle Formeln H ∈ N ∪ {F}]. Dann

A(G) = 1 und somit A(F → G) = 1.

145




Beweis: “⇐”

Annahme: N |= F → G d.h. fur alle A:Π→{0, 1},

falls [A(H)=1 fur alle Formeln H∈N] so A(F → G)=1.

Wir beweisen, dass N ∪ {F} |= G , d.h. fur alle A : Π → {0, 1}

falls [A(H) = 1 fur alle Formeln H ∈ N ∪ {F}] so A(G) = 1.

Sei A : Π → {0, 1} mit A(H) = 1 fur alle Formeln H ∈ N ∪ {F}.

Dann (i) A(F ) = 1 und

(ii) [A(H) = 1 fur alle Formeln H ∈ N], also A(F → G) = 1.

Es folgt, dass 1 = A(F → G) = (A(F ) → A(G)) = (1 → A(G)) = A(G),

so A(G) = 1.

146


F ,G Formeln.

Theorem. F ≡ G gdw. |= F ↔ G .

Beweis:

F ≡ F g.d.w. fur alle A : Π → {0, 1}, A(F ) = A(G)

g.d.w. fur alle A : Π → {0, 1}, (A(F ) ↔ A(G)) = 1

g.d.w. fur alle A : Π → {0, 1}, A(F ↔ G) = 1

g.d.w. |= F ↔ G

147

Allgemeingultigkeit/Folgerung:

Zusammenfassung


Theorem. F |= G gdw. |= F → G .


Theorem. F ≡ G gdw. |= F ↔ G .

148

Unerfullbarkeit/Allgemeingultigkeit/Folgerung

F ,G Formeln.


Beweis auf Seite 128.

Theorem. F |= G gdw. F ∧ ¬G ist unerfullbar.

Beweis:

F |= G gdw. |= F → G d.h. F → G allgemeingultig

gdw. ¬(F → G) unerfullbar.

gdw. F ∧ ¬G unerfullbar.

... da ¬(F → G) ≡ ¬(¬F ∨ G) ≡ ¬¬F ∧ ¬G ≡ F ∧ ¬G .

149



Theorem. N |= G gdw. N ∪ ¬G ist unerfullbar.

Beweis: “⇒”

Annahme: N |= G d.h. fur alle A:Π→{0, 1},

falls [A(H)=1 fur alle Formeln H∈N] so A(G)=1.

Zu zeigen: N ∪ ¬G unerfullbar.

Beweis durch Widerspruch: Wir nehmen an, N ∪ ¬G erfullbar,

d.h. es gibt A:Π→{0, 1}, mit

[A(H)=1 fur alle Formeln H∈N ∪ {¬G}].

Dann [A(H)=1 fur alle Formeln H∈N] und A(¬G) = 1 (d.h.

A(G) = 0). Widerspruch.

150




Beweis: “⇐”

Annahme: N ∪ ¬G unerfullbar.

Zu zeigen: N |= G d.h. fur alle A:Π→{0, 1},

falls [A(H)=1 fur alle Formeln H∈N] so A(G)=1.

Beweis: Sei A:Π→{0, 1}, mit [A(H)=1 fur alle Formeln H∈N].

Falls A(G) = 0, ware A ein Modell fur N ∪ {¬G}. Das ist

aber unmoglich, da wir angenommen haben, dass N ∪ {¬G}

unerfullbar ist.

Es folgt, dass A(G) = 1.

151

Unerfullbarkeit/Allgemeingultigkeit/Folgerung:

Zusammenfassung



Theorem. F |= G gdw. F ∧ ¬G ist unerfullbar.


Nota bene: falls N unerfullbar, so N |= G fur jede Formel G

... auch fur ⊥.

Notation: N |= ⊥ fur N unerfullbar.

152

Zusammenfassung

• Erfullbarkeit, Allgemeingultigkeit

• Erster Kalkul: Wahrheitstafelmethode

• Folgerung, Aquivalenz

• Wichtige Aquivalenzen

• Ein zweiter Kalkul: Logische Umformung

• Unerfullbarkeit/Allgemeingultigkeit/Folgerung

153

2. Aussagenlogik

Teil 3

06.05.2013

154

Unser Ziel

Kalkul(e) zur systematischen Uberprufung von Erfullbarkeit

(fur Formeln und/oder Formelmengen)

Dazu brauchen wir “Normalformen”

155

Normalformen

Definition:

• Atom: aussagenlogische Variable

• Literal: Atom, oder

Negation eines Atoms

Beispiel. Sei Π = {P,Q,R}.

Atome: P, Q, R

Literale: P, ¬P, Q, ¬Q, R, ¬R

156

Normalformen

Definition:

• Atom: aussagenlogische Variable

• Literal: Atom, oder

Negation eines Atoms

Definition:

Klausel: Eine Disjunktion von Literalen

• mehrstellige Disjunktionen (P ∨ ¬Q ∨ R), (P ∨ P ∨ ¬Q)

• einstellige Disjunktionen P

• die nullstellige Disjunktion (leere Klausel) ⊥

157

Normalformen

Definition:

Konjunktive Normalform (KNF): Eine Konjunktion von Disjunktionen von

Literalen, d.h., eine Konjunktion von Klauseln

mehrstellig, einstellig oder nullstellig

Beispiele:

(P ∨ ¬Q) ∧ (Q ∨ ¬R ∨ ¬S)

P ∨ Q

P ∧ (Q ∨ R)

P ∧ Q

P ∧ P

⊤

158

Normalformen

Definition:

Disjunktive Normalform (DNF): Eine Disjunktion von Konjunktionen von

Literalen.

mehrstellig, einstellig oder nullstellig

Beispiele:

(P ∧ ¬Q) ∨ (Q ∧ ¬R ∧ ¬S)

P ∧ Q

P ∨ (Q ∧ R)

P ∨ Q

P ∨ P

⊥

159

Normalformen

Eigenschaften:

• Zu jeder aussagenlogischen Formel gibt es:

- eine aquivalente Formel in KNF

- eine aquivalente Formel in DNF

• Diese aquivalenten Formeln in DNF bzw. KNF sind nicht eindeutig

• Solche Formeln konnen aus einer Wahrheitstafel abgelesen werden

• Solche Formeln konnen durch Umformungen hergestellt werden

160

Beispiel: DNF

F : (P ∨ Q) ∧ ((¬P ∧ Q) ∨ R)

P Q R (P ∨ Q) ¬P (¬P ∧ Q) ((¬P ∧ Q) ∨ R) F

0 0 0 0 1 0 0 0

0 0 1 0 1 0 1 0

0 1 0 1 1 1 1 1

0 1 1 1 1 1 1 1

1 0 0 1 0 0 0 0

1 0 1 1 0 0 1 1

1 1 0 1 0 0 0 0

1 1 1 1 0 0 1 1

DNF: (¬P ∧ Q ∧ ¬R) ∨ (¬P ∧ Q ∧ R) ∨ (P ∧ ¬Q ∧ R) ∨ (P ∧ Q ∧ R)

161

Beispiel: KNF

F : (P ∨ Q) ∧ ((¬P ∧ Q) ∨ R)

P Q R (P ∨ Q) ¬P (¬P ∧ Q) ((¬P ∧ Q) ∨ R) F ¬F

0 0 0 0 1 0 0 0 1

0 0 1 0 1 0 1 0 1

0 1 0 1 1 1 1 1 0

0 1 1 1 1 1 1 1 0

1 0 0 1 0 0 0 0 1

1 0 1 1 0 0 1 1 0

1 1 0 1 0 0 0 0 1

1 1 1 1 0 0 1 1 0

DNF fur ¬F : (¬P ∧¬Q ∧¬R)∨ (¬P ∧¬Q ∧ R)∨ (P ∧¬Q ∧¬R)∨ (P ∧Q ∧¬R)

KNF fur F : (P ∨ Q ∨ R) ∧ (P ∨ Q ∨ ¬R) ∧ (¬P ∨ Q ∨ R) ∧ (¬P ∨ ¬Q ∨ R)

162

Normalformen

DNF fur F :∨

A:{P1,...,Pn}→{0,1}

A(F )=1

(PA(P1)1 ∧ · · · ∧ P

A(Pn)n )

wobei:

P0 = ¬P

P1 = P

Theorem

Fur alle Interpretationen A′ : {P1, . . . ,Pn} → {0, 1}:

A′(F ) = 1 gdw. A′(∨

A:{P1,...,Pn}→{0,1}

A(F )=1

(PA(P1)1 ∧ · · · ∧ P

A(Pn)n )) = 1.

163

Normalformen

DNF fur F :∨

A:{P1,...,Pn}→{0,1}

A(F )=1

(PA(P1)1 ∧ · · · ∧ P

A(Pn)n )

wobei:

P0 = ¬P

P1 = P

KNF fur F: ¬F ′,

wobei F ′ die DNF von ¬F ist.

KNF fur F :∧

A:{P1,...,Pn}→{0,1}

A(F )=0

(P1−A(P1)1 ∨ · · · ∨ P

1−A(Pn)n )

164

Normalformen

Eigenschaften:

• Zu jeder aussagenlogischen Formel gibt es:

- eine aquivalente Formel in KNF

- eine aquivalente Formel in DNF

• Diese aquivalenten Formeln in DNF bzw. KNF sind nicht eindeutig

• Solche Formeln konnen aus einer Wahrheitstafel abgelesen werden

• Solche Formeln konnen durch Umformungen hergestellt werden

165

Umformung in KNF

Vier Schritte:

1. Elimination von ↔

Verwende A ↔ B ≡ (A → B) ∧ (B → A)

2. Elimination von →

Verwende A → B ≡ (¬A ∨ B)

3. “Nach innen schieben” von ¬

Verwende de Morgans Regeln und ¬¬A ≡ A

7→ Negationsnormalform (NNF)

Eine logische Formel ist in Negationsnormalform (NNF),

falls die Negationsoperatoren in ihr nur direkt uber

atomaren Aussagen vorkommen.

166

Umformung in KNF

Vier Schritte:






Verwende de Morgans Regeln und ¬¬A ≡ A (NNF)

4. “Nach innen schieben” von ∨

Verwende Distributivitat von ∨ uber ∧

167

Umformung in KNF: Beispiel

Gegeben:

P ↔ (Q ∨ R)


(P → (Q ∨ R)) ∧ ((Q ∨ R) → P)


(¬P ∨ Q ∨ R) ∧ (¬(Q ∨ R) ∨ P)

3. “Nach innen schieben” von ¬ (NNF)

(¬P ∨ Q ∨ R) ∧ ((¬Q ∧ ¬R)) ∨ P)

4. “Nach innen schieben” von ∨

(¬P ∨ Q ∨ R) ∧ (¬Q ∨ P) ∧ (¬R ∨ P))

168

Umformung in DNF

Vier Schritte:






Verwende de Morgans Regeln und ¬¬A ≡ A (NNF)

4. “Nach innen schieben” von ∧

Verwende Distributivitat von ∧ uber ∨

169

Umformung in DNF: Beispiel

Gegeben:

P ↔ (Q ∨ R)

1. Negationsnormalform (NNF) (s. Seite 168):

(¬P ∨ Q ∨ R) ∧ ((¬Q ∧ ¬R) ∨ P)

2. “Nach innen schieben” von ∧

(¬P ∧ ((¬Q ∧ ¬R) ∨ P)) ∨ (Q ∧ ((¬Q ∧ ¬R) ∨ P)) ∨ (R ∧ ((¬Q ∧ ¬R) ∨ P))

≡ (¬P ∧ ¬Q ∧ ¬R) ∨ (¬P ∧ P) ∨ (Q ∧ ¬Q ∧ ¬R) ∨ (Q ∧ P) ∨(R ∧ ¬Q ∧ ¬R) ∨ (R ∧ P)

≡ (¬P ∧ ¬Q ∧ ¬R) ∨ (¬P ∧ P)︸︷︷︸

≡⊥

∨ ((Q ∧ ¬Q)︸︷︷︸

≡⊥

∧¬R) ∨ (Q ∧ P) ∨

((R ∧ ¬R)︸︷︷︸

≡⊥

∧¬Q) ∨ (R ∧ P)

≡ (¬P ∧ ¬Q ∧ ¬R) ∨ (Q ∧ P) ∨ (R ∧ P)

170

Beispiel zur exponentiellen Lange der KNF

Gegeben:

An = (P11 ∧ P12) ∨ · · · ∨ (Pn1 ∧ Pn2)

Zu An aquivalente KNF∧

f :{1,...,n}→{1,2}

(P1,f (1) ∨ · · · ∨ Pn,f (n))

171


Gegeben:

An = (P11 ∧ P12) ∨ · · · ∨ (Pn1 ∧ Pn2)

n = 1 : A1 = P11∧P12 Lange: 21

n = 2 : A2 = (P11∧P12)∨(P21∧P22)

≡ ((P11∧P12)∨P21)∧((P11∧P12)∨P22)

≡ (P11∨P21)∧(P12∨P21)∧(P11∨P22)∧(P12∨P22) Lange: 22

n = 3 : A3 = (P11∧P12)∨(P21∧P22)︸︷︷︸

A2

∨(P31∧P32)

≡ ((P11∨P21)∧(P12∨P21)∧(P11∨P22)∧(P12∨P22))︸︷︷︸

KNF (A2)

∨(P31∧P32)

≡ (((P11∨P21)∧(P12∨P21)∧(P11∨P22)∧(P12∨P22))∨P31)∧(((P11∨P21)∧(P12∨P21)∧(P11∨P22)∧(P12∨P22))∨P32)

≡ (((P11∨P21∨P31)∧(P12∨P21∨P31)∧(P11∨P22∨P31)∧(P12∨P22∨P31)∧(((P11∨P21∨P32)∧(P12∨P21∨P32)∧(P11∨P22∨P32)∧(P12∨P22∨P32) Lange: 23

172


Gegeben: An = (P11 ∧ P12) ∨ · · · ∨ (Pn1 ∧ Pn2)

• Klausel in KNF von An: 2n

Beweis durch Induktion

Induktionsbasis: n = 1 : A1 in KNF, 21 Klausel.

173


Gegeben: An = (P11 ∧ P12) ∨ · · · ∨ (Pn1 ∧ Pn2)

• Klausel in KNF von An: 2n

Beweis durch Induktion

Induktionsvoraussetzung: KNF von An hat 2n Klausel

KNF (An) = C1 ∧ · · · ∧ C2n , Ci = (Li1 ∨ · · · ∨ Lini ) Klausel

Induktionsschritt: Zu zeigen: KNF von An+1 hat 2n+1 Klausel

An+1 = (P11 ∧ P12) ∨ · · · ∨ (Pn1 ∧ Pn2) ∨ (P(n+1),1 ∧ P(n+1),2)≡ ((P11 ∧ P12) ∨ · · · ∨ (Pn1 ∧ Pn2)

︸︷︷︸

An

) ∨ (P(n+1),1 ∧ P(n+1),2)

≡ (C1 ∧ · · · ∧ C2n )︸︷︷︸

KNF (An)

∨ (P(n+1),1 ∧ P(n+1),2)

≡ ((C1 ∧ · · · ∧ C2n ) ∨ P(n+1),1) ∧ ((C1 ∧ · · · ∧ C2n ) ∨ P(n+1),2)≡ (C1 ∨ P(n+1),1) ∧ · · · ∧ (C2n ∨ P(n+1),1)

︸︷︷︸

2n

∧ (C1 ∨ P(n+1),2) ∧ · · · ∧ (C2n ∨ P(n+1),2)︸︷︷︸

2n

174

KNF: Mengenschreibweise

Notation:

Klausel als Menge von Literalen

Formel in KNF als Menge von Klauseln

Beispiel:

(P ∨ Q ∨ R) ∧ (P ∨ Q ∨ ¬R) ∧ (¬P ∨ Q ∨ R) ∧ (¬P ∨ ¬Q ∨ R)

{ {P,Q,R}, {P,Q,¬R}, {¬P,Q,R}, {¬P,¬Q,R} }

175

KNF: Mengenschreibweise

Bedeutung der leeren Menge

• Leere Klausel

= leere Menge von Literalen

= leere Disjunktion

= ⊥

• Leere Menge von Klausels

= leere Konjunktion

= ⊤

176

Vereinfachung der KNF: Subsumption

Theorem (Subsumption Regel)

Enthalt eine KNF-Formel (= Klauselmenge) Klauseln K ,K ′ mit

K ⊂ K ′

dann entsteht eine aquivalente Formel, wenn K ′ weggelassen wird.

Beweis:

K = {L1, . . . , Lp} ⊆ {L1, . . . , Lp , Lp+1, . . . , Lm} = K ′

F enthalt K ∧ K ′

K ∧ K ′ = (L1 ∨ · · · ∨ Lp) ∧ ((L1 ∨ · · · ∨ Lp) ∨ Lp+1 ∨ . . . Lm)

≡ (L1 ∨ · · · ∨ Lp) = K (Absorption)

177

Das SAT-Problem (Erfullbarkeitsproblem)

Definition: SAT-Problem

Gegeben: Eine aussagenlogische Formel F

Frage: Ist F erfullbar?

NB: F allgemeingultig gdw. ¬F nicht erfullbar

178


Erfullbarkeitsproblem fur DNF Formeln

Sei F =∨n

i=1(∧m

j=1 Lij ) in DNF

F unerfullbar gdw. (∧m

j=1 Lij ) unerfullbar fur alle i = 1, . . . , n

gdw. (∧m

j=1 Lij ) enthalt zwei komplementare Literale fur alle i

179

Zusammenfassung

• Normalformen

Atome, Literale, Klauseln

Konjunktive und Disjunktive Normalform

Ablesen von DNF und KNF aus Wahrheitstafeln

Umformen in KNF/DNF

Mengenschreibweise

Subsumption

• SAT-Problem (Erfullbarkeitsproblem)

Definition


180

2. Aussagenlogik

Teil 4

07.05.2012

181



Sei F =∨n

i=1(∧m

j=1 Lij ) in DNF



gdw. (∧m


Beispiele:

(P ∧ ¬Q)︸︷︷︸

erfullbar

∨ (P ∧ Q ∧ ¬R ∧ ¬Q)︸︷︷︸

unerfullbar

erfullbar

(P ∧ ¬Q ∧ ¬P)︸︷︷︸

unerfullbar

∨ (P ∧ Q ∧ ¬R ∧ ¬Q)︸︷︷︸

unerfullbar

unerfullbar

182



Sei F =∨n

i=1(∧m

j=1 Lij ) in DNF



gdw. (∧m


Allgemeingultigkeit fur KNF Formeln

F =∧n

i=1(∨m

j=1 Lij ) in KNF ist allgemeingultig gdw. jede Disjunktion∨m

j=1 Lij zwei

komplementare Literale enthalt.

Beispiele:

(P ∨ ¬Q)︸︷︷︸

erfullbar (keine Tautologie)

∧ (P ∨ Q ∨ ¬R ∨ ¬Q)︸︷︷︸

Tautologie

keine Tautologie (nicht allgemeingultig)

(P ∨ ¬Q ∨ ¬P)︸︷︷︸

Tautologie

∧ (P ∨ Q ∨ ¬R ∨ ¬Q)︸︷︷︸

Tautologie

Tautologie (allgemeingultig)

183


Definition: SAT-Problem

Gegeben: Eine aussagenlogische Formel F

Frage: Ist F erfullbar?

Theorem (ohne Beweis)

SAT ist ein NP-vollstandiges Problem

184

NP

Zur Erinnerung:

• P ist die Klasse aller Probleme, die in polynomieller Zeit entscheidbar

sind.

• NP ist die Klasse aller Probleme, die nichtdeterministisch in

polynomieller Zeit entscheidbar sind.

Ein Entscheidungsproblem ist genau dann in NP, wenn eine gegebene

Losung fur das entsprechende Suchproblem in Polynomialzeit uberpruft

werden kann.

SAT ist in NP:

• Rate eine “Losung” (Interpretation A mit A(F ) = 1)

• Uberprufe, ob A wirklich eine “Losung” ist (i.e. ob A(F ) = 1)

kann in Polynomialzeit uberpruft werden

185

NP-Vollstandigkeit

Zur Erinnerung:

“SAT ist NP-vollstandig” heißt:

• SAT ist nichtdeterministisch in polynomieller Zeit entscheidbar

• Jedes nichtdeterministisch in polynomieller Zeit entscheidbare Problem

kann in polynomieller Zeit auf SAT reduziert werden

• Wenn es stimmt, dass NP 6= P, dann ist SAT nicht in polynomieller

Zeit entscheidbar

186

Teilklassen des Erfullbarkeitsproblems

Definition:

k-KNF Formel: KNF-Formeln, deren Klauseln hochstens k Literale haben

Beispiele:

P ∧ ¬Q 1-KNF

P ∧ (¬P ∨ Q) ∧ (R ∨ ¬Q) 2-KNF

(P ∨ Q) ∧ (P ∨ ¬Q ∨ R) 3-KNF

Alternative Definition (nicht allgemeiner):

k-KNF Formel: KNF-Formeln, deren Klauseln genau k Literale haben

Beispiele:

P ∧ ¬Q 1-KNF

(P ∨ P) ∧ (¬P ∨ Q) ∧ (R ∨ ¬Q) 2-KNF

(P ∨ P ∨ Q) ∧ (P ∨ ¬Q ∨ R) 3-KNF

187


Definition:


Theorem

• Erfullbarkeit fur Formeln in KNF: NP-vollstandig (ohne Beweis)

• Erfullbarkeit fur Formeln in 3-KNF: NP-vollstandig (Beweisidee)

188

3-SAT

Theorem

Erfullbarkeit fur Formeln in 3-KNF (3-SAT) ist NP-vollstandig

Beweis

• 3-SAT ist ein Spezialfall von SAT und deshalb wie SAT in NP.

• Um zu zeigen, dass 3-SAT ebenfalls NP-vollstandig ist, mussen wir

zeigen, dass jedes SAT Problem in polynomieller Zeit auf das 3-SAT

Problem reduzierbar ist.

189

3-SAT

Theorem


Beweis (Teil 2)

Wir zeigen, dass jedes SAT Problem in polynomieller Zeit auf das 3-SAT

Problem reduzierbar ist.

Gegeben sei eine Formel F in KNF. Wir transformieren F in eine Formel F ′

in 3-KNF, so dass:

F ist erfullbar gdw. F ′ ist erfullbar.

Eine k-Klausel sei eine Klausel mit k Literalen.

Aus einer 1- bzw 2-Klausel konnen wir leicht eine aquivalente 3-Klausel

machen, indem wir ein Literal wiederholen.

Was machen wir mit k-Klauseln fur k > 3?

190

3-SAT

Theorem


Beweis (Teil 3)

Sei C beispielsweise eine 4-Klausel der Form

C = L1 ∨ L2 ∨ L3 ∨ L4.

In einer Klauseltransformation ersetzen wir C durch die Teilformel

C0 = (L1 ∨ L2 ∨ H) ∧ (¬H ∨ L3 ∨ L4),

wobei H eine zusatzlich eingefuhrte Hilfsvariable bezeichnet.

191

Beispiel

C = P ∨ ¬Q ∨ ¬R ∨ S 7→ (P ∨ ¬Q ∨ H) ∧ (¬H ∨ ¬R ∨ S).

192

3-SAT

Theorem


Beweis (Teil 3)

Sei C beispielsweise eine 4-Klausel der Form

C = L1 ∨ L2 ∨ L3 ∨ L4.

In einer Klauseltransformation ersetzen wir C durch die Teilformel

C0 = (L1 ∨ L2 ∨ H) ∧ (¬H ∨ L3 ∨ L4),

wobei H eine zusatzlich eingefuhrte Hilfsvariable bezeichnet.

F ′ sei aus F entstanden durch Ersetzung von C durch C0.

zu zeigen: F ′ erfullbar gdw. F erfullbar

193

3-SAT

Theorem


Beweis (Teil 4)

C = L1 ∨ L2 ∨ L3 ∨ L4; C0 = (L1 ∨ L2 ∨ H) ∧ (¬H ∨ L3 ∨ L4),



“⇐”

Sei A eine erfullende Belegung fur F . A weist mindestens einem Literal aus C den

Wert 1 zu. Wir unterscheiden zwei Falle:

1) Falls L1 oder L2 den Wert 1 haben, so ist F ′ fur A(H) = 0 erfullt.

2) Falls L3 oder L4 den Wert 1 haben, so ist F ′ fur A(H) = 1 erfullt.

Also ist F ′ in beiden Fallen erfullbar.

194

3-SAT

Theorem


Beweis (Teil 5)

C = L1 ∨ L2 ∨ L3 ∨ L4; C0 = (L1 ∨ L2 ∨ H) ∧ (¬H ∨ L3 ∨ L4),



“⇒”

Sei A eine erfullende Belegung fur F ′. Wir unterscheiden zwei Falle:

1) Falls A(H) = 0, so muss A(L1) = 1 oder A(L2) = 1.

2) Falls A(H) = 1, so muss A(L3) = 1 oder A(L4) = 1

In beiden Fallen erfullt A somit auch C , i.e. auch F .

195

3-SAT

Theorem


Beweis (Teil 6)

Wir verallgemeinern die Klauseltransformation fur k ≥ 4:

Jede Klausel der Form

L1 ∨ L2 ∨ · · · ∨ Lk−1 ∨ Lk

wird durch eine Formel der Form

(L1 ∨ L2 ∨ ... ∨ Lk−2 ∨ H) ∧ (¬H ∨ Lk−1 ∨ Lk)

ersetzt.

Die Erfullbarkeitsaquivalenz folgt analog zum Fall k = 4.

196

Beispiele

Beispiel 1:

(P ∨ ¬Q ∨ R ∨ S ∨ U ∨ ¬V )

7→ (P ∨ ¬Q ∨ R ∨ S ∨ H1) ∧ (¬H1 ∨ U ∨ ¬V )

7→ (P ∨ ¬Q ∨ R ∨ H2) ∧ (¬H2 ∨ S ∨ H1) ∧ (¬H1 ∨ U ∨ ¬V )

7→ (P ∨ ¬Q ∨ H3) ∧ (¬H3 ∨ R ∨ H2)∧(¬H2 ∨ S ∨ H1) ∧ (¬H1 ∨ U ∨ ¬V )

Beispiel 2:

(P ∨ ¬Q ∨ ¬R ∨ S) ∧ (¬P ∨ Q ∨ R ∨ ¬S)

7→ (P ∨ ¬Q ∨ H1) ∧ (¬H1 ∨ ¬R ∨ S) ∧ (¬P ∨ Q ∨ R ∨ ¬S)

7→ (P ∨ ¬Q ∨ H1) ∧ (¬H1 ∨ ¬R ∨ S) ∧ (¬P ∨ Q ∨ H2) ∧ (¬H2 ∨ R ∨ ¬S)

197

Bis jetzt

• Das SAT-Problem (Erfullbarkeitsproblem)

• Teilklassen des Erfullbarkeitsproblems


Theorem


• Erfullbarkeit fur Formeln in 3-KNF (3-SAT): NP-vollstandig

• Erfullbarkeit fur Formeln in 2-KNF: polynomiell entscheidbar

(nachste Vorlesung)

• Erfullbarkeit fur Formeln in DNF: polynomiell entscheidbar

F =∨n

i=1(∧m

j=1 Lij ) Formel in DNF unerfullbar gdw. fur alle

i , (∧m

j=1 Lij ) enthalt zwei komplementare Literale.

198


Definition:


Theorem


• Erfullbarkeit fur Formeln in 3-KNF: NP-vollstandig (Beweisidee)

• Erfullbarkeit fur Formeln in 2-KNF: polynomiell entscheidbar

• Erfullbarkeit fur Formeln in DNF: polynomiell entscheidbar

199

Horn-Formeln

Defintion:

Horn-Formel: Formel in KNF, in der jede Klausel hochstens ein positives

Literal enthalt

Notation: als Implikation

¬P1 ∨ · · · ∨ ¬Pn ∨ P P1 ∧ · · · ∧ Pn → P

¬P1 ∨ · · · ∨ ¬Pn PA ∧ · · · ∧ Pn →

P → P

P1 ∧ · · · ∧ Pn : Rumpf

P: Kopf → P: Fakt

200

Horn Formel: Beispiele

Klausel Literalmengen Implikationen

¬P {¬P} P →

Q ∨ ¬R ∨ ¬S {Q,¬R,¬S} R, S → Q

¬Q ∨ ¬S {¬Q,¬S} Q,S →

R {R} → R

¬Q ∨ P {¬Q,P} Q → P

201

Erfullbarkeitsproblem fur Horn-Formeln

Theorem

Die Erfullbarkeit von Horn-Formeln ist in quadratischer Zeit entscheidbar.

Lemma. Sei F Hornformel die keine Fakten enthalt. Dann ist F erfullbar.

Beweis: Sei A : Π → {0, 1} mit A(P) = 0 fur alle P ∈ Π. Dann A(F ) = 1.

202


Theorem


Beweis: (Idee)

Ziel: A : Π → {0, 1} mit A(F ) = 1.

Falls keine Fakten in F : F erfullbar.

Sonst: Fur alle Fakten → P in F : A(P) := 1;

Wiederhole das Verfahren fur F ′, entstanden aus F durch Ersetzung von P

mit ⊤.

203

Erfullbarkeitstest fur Horn-Formeln

Eingabe: F = D1 ∧ · · · ∧ Dn eine Hornformel

(die Klausel Di enthalt hochstens ein positives Literal)

Ein Atom in F zu markieren, bedeutet, es an allen Stellen seines Auftretens

in F zu markieren

204

Erfullbarkeitstest fur Horn-Formeln

0: IF keine Fakten (Klausel “→ A”) vorhanden

THEN Ausgabe: erfullbar

ELSE markiere alle Fakten in F (Atome A mit → A in F )

1: IF keine Klausel A1 ∧ · · · ∧ An → B in F , so dass

alle Atome in A1, . . . ,An markiert aber B nicht

THEN Ausgabe: erfullbar

ELSE wahle die erste solche Klausel

IF B leer

THEN Ausgabe: unerfullbar

ELSE markiere uberall B in F

GOTO 1

205

Beispiel 1

(¬P) ∧ (Q) ∧ (¬P ∨ R) ∧ (¬Q ∨ S) ∧ (T ∨ ¬W ) ∧ (¬S ∨ U)∧

(¬U ∨ ¬T ∨ P ∨ ¬Z) ∧ (¬Q ∨ ¬S ∨ ¬U ∨W )

Konjunktion von Implikationen:

(P → ⊥) ∧(⊤ → Q) ∧(P → R) ∧(Q → S) ∧(W → T ) ∧(S → U) ∧

((U ∧ T ∧ Z) → P) ∧((Q ∧ S ∧ U) → W )

P →→ Q

P → R

Q → S

W → T

S → U

U,T , Z → P

Q, S,U → W

206

Beispiel 1

(¬P) ∧ (Q) ∧ (¬P ∨ R) ∧ (¬Q ∨ S) ∧ (T ∨ ¬W ) ∧ (¬S ∨ U)∧

(¬U ∨ ¬T ∨ P ∨ ¬Z) ∧ (¬Q ∨ ¬S ∨ ¬U ∨W ) Erfullbar

P →→ Q

P → R

Q → S

W → T

S → U

U,T , Z → P

Q, S,U → W

Markierte Atome und Erklarung:

{Q} initialer Fakt wegen ⊤ → Q

{Q, S} wegen Q → S

{Q, S,U} wegen S → U

{Q, S,U,W} wegen Q, S,U → W

{Q, S,U,W ,T} wegen W → T

Keine weiteren Schritte moglich, da es

keine Implikation gibt,deren linke Seite

vollstandig markiert ist und die rechte Seite nicht

Modell: A(Q) = A(S) = A(U) = A(W ) = A(T ) = 1, A(P) = A(R) = A(Z) = 0

Markierte Atome: wahr; nicht markierte Atome: falsch.

207

Beispiel 2

(¬P) ∧ (¬P ∨ R) ∧ (¬Q ∨ S) ∧ (T ∨ ¬W ) ∧ (¬S ∨ U)∧

(¬U ∨ ¬T ∨ P ∨ ¬Z) ∧ (¬Q ∨ ¬S ∨ ¬U ∨W ) Erfullbar

P →P → R

Q → S

W → T

S → U

U,T , Z → P

Q, S,U → W


Keine Schritte moglich, da es

keine Implikation gibt,deren linke Seite

vollstandig markiert ist und die rechte Seite nicht

Modell: A(P) = A(Q) = A(R) = A(S) = A(T ) = A(U) = A(W ) = A(Z) = 0

208

Beispiel 3

(¬P) ∧ (Q) ∧ (¬P ∨ R) ∧ (¬Q ∨ S) ∧ (T ∨ ¬W ) ∧ (¬S ∨ U)∧

(¬U ∨ ¬T ∨ P ∨ ¬Z) ∧ (¬Q ∨ ¬S ∨ ¬U)

P →→ Q

P → R

Q → S

W → T

S → U

U,T , Z → P

Q, S,U →


{Q} initialer Fakt wegen ⊤ → Q

{Q, S} wegen Q → S

{Q, S,U} wegen S → U

Unerfullbar

Q, S,U markiert, aber Kopf von

Q, S,U → leer

209

Zusammenfassung

• SAT-Problem (SAT, 3-SAT, 2-SAT, DNF-SAT)

• Horn-Formeln

• Erfullbarkeitstest fur Hornformeln

210

2. Aussagenlogik

Teil 5

14.05.2012

211


Theorem


Beweis: (Idee)

Ziel: A : Π → {0, 1} mit A(F ) = 1.

Falls keine Fakten in F : F erfullbar.

Sonst: Fur alle Fakten → P in F : A(P) := 1;

Wiederhole das Verfahren fur F ′, entstanden aus F durch Ersetzung von P

mit ⊤.

Komplexitat: |F | × |F |

212

Unser Ziel



1. Formeln in KNF (Mengen von Klauseln)

Resolution

2. Formelmengen

Semantische Tableaux

213

1. Resolution

214

Motivation

(¬P) ∧ (Q) ∧ (¬P ∨ R) ∧ (¬Q ∨ S) ∧ (T ∨ ¬W ) ∧ (¬S ∨ U)∧

(¬U ∨ ¬T ∨ P ∨ ¬Z) ∧ (¬Q ∨ ¬S ∨ ¬U ∨W )

Implikationen

P →→ Q

P → R

Q → S

W → T

S → U

U,T , Z → P

Q, S,U → W

Klauseln

¬P

Q

¬P ∨ R

S

T

U

¬Z ∨ P

W


{Q} initialer Fakt wegen ⊤ → Q Q 7→ ⊤{Q, S} wegen Q → S S 7→ ⊤{Q, S,U} wegen S → U U 7→ ⊤{Q, S,U,W} wegen Q, S,U → W W 7→ ⊤{Q, S,U,W ,T} wegen W → T T 7→ ⊤

Modell:

A(Q) = A(S) = A(U) = A(W ) = A(T ) = 1

A(P) = A(R) = A(Z) = 0

Markierte Atome: wahr; nicht markierte Atome: falsch.

215

Bemerkung

Horn Klauseln:

P P,P1 . . .Pn → Q

P1 . . .Pn → Q

Klauselschreibweise:

P ¬P ∨ ¬P1 . . .¬Pn ∨ Q

¬P1 ∨ · · · ∨ ¬Pn ∨ Q

Mengenschreibweise:

{P} {¬P,¬P1,¬Pn,Q}

{¬P1, . . . ,¬Pn,Q}

216

Verallgemeinerung?

Syllogismus (in der ersten Vorlesung erwahnt):

P P → C

C

Mengenschreibweise: 1-Resolution (unit resolution)

{P} {¬P} ∪ C

C

{¬P} {P} ∪ C

C

217

Verallgemeinerung?

Nicht geeignet fur Erfullbarkeitsuberprufung beliebiger Klauselmengen:

Die Klauselmenge

M = {{P1,P2}, {P1,¬P2}, {¬P1,P2}, {¬P1,¬P2}}

ist nicht erfullbar, aber mit 1-Resolution ist aus M nichts ableitbar, also

auch nicht ⊥.

Ziel: Kalkul mit der Eigenschaft dass:

(1) falls M unerfullbar ⊥ ist aus M ableitbar

(2) falls ⊥ aus M ableitbar, M unerfullbar.

7→ Das Resolutionkalkul

218

Der aussagenlogische Resolutionkalkul

Wesentliche Eigenschaften

• Widerlegungskalkul: Testet auf Unerfullbarkeit

• Voraussetzung: Alle Formeln in konjunktiver Normalform

• Eine einzige Regel

• Operiert auf Klauseln (in Mengenschreibweise)

219

Resolutionskalkul

Definition: Resolutionsregel (einzige Regel des Kalkuls)

C1 ∪ {P} {¬P} ∪ C2

C1 ∪ C2

wobei

• P eine aussagenlogische Variable

• C1,C2 Klauseln (konnen leer sein)

Definition:

C1 ∪ C2 heißt Resolvente von C1 ∪ {P},C2 ∪ {¬P}

220

Resolution: Beispiel

Gegeben die Klauselmenge:

M = {{P1,P2}, {P1,¬P2}, {¬P1,P2}, {¬P1,¬P2}}

Resolution:{P1,P2} {P1,¬P2}

{P1}

{¬P1,P2} {¬P1,¬P2}

{¬P1}

{P1} {¬P1}

⊥

Insgesamt: M ⊢Res⊥

also: M unerfullbar

221

Resolution: Weiteres Beispiel

Zu zeigen:

(P → Q) → ((Q → R) → (P → R))

ist allgemeingultig

Dazu zeigen wir, dass

¬[(P → Q) → ((Q → R) → (P → R))]

unerfullbar ist.

Klauselnormalform:

{{¬P,Q}, {¬Q,R}, {P}, {¬R}}

222


Klauselnormalform:

M = {{¬P,Q}, {¬Q,R}, {P}, {¬R}}

Ableitung der leeren Klausel aus M:

(1) {¬P,Q} gegeben

(2) {¬Q,R} gegeben

(3) {P} gegeben

(4) {¬R} gegeben

(5) {Q} aus (1) und (3)

(6) {R} aus (2) und (5)

(7) ⊥ aus (4) und (6)

223

Resolution: Bemerkungen

Vorsicht bei Klauseln mit mehreren Resolutionsmoglichkeiten

• Zwei Klauseln konnen mehr als eine Resolvente haben

z.B.: {A,B} und {¬A,¬B}

• {A,B,C} und {¬A,¬B,D} haben NICHT {C ,D} als Resolvente

Heuristik: Immer moglichst kleine Klauseln ableiten

224

Notwendigkeit der Mengenschreibweise

Die Menge

E = {P1 ∨ ¬P2,¬P1 ∨ P2,¬P1 ∨ ¬P2,P1 ∨ P2}

ist unerfullbar.

Es gibt folgende Resolutionsmoglichkeiten (ohne Mengenschreibweise)

P1 ∨ ¬P2 ¬P1 ∨ P2

¬P2 ∨ P2

P1 ∨ ¬P2 ¬P1 ∨ P2

¬P1 ∨ P1

P1 ∨ ¬P2 ¬P1 ∨ ¬P2

¬P2 ∨ ¬P2

P1 ∨ ¬P2 P1 ∨ P2

P1 ∨ P1

¬P1 ∨ P2 ¬P1 ∨ ¬P2

¬P1 ∨ ¬P1

¬P1 ∨ P2 P1 ∨ P2

P2 ∨ P2

¬P1 ∨ ¬P2 P1 ∨ P2

¬P1 ∨ P1

¬P1 ∨ ¬P2 P1 ∨ P2

¬P2 ∨ P2

Auf diese Weise ist ⊥ nicht herleitbar

225

Ohne Mengenschreibweise

Resolutionsregel:

C1 ∨ P ¬P ∨ C2

C1 ∨ C2

Faktorisieren:C ∨ L ∨ L

C ∨ L

226

Resolution mit Faktorisierung

Die Menge

E = {P1 ∨ ¬P2,¬P1 ∨ P2,¬P1 ∨ ¬P2,P1 ∨ P2}

ist unerfullbar.

Es gibt folgende Resolutionsmoglichkeiten (mit Faktorisieren)

P1 ∨ ¬P2 ¬P1 ∨ P2

¬P2 ∨ P2

P1 ∨ ¬P2 ¬P1 ∨ P2

¬P1 ∨ P1

P1 ∨ ¬P2 ¬P1 ∨ ¬P2

¬P2 ∨ ¬P2

P1 ∨ ¬P2 P1 ∨ P2

P1 ∨ P1

¬P1 ∨ P2 ¬P1 ∨ ¬P2

¬P1 ∨ ¬P1

¬P1 ∨ P2 P1 ∨ P2

P2 ∨ P2

¬P1 ∨ ¬P2 P1 ∨ P2

¬P1 ∨ P1

¬P1 ∨ ¬P2 P1 ∨ P2

¬P2 ∨ P2

P1 ∨ P1

P1

¬P1 ∨ ¬P1

¬P1

P2 ∨ P2

P2

¬P2 ∨ ¬P2

¬P2

P1 ¬P1

⊥

227

Resolution: Beispiel

Gegeben die Klauselmenge:

M = {{P1,P2}, {P1,¬P2}, {¬P1,P2}, {¬P1,¬P2}}

Resolution:{P1,P2} {P1,¬P2}

{P1}

{¬P1,P2} {¬P1,¬P2}

{¬P1}

{P1} {¬P1}

⊥

Insgesamt: M ⊢Res⊥

also: M unerfullbar

228

Resolution

Ziele:

• Formalisieren, was M ⊢Res⊥ bedeutet

• Zeigen, dass M ⊢Res⊥ gdw. M unerfullbar.

229

Resolution

Sei F eine Klauselmenge und

Res(F ) = F ∪ {R | R ist eine Resolvente zweier Klauseln aus F}

Res0(F ) = F

Resn+1(F ) = Res(Resn(F ))

Res⋆(F ) =⋃

n∈N Resn(F )

(bezeichnet die Vereinigung der Resolventen aus aller moglichen Resolutionsschritte

auf F )

Notation: Falls C ∈ Res⋆(F ), so schreiben wir F ⊢Res C .

Definition: Beweis fur C (aus F ): C1, . . .Cn, wobei:

Cn = C und fur alle 1 ≤ i ≤ n: (Ci ∈ F oder Ci Resolvente furCj1

Cj2Ci

mit

j1, j2<i).

230


Klauselnormalform:

M = {{¬P,Q}, {¬Q,R}, {P}, {¬R}}

(1) {¬P,Q} gegeben

(2) {¬Q,R} gegeben

(3) {P} gegeben

(4) {¬R} gegeben

(5) {Q} aus (1) und (3)

(6) {R} aus (2) und (5)

Beweis fur {R} aus M

231


Klauselnormalform:

M = {{¬P,Q}, {¬Q,R}, {P}, {¬R}}

(1) {¬P,Q} gegeben

(2) {¬Q,R} gegeben

(3) {P} gegeben

(4) {¬R} gegeben

(5) {Q} aus (1) und (3)

(6) {R} aus (2) und (5)

(7) ⊥ aus (4) und (6)

Beweis fur ⊥ aus M (Widerspruch)

232

Resolution: Korrektheit und Vollstandigkeit

Theorem (Korrektheit)

Fur eine Menge M von Klauseln gilt: Falls M ⊢Res⊥, so M unerfullbar.

Theorem (Vollstandigkeit)

Fur eine Menge M von Klauseln gilt: Falls M unerfullbar, so M ⊢Res⊥.

233

Resolution: Korrektheit



Beweis: Wir werden zeigen, dass falls C ∈ Res∗(M), so M ≡ M ∪ {C}.

(Theorem auf Seite 236). (NB: M ∪ {C} Notation fur M ∧ C .)

Dann, falls M ⊢Res⊥, so ⊥∈ Res∗(M), d.h. M ≡ M ∪ {⊥}.

Aber M ∪ {⊥} ist unerfullbar, deshalb ist auch M unerfullbar.

Erklarung 1: Falls M = {C1, . . . ,Cn} so M ∪ {⊥} ist eine Notation fur

C1 ∧ · · · ∧ Cn ∧ ⊥. Aber C1 ∧ · · · ∧ Cn ∧ ⊥ ≡ ⊥, so ist C1 ∧ · · · ∧ Cn ∧ ⊥unerfullbar (also auch M ∪ {⊥}). Da M ≡ M ∪ {⊥}, ist auch M unerfullbar.

Erklarung 2: Es gibt keine Wertebelegung A die alle Klauseln in M ∪ {⊥} wahr macht

(d.h. so dass: A(D) = 1 fur alle Klauseln D in M und A(⊥) = 1).

234


Lemma: C1 ∨ P,C2 ∨ ¬P |= C1 ∨ C2

Beweis:

Sei A Interpretation mit A(C1 ∨ P) = 1 und A(C2 ∨ ¬P) = 1.

Zu zeigen: A(C1 ∨ C2) = 1.

Fall 1: A(C1) = 1. Dann A(C1 ∨ C2) = 1.

Fall 2: A(C1) = 0. Dann A(P) = 1.

Da A(C2 ∨ ¬P) = 1, so A(C2) = 1, d.h. A(C1 ∨ C2) = 1.

235


Theorem: Falls C ∈ Res⋆(F ), so F ≡ F ∪ {C}.

Beweis: Annahme: C ∈ Resn(F ).

Zu zeigen: F ≡ F ∧ C , i.e.:

Fur alle A : Π → {0, 1} gilt: A(F ) = 1 gdw. (A(F ) = 1 und A(C) = 1).

• Sei A : Π → {0, 1} mit A(F ) = 1.

Induktion: Fur alle m ∈ N gilt: Falls D ∈ Resm(F ), so A(D) = 1.

(folgt aus: C1 ∨ P,C2 ∨ ¬P |= C1 ∨ C2)

Dann A(C) = 1, so (A(F ) = 1 und A(C) = 1), d.h. A(F ∧ C) = 1.

• Sei A : Π → {0, 1} mit A(F ∧ C) = 1.

Dann A(F ) = 1 und A(C) = 1, so A(F ) = 1.

236

Resolution: Vollstandigkeit

Theorem.

Fur jede endliche Menge M von Klauseln gilt:

falls M unerfullbar, so M ⊢Res⊥.

Beweis: Induktion:

p(n): Sei M Menge von Klauseln mit n Aussagenvariablen.

Falls M unerfullbar, so M ⊢Res⊥

237

2. Aussagenlogik

Teil 6

28.05.2012

238

Resolution

Ziele:

• Formalisieren, was M ⊢Res C bedeutet

• Zeigen, dass M ⊢Res⊥ gdw. M unerfullbar.

Korrektheit: Falls M ⊢Res⊥, so M unerfullbar.

Vollstandigkeit: Falls M unerfullbar, so M ⊢Res⊥

• Zeigen, dass das Verfahren terminiert.

239

Resolution: Korrektheit und Vollstandigkeit



letzte Vorlesung


Fur eine Menge M von Klauseln gilt: Falls M unerfullbar, so M ⊢Res⊥.

heute

240


Theorem.



Beweis: Induktion:

p(n): Sei M Menge von Klauseln mit n Aussagenvariablen.

Falls M unerfullbar, so M ⊢Res⊥

Induktionsbasis: n = 0.

Dann M = {⊥}, d.h. M ⊢Res⊥

241


M0 sei aus M entstanden durch Ersetzung von Pn+1 durch ⊥:

- Pn+1 wird aus allen Klauseln geloscht,

- Klauseln, die ¬Pn+1 enthalten werden ebenfalls geloscht

M1 sei aus M entstanden durch Ersetzung von Pn+1 durch ⊤:

- ¬Pn+1 wird aus allen Klauseln geloscht,

- Klauseln, die Pn+1 enthalten werden ebenfalls geloscht

Fakten:

• M0,M1 enthalten nur Aussagenvariablen {P1, . . . ,Pn}• M0,M1 unerfullbar

Induktionsvoraussetzung:

M0 ⊢Res⊥, i.e. es gibt C1,C2, . . . ,Cm Beweis (aus M0) fur ⊥Pn+1 zuruck: C ′

1 ,C′

2 , . . . ,C′

m Beweis (aus M) fur ⊥ oder Pn+1

M1 ⊢Res⊥, i.e. es gibt D1,D2, . . . ,Dk Beweis (aus M1) fur ⊥¬Pn+1 zuruck: D′

1 ,D′

2 , . . . ,D′

k Beweis (aus M) fur ⊥ oder ¬Pn+1

⇒ M ⊢Res⊥

242


Theorem.



Es gilt auch:

Theorem.

Fur jede Menge M von Klauseln gilt:


243

Terminierung

Theorem.

Aussagenlogische Resolution (fur Klauselmengen in Mengennotation)

terminiert, fur jede endliche Menge von Klauseln.

Beweis: Es gibt nicht mehr als 22n Klauseln (in Mengennotation) mit n

Aussagenvariablen.

7→ nicht mehr als (22n)2 mogliche Anwendungen der Resolutionsregel.

244

2-SAT

Theorem

Erfullbarkeit fur Formeln in 2-KNF (2SAT) ist polynomiell entscheidbar

Beweis (Krom, 1967)

Fall 1: Fur jede Aussagenvariable P, entweder enthalten alle Klauseln P oder ¬P:

erfullbar.

Fall 2: Es gibt Klauseln C1 = L1 ∨ P, C2 = L2 ∨ ¬P

Resolutionschritt; Resolvente L1 ∨ L2 (Mengennotation)

Fakt: Resolventen sind immer auch in 2-KNF.

Wenn F n Aussagenvariablen enthalt, gibt es 2n mogliche Literale, und ≤ 4n2

nicht-leere verschiedene 2-KNF Klauseln.

F ist erfullbar gdw. ⊥6∈ Res∗(F )

Wenn wir Res∗(F ) berechnen: nicht mehr als (4n2)2 Resolutionsschritte

notwendig.

7→ Erfullbarkeit von F ist polynomiell entscheidbar.

245

1-Resolution

Die 1-Resolution (unit resolution) benutzt dieselbe Notation wie im

Resolutionskalkul. Die 1-Resolutionsregel ist ein Spezialfall der allgemeinen

Resolutionsregel:

{P} {¬P} ∪ C

C

{¬P} {P} ∪ C

C

Der 1-Resolutionskalkul ist nicht vollstandig.

Die Klauselmenge

M = {{P1,P2}, {P1,¬P2}, {¬P1,P2}, {¬P1,¬P2}}

ist nicht erfullbar, aber mit 1-Resolution ist aus M nichts ableitbar, also

auch nicht ⊥.

246

Unser Ziel




Resolution bis jetzt

2. Formelmengen


247

Unser Ziel




Resolution

2. Formelmengen


248

Der aussagenlogische Tableaukalkul

Wesentliche Eigenschaften

• Widerlegungskalkul: Testet auf Unerfullbarkeit

• Beweis durch Fallunterscheidung

• Top-down-Analyse der gegebenen Formeln

249

Der aussagenlogische Tableaukalkul

Vorteile

• Intuitiver als Resolution

• Formeln mussen nicht in Normalform sein

• Falls Formelmenge erfullbar ist (Test schlagt fehl), wird ein

Gegenbeispiel (eine erfullende Interpretation) konstruiert

Nachteile

• Mehr als eine Regel

250

Formeltypen

Konjunktive Formeln: Typ α

• ¬¬F

• F ∧ G

• ¬(F ∨ G)

• ¬(F → G)

Disjunktive Formeln: Typ β

• ¬(F ∧ G)

• F ∨ G

• F → G

251

Formeltypen

Konjunktive Formeln: Typ α

• ¬¬F

• F ∧ G

• ¬(F ∨ G)

• ¬(F → G)

Zuordnungsregeln Formeln / Unterformeln

α α1 α2

F ∧ G F G

¬(F ∨ G) ¬F ¬G

¬(F → G) F ¬G

¬¬F F

252

Formeltypen

Disjunktive Formeln: Typ β

• ¬(F ∧ G)

• F ∨ G

• F → G

Zuordnungsregeln Formeln / Unterformeln

β β1 β2

¬(F ∧ G) ¬F ¬G

F ∨ G F G

F → G ¬F G

253

Regeln des (aussagenlogischen) Tableaukalkuls

α

α1

α2

Konjunktiv

p ∧ q

|p

|q

β

β1 | β2

Disjunktiv

p ∨ q

/ \

p q

φ

¬φ

⊥

Widerspruch

φ

¬φ

|⊥

254

Instanzen der α und β-Regel

Instanzen der α-Regel

P ∧ Q

P

Q

¬(P ∨ Q)

¬P

¬Q

¬(P → Q)

P

¬Q

¬¬P

P

Instanzen der β-Regel

P ∨ Q

P | Q

¬(P ∧ Q)

¬P | ¬Q

P → Q

¬P | Q

255

Ein Tableau fur {P ∧ ¬(Q ∨ ¬R), ¬Q ∨ ¬R}

(3) ¬Q

(5) P

(6) ¬(Q ∨ ¬R)

(7) ¬Q

(8) ¬¬R

(9) R

(4) ¬R

(10) P

(11) ¬(Q ∨ ¬R)

��

XXXXX

1.(1) P ∧ ¬(Q ∨ ¬R)

(2) ¬Q ∨ ¬R Dieses Tableau ist nicht

“maximal”, aber der erste

“Ast” ist.

Dieser Ast ist nicht

“geschlossen” (enthalt

keinen Widerspruch),

also ist die Menge {1, 2}

erfullbar.

(Diese Begriffe werden auf

den nachsten Seiten

erklart.)

256

Determinismus von Kalkul und Regeln

Determinismus

• Die Regeln sind alle deterministisch

• Der Kalkul aber nicht:

Auswahl der nachsten Formel, auf die eine Regel angewendet wird

Heuristik

• Nicht-verzweigende Regeln zuerst: α vor β

Nota bene:

Dieselbe Formel kann mehrfach (auf verschiedenen Asten) verwendet

werden

257

Formale Definition des Kalkuls

Definition

Tableau: Binarer Baum, dessen Knoten mit Formeln markiert sind

Definition

Tableauast: Maximaler Pfad in einem Tableau (von Wurzel zu Blatt)

258


Sei M eine Formelmenge

Initialisierung

Das Tableau, das nur aus dem Knoten 1 besteht, ist ein Tableau fur M

Erweiterung

• T ein Tableau fur M

• B ein Ast von T

• F eine Formel auf B oder in M, die kein Literal ist

T ′ entstehe durch Erweiterung von B gemaß der auf F anwendbaren Regel

(α oder β)

Dann ist T ′ ein Tableau fur M.

259


Nota bene:

Alle Aste in einem Tableau fur M enthalten implizit alle Formeln in M

Definition.

Ast B eines Tableaus fur M ist geschlossen, wenn es eine Formel F existiert,

so dass B die Formeln F und ¬F enthalt.

Definition.

Ein Tableau ist geschlossen, wenn jeder seiner Aste geschlossen ist.

Definition.

Ein Tableau fur M, das geschlossen ist, ist ein Tableaubeweis fur (die

Unerfullbarkeit von) M

260

Beispiel

Zu zeigen:

(P → (Q → R)) → ((P ∨ S) → ((Q → R) ∨ S)) allgemeingultig

Wir zeigen, dass

¬[(P → (Q → R)) → ((P ∨ S) → ((Q → R) ∨ S))]

unerfullbar ist.

261

Beispiel

(10) P β [41] (11) S β [42]

��

XXXXX

(8) ¬P β [21] (9) Q → R β [22]

hhhhhhhhh

(1) ¬[(P → (Q → R)) → ((P ∨ S) → ((Q → R) ∨ S))]

(2) (P → (Q → R)) α [11]

(3) ¬((P ∨ S) → ((Q → R) ∨ S)) α [12]

(4) P ∨ S α [31]

(5) ¬((Q → R) ∨ S)) α [32]

(6) ¬(Q → R) α [51]

(7) ¬S α [52]

geschlossenes Tableau.

262

2. Aussagenlogik

Teil 7

3.06.2013

263

Klauseltableau

M Menge von Klauseln

Anderungen

• Keine α-Regel

• Erweiterungsregel kann Verzweigungsgrad > 2 haben

• Alle Knoten im Tableau enthalten Literale

264

Klauseltableau: Beispiel

M = { {P,Q,R}, {¬R}, {¬P,Q}, {P,¬Q}, {¬P,¬Q} }

1.

gggggg

gggggg

VVVVVV

VVVVV

¬P

uuuu KK

KKQ

uuuu LL

LL

P ¬Q

ssss PP

PPP

pppp II

I ¬Q

⊥ P Q R ¬P ¬Q ⊥

⊥ ⊥ ⊥ ⊥ ⊥

265

Korrektheit und Vollstandigkeit des

Tableaukalkuls

Theorem.

Eine Formelmenge M ist unerfullbar

genau dann, wenn

es einen Tableaubeweis fur (die Unerfullbarkeit von) M gibt

Korrektheit: “⇐”

Falls es einen Tableaubeweis fur (die Unerfullbarkeit von) M gibt

(d.h. ein Tableau fur M, das geschlossen ist)

so ist M unerfullbar.

... alternativ:

Falls M erfullbar ist, hat M kein geschlossenes Tableau.

266

Korrektheit und Vollstandigkeit des

Tableaukalkuls

Theorem.

Eine Formelmenge M ist unerfullbar

genau dann, wenn

es einen Tableaubeweis fur (die Unerfullbarkeit von) M gibt

Vollstandigkeit: “⇒”

Falls M unerfullbar ist,

gibt es einen Tableaubeweis fur (die Unerfullbarkeit von) M

(d.h. ein Tableau fur M, das geschlossen ist).

267

Kern des Korrektheitsbeweises



(d.h. ein Tableau fur M, das geschlossen ist) so ist M unerfullbar.

... alternativ: Falls M erfullbar ist, hat M kein geschlossenes Tableau.

Definition.

Ein Tableauast ist erfullbar, wenn die Menge seiner Formeln erfullbar ist

Ein Tableau ist erfullbar, wenn es (mindestens) einen erfullbaren Ast hat

Lemma 1. Jedes Tableau fur eine erfullbare Formelmenge M ist erfullbar

Lemma 2. Ein geschlossenes Tableau ist nicht erfullbar

... Also: Kein geschlossenes Tableau fur erfullbare Formelmenge

268

Lemma 1: Beweis

Definition.

Tableauast ist erfullbar, wenn die Menge seiner Formeln erfullbar ist.

Tableau ist erfullbar, wenn es (mindestens) einen erfullbaren Ast hat


Beweis: Induktion p(n): Falls M erfullbar und das Tableau T in n Schritten

aus M gebildet wurde, ist T erfullbar

Induktionsbasis: T wurde in einem Schritt gebildet.

Initialisierung

Das Tableau, das nur aus dem Knoten 1 besteht, ist ein Tableau fur M

da M erfullbar ist, ist ein solches Tableau erfullbar

269

Lemma 1: Beweis

Definition.Tableauast ist erfullbar, wenn die Menge seiner Formeln erfullbar ist.Tableau ist erfullbar, wenn es (mindestens) einen erfullbaren Ast hat




Induktionsschritt: Annahme p(n) gilt. Zu zeigen: p(n + 1).

Sei T ein in n + 1 Schritten gebildetes Tableau fur M.

Dann gibt es ein Tableau T ′ fur M (in n Schritten gebildet), ein Ast B von T ′ und

eine Formel F auf B, die kein Literal ist, so dass T durch die Erweiterung von B

gemaß der auf F anwendbaren Regel (α oder β) entstanden ist.

Induktionsvoraussetzung: T ′ erfullbar, d.h. hat (mindestens) einen erfullbaren Ast B′.

Fall 1: B′ 6= B. Dann ist B′ auch Ast in T , d.h. T erfullbar.

270

Lemma 1: Beweis








eine Formel F auf B oder in M, die kein Literal ist, so dass T durch die Erweiterung

von B gemaß der auf F anwendbaren Regel (α oder β) entstanden ist.


Fall 2: B′ = B d.h. B erfullbar. Sei A Modell fur die Formeln NB auf B.

Fall 2a: α-Regel angewandt F ≡ F1 ∧ F2. Dann ist A Modell fur

NB ∪ {F1, F2}, d.h.: die Erweiterung von B mit dieser α-Regel ist erfullbar,

so T erfullbar.

271

Lemma 1: Beweis








eine Formel F auf B oder in M, die kein Literal ist, so dass T durch die Erweiterung

von B gemaß der auf F anwendbaren Regel (α oder β) entstanden ist.


Fall 2: B′ = B d.h. B erfullbar. Sei A Modell fur die Formeln NB auf B.

Fall 2b: β-Regel angewandt F≡F1∨F2. Dann 1=A(F )=A(F1)∨A(F2), so

A(F1)=1 oder A(F2)=1. Dann A|=NB∪{Fi}, i=1 oder 2, d.h. A Modell

fur alle Formeln auf der Erweiterung von B mit F1 oder F2, so T erfullbar.

272

Lemma 2: Beweis

Definition.

Tableauast ist erfullbar, wenn die Menge seiner Formeln erfullbar ist

Tableau ist erfullbar, wenn es (mindestens) einen erfullbaren Ast hat


Lemma 2. Ein geschlossenes Tableau ist nicht erfullbar

Beweis: Kontraposition

Annahme: T erfullbar. Dann hat T einen erfullbaren Ast B.

Falls die Menge der Formeln auf B (und M) erfullbar ist, kann B nicht Formeln F und

¬F enthalten, d.h. B kann nicht geschlossen sein.

273

Korrektheit und Vollstandigkeit



(d.h. ein Tableau fur M, das geschlossen ist) so ist M unerfullbar.


Falls M unerfullbar, so gibt es einen Tableaubeweis fur die Unerfullbarkeit

von M (d.h. einen Tableau fur M, das geschlossen ist).

... alternativ:

“falls es keinen Tableaubeweis fur die Unerfullbarkeit von M gibt (d.h.

“maximales Tableau’” fur M nicht geschlossen) so ist M erfullbar”

274

Kern des Vollstandigkeitsbeweises

Definition.

Ein Tableau heißt voll expandiert, wenn

• jede Regel

• auf jede passende Formel

• auf jedem offenen Ast

angewendet worden ist.

Lemma 3.

Sei B offener Ast in voll expandiertem Tableau.

Dann ist die Menge der Formeln in B erfullbar.

... Also: Voll expandiertes Tableau fur unerfullbares M ist geschlossen

275

Lemma 3: Beweis

Lemma 3.

Sei B offener Ast in voll expandiertem Tableau.

Dann ist die Menge der Formeln in B erfullbar.

Beweis: (fur klausale Tableaux)

Sei N die Menge der Formeln auf B. Da B offen ist, ist ⊥ nicht in N.

Seien C ∨ A, D ∨ ¬A zwei Klauseln in N die komplementare Literale enthalten. Einer

von C ,D ist nicht leer (sonst ware B geschlossen).

Annahme: C nicht leer. Da B voll expandiert ist, wurde die β-Regel fur C ∨ A

angewandt (auch fur D ∨ ¬A falls D nicht leer).

Fall 1: A,¬A ∈ B: unmoglich, da B offen ist.

Fall 2: A, L ∈ B mit L Literal in D. N erfullbar gdw. N\{D ∨ ¬A} erfullbar.

Fall 3: L,¬A ∈ B, mit L Literal in C . N erfullbar gdw. N\{C ∨ A} erfullbar.

Fall 4: L1, L2 ∈ B, mit L1 Literal in C , L2 Literal in D.

N erfullbar gdw. N\{C ∨ A,D ∨ ¬A} erfullbar.

N 7→ N′, N′ Klauselmenge ohne komplementare Literale und ohne ⊥Die Erfullbarkeit von N′ folgt aus der Vollstandigkeit der Resolution.

276

Klauseltableau: Einschrankungen des Suchraums

Regularitat:

Kein Literal darf auf einem Ast mehr als einmal vorkommen

Schwache Konnektionsbedingung (Connection calculus)

Bei Erweiterung von Ast B muss mindestens eines der neuen Literale

komplementar zu Literal in B sein.

Starke Konnektionsbedingung (Modellelimination)

Bei Erweiterung von Ast B muss mindestens eines der neuen Literale

komplementar zum Blatt von B sein – außer beim ersten Schritt.

277

Klauseltableau: Einschrankungen des Suchraums

Theorem (hier ohne Beweis)

Regularitat, starke und schwache Konnektionsbedingung

erhalten Vollstandigkeit.

Jedoch

Bei starker Konnektionsbedingung kann ungunstige Erweiterung in

Sackgasse fuhren.

(bei schwacher Konnektionsbedinung nicht)

Beispiel: M = {{P}, {¬Q}, {¬P,Q}, {¬P,R}}

Zuerst {¬P,Q}: OK

Zuerst {¬P,R}: Sackgasse

278

Klauseltableau: Weiteres Beispiel

Signatur: F : Flugreise V : Vollpension M: Meer P: Pool

Falls sie nicht mit dem Flugzeug fliegen, besteht der Vater auf Vollpension am Meer.

¬F → (V ∧ M)

Die Mutter mochte mindestens einen ihrer drei Wunsche erfullt sehen: ans Meer

fliegen, oder am Meer ohne Pool, oder Vollpension und Pool.

(M ∧ F ) ∨ (M ∧ ¬P) ∨ (V ∧ P)

Gibt es keinen Pool, so besteht Tochter Lisa auf einer Flugreise und Urlaub am Meer

und darauf, dass keine Vollpension gebucht wird.

¬P → (F ∧ M ∧ ¬V )

Auch dem Baby soll einer seiner Wunsche erfullt werden: erstens einen Pool und nicht

fliegen oder zweitens Vollpension, dann aber ohne Pool.

(P ∧ ¬F ) ∨ (V ∧ ¬P)

279


Behauptung

Dann mussen sie ans Meer mit Vollpension, mit Pool und ohne Flug.

M ∧ V ∧ P ∧ ¬F

Zu zeigen:

{¬F → (V ∧M), (M ∧ F ) ∨ (M ∧ ¬P) ∨ (V ∧ P),

¬P → (F ∧M ∧ ¬V ), (P ∧ ¬F ) ∨ (V ∧ ¬P)} |= M ∧ V ∧ P ∧ ¬F

Wir zeigen, dass die folgende Konjunktion unerfullbar ist:

(¬F → (V ∧M), (M ∧ F ))∧

((M ∧ F ) ∨ (M ∧ ¬P) ∨ (V ∧ P))∧

(¬P → (F ∧M ∧ ¬V ))∧

((P ∧ ¬F ) ∨ (V ∧ ¬P))∧

¬M ∨ ¬V ∨ ¬P ∨ F (Negation der Behauptung)

280


¬F → (V ∧ M) (1) F ∨ V

(2) F ∨ M

(M ∧ F ) ∨ (M ∧ ¬P) ∨ (V ∧ P) (3) M ∨ V

(4) M ∨ P

(5) M ∨ ¬P ∨ V

(6) F ∨ M ∨ V

(7) F ∨ M ∨ P

(8) F ∨ ¬P ∨ V

¬P → (F ∧ M ∧ ¬V ) (9) P ∨ F

(10) P ∨ M

(11) P ∨ ¬V

(P ∧ ¬F ) ∨ (V ∧ ¬P) (12) P ∨ V

(13) ¬F ∨ V

(14) ¬F ∨ ¬P

Negation der Behauptung (15) ¬M ∨ ¬V ∨ ¬P ∨ F

281


Beobachtung

Konstruktion des Konnektionstableaus

• bei Beginn mit Klausel (1)

• mit Regularitat

• mit starker Konnektionsbedingung

Dann:

Nahezu deterministische Beweiskonstruktion

282


(1) F ∨ V

(2) F ∨ M

(3) M ∨ V

(4) M ∨ P

(5) M ∨ ¬P ∨ V

(6) F ∨ M ∨ V

(7) F ∨ M ∨ P

(8) F ∨ ¬P ∨ V

(9) P ∨ F

(10) P ∨ M

(11) P ∨ ¬V

(12) P ∨ V

(13) ¬F ∨ V

(14) ¬F ∨ ¬P

(15) ¬M ∨ ¬V ∨ ¬P ∨ F

F

FP

V P F

1

F V

P VV

P

M V P F

F M

283

2. Aussagenlogik

Teil 8

4.06.2013

284

Terminierung

Definition. Ein Tableau ist strikt, falls fur jede Formel F die entsprechende

Erweiterungsregel hochstens einmal auf jeden Ast, der die Formel enthalt,

angewandt wurde.

Theorem.

Sei T ein striktes aussagenlogisches Tableau. Dann ist T endlich.

Beweis: Neue Formeln mit denen ein Tableau erweitert wird sind ⊥, (⊤) oder

Teilformeln der Formel, auf der die Erweiterungsregel angewandt wird. Da T strikt

ist, wird fur jede Formel F die entsprechende Erweiterungsregel hochstens einmal auf

jeden Ast, der die Formel enthalt, angewandt.

Dann sind alle Aste in T endlich, und so ist auch T endlich (Konig’s Lemma).

285

Zusammenfassung: Tableaukalkul

Beweis durch Widerspruch und Fallunterscheidung

• Tableauregeln (mit uniformer Notation)

• Formale Definition des Kalkuls

• Korrektheit und Vollstandigkeit

• Klauseltableau

• Regularitat

• Schwache und starke Konnektionsbedingung

• Strikte Tableaux

• Terminierung

286

VioricaSofronie-Stokkermans...

Documents

Transcript of VioricaSofronie-Stokkermans...