VioricaSofronie-Stokkermans...

Logik fur Informatiker

Viorica Sofronie-Stokkermans

e-mail: sofronie@uni-koblenz.de

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

Logik in der Informatik

Was ist Logik?

• Mathematisch?

• Unverstandlich?

hoffentlich nein

• Reine Theorie ohne praktischen Nutzen?

nein: Verifikation von Hardware, Software, Protokollen

Sprachverarbeitung und Wissensreprasentation

Abfragensprachen fur Datenbanken; ...

Formale Logik

• 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

Modellierung

Abstraktion

Modellierung

Adaquatheit des Modells

Wenn formulierbare Aussage wahr im Modell, dann entsprechende Aussage

wahr in Wirklichkeit

Modellierung: Strukturen

Aufzug oben Aufzug oben

Aufzug mitte

Mitte gedruckt

F.nach unten

Mitte gedruckt

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

Aufzug mitteAufzug mitte

Mitte gedruckt

F.nach unten

Mitte gedruckt

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

Aufzug mitteAufzug mitte

Mitte gedruckt

F.nach unten

Mitte gedruckt

F.nach unten

Unten gedruckt

Aussagen beziehen sich auf Strukturen

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

auswertbar

Formale Logik

• Syntax

welche Formeln?

• Semantik

Modelle (Strukturen)

Wann ist eine Formel wahr (in einer Struktur)?

• Deduktionsmechanismus

Ableitung neuer wahrer Formeln

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

∧ ∨ → ¬

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

Aussagenlogik: Semantik

wahr in: Aufzug oben oben

Mitte gedruckt

F.nach unten

Aussagenlogik: Semantik

falsch in:

Aufzug mitte

F.nach unten

Unten gedruckt

Aussagenlogik: Deduktionsmechanismus

Syllogismen:

P P → Q

AufzugUnten AufzugUnten → ¬AufzugOben

¬AufzugOben

Aussagenlogik: Deduktionsmechanismus

Deduktionsmechanismus im allgemeinen

Kalkul

In dieser Vorlesung:

• Wahrheitstafeln

• Logische Umformung

• Resolutionskalkul

• Tableaukalkul

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.

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, ...

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:

(fur alle);

(es gibt)

Formeln mit Quantoren:

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

x ungerade(x)

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)

Beispiel 2:

Formel:

Mann(Vater(Jan))

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

Mann(Mutter(Anna))

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

Quantoren

: fur alle

: es gibt

Formeln mit Quantoren:

x Mann(Vater(x))

x Mann(Mutter(x))

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

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

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

Pradikatenlogik: Deduktionsmechanismus

Syllogismen:

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

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

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

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

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

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

Syllogismen:

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

Beispiel:

studiertIn(Jan, koblenz)

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

schlau(Jan)

In dieser Vorlesung:

• Resolutionskalkul

• Tableaukalkul

Das Prinzip

z.B. naturliche Sprache

Problem Losung

LosungFormeln

prazise Beschreibung

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.

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.

Das folgende Schlusselaustauschverfahren wurde 1993 von den beiden Kryp-

tographen Neuman und Stubblebine vorgeschlagen:

Schritt 1:

Alice schickt (offen) Identifikation und Zufallszahl an Bob.

Schritt 2:

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

Schritt 3:

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

einmal fur Alice und einmal fur Bob verschlusselt.

Schritt 4:

Alice leitet den neuen gemeinsamen Schlussel weiter an Bob.

Schritt 5:

Alice und Bob konnen nun mit dem gemeinsamen Schlussel kommunizieren.

Ist das Verfahren sicher?

Wir ubersetzen das Problem in Formeln und lassen sie von einem

Theorembeweiser untersuchen.

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.

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

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.

Das ganze Bild

Probleme (Beschreibung in natürlicher Sprache)

Formalisierung

Gültige Formel Beweisbare Formel

Kalkül

Logische Sprache: Syntax

Aussagenlogik /

Formel

Modelle: Semantik

Vollständigkeit

Korrektheit

Prädikatenlogik

Das ganze Bild

Modellierung

Formalisierung

Kalkül

Aussagenlogik / Prädikatenlogik

Formel

Modelle: Semantik

Vollständigkeit

Korrektheit

Das ganze Bild

(automatische)

Deduktion

Formalisierung

Kalkül

Aussagenlogik /

Formel

Modelle: Semantik

Vollständigkeit

Korrektheit

Prädikatenlogik

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

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

1. Grundlegende Beweisstrategien

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

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,

n2= (2k + 1)

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

+ 2k) + 1.

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

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.

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

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

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

- 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.

- 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.

Aussagen mit Quantoren

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:

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

︸︷︷︸

→√n ist gerade

︸︷︷︸

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

x ∈ U A(x)

Sei a ein geeignetes Element aus U.

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

x ∈ U : A(x).

Behauptung:

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

x ∈ N : A(x)

x ∈ U A(x)

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

x ∈ U : A(x).E

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

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

Damit folgt

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

Beweise mittels Vollstandiger Induktion

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

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.

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

auch deren Nachfolger S(n) enthalt, umfasst alle

naturlichen Zahlen.

X Menge: Falls 0 ∈ X , und

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

n ∈ N : n ∈ X

Induktionssatz

Gelten die beiden Aussagen:

- p(0) und Induktionsbasis

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

dann gilt auch

n ∈ N : p(n).

Struktur eines Induktionsbeweises

(1) Induktionsbasis: Beweise p(0)

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

fur ein beliebiges n ∈ N

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

Beispiel

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

Fur alle n ∈ N,

n−1∑

(2i + 1) = n2.

p(n) :

n−1∑

(2i + 1) = n2

(1) Induktionsbasis: Beweise p(0) OK

(2) Induktionsvoraussetzung: Fur ein beliebig gewahltes

n ∈ N gilt p(n):

n−1∑

(2i + 1) = n2

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

p(n + 1) :

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

Beweis:

(2i + 1) = (

n−1∑

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

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

Wohlfundierte (Noethersche) Induktion

Verallgemeinerte vollstandige Induktion

p(0) und

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

dann gilt die Aussage

n ∈ N : p(n).

Aquivalent

p(0) und

n ∈ N : (

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

n ∈ N : p(n).

Verallgemeinerte vollstandige Induktion

p(0) und

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

n ∈ N : p(n).

Aquivalent

Gilt die Aussage:

n ∈ N : (

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

n ∈ N : p(n).

Vollstandige Induktion

Zu zeigen:

n ≥ n0 : P(n)

Sei n ∈ N, n ≥ n0.

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

Induktionsschluss: Folgere p(n) aus der Induktionsvoraussetzung.

Theorem:

n ∈ N : (

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

dann gilt

n ∈ N : p(n) Q

Beweis: Zu zeigen: P → Q

Kontrapositionsbeweis: Wir zeigen, dass ¬Q → ¬P

Annahme: ¬Q := ¬(

n ∈ N : p(n)) ≡

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.

m(m ∈ Y ∧ (

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

Theorem:

n ∈ N : (

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

dann gilt

n ∈ N : p(n) Q

Beweis: Zu zeigen: P → Q

Kontrapositionsbeweis: Wir zeigen, dass ¬Q → ¬P

Annahme: ¬Q := ¬(

n ∈ N : p(n)) ≡

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.

m(m ∈ Y ∧ (

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

Theorem:

n ∈ N : (

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

dann gilt

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

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.

Fehlerquellen

Haufige Fehler bei Induktionsbeweisen

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

• Induktionsanfang inkorrekt

• Bei Induktionsschritt die Grenzfalle nicht bedacht

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

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

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.

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.

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.

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.

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

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

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

(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

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.

Zu zeigen:

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.

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.

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 ∈ Σ.

Beispiel

Zu zeigen:

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

Sei w1 ∈ Σ∗, beliebig.

Zu zeigen:

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

Beispiel

Zu zeigen:

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

Sei w1 ∈ Σ∗, beliebig.

Zu zeigen:

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)

Beispiel 2

Bin : Menge allen (vollstandigen) binaren Baume

B B1 2

Tree(B , B )1 2

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.

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

B ∈ Bin,P(B) gilt.

Zusammenfassung

• Grundlegende Beweisstrategien

• Induktion uber die naturlichen Zahlen

• Fehlerquellen

• Strukturelle Induktion

2. Aussagenlogik

Teil 1

23.04.2013

Beispiel: Das 8-Damen Problem

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

gegenseitig nicht bedrohen.

Beschreibung des Problems

Fur jedes Feld des Schachbretts eine aussagenlogische Variable

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

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

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

︸︷︷︸

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

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

Formale Logik

• Syntax

welche Formeln?

• Semantik

Modelle (Strukturen)

Wann ist eine Formel wahr (in einer Struktur)?

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

Vokabular der Aussagenlogik

Abzahlbare Menge von Symbolen, etwa

Π = {P0, . . . ,Pn}

Π = {P0,P1, . . . }

Bezeichnungen fur Symbole in Π

• atomare Aussagen

• Atome

• Aussagenvariablen

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Π.

Aussagenformeln

ForΠ Menge der Formeln uber Π:

F ,G ,H ::= ⊥ (Falsum)

| ⊤ (Verum)

| P, P ∈ Π (atomare Formel)

| ¬F (Negation)

| (F ∧ G) (Konjunktion)

| (F ∨ G) (Disjunktion)

| (F → G) (Implikation)

| (F ↔ G) (Aquivalenz)

Konventionen zur Notation

• Klammereinsparungen werden nach folgenden Regeln vorgenommen:

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

– ∨ und ∧ sind assoziativ und kommutativ,

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.

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

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

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

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

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.

Π 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:

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

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)

A∗(¬F ) =

0 falls A∗(F ) = 1

1 falls A∗(F ) = 0

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

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

Wahrheitstafel fur die logischen Operatoren

∧ 0 1

∨ 0 1

→ 0 1

↔ 0 1

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∗.

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

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

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

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

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

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.

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

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

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 .

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

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

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

2. Aussagenlogik

Teil 2

30.04.2012

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

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.

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 .

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)

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)

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

(F ∧ G) ≡ F , falls G Tautologie

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

(F ∧ G) ≡ ⊥, falls G unerfullbar

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

Wichtige Aquivalenzen mit ⊤/⊥

(A ∧ ¬A) ≡ ⊥

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

(A ∧ ⊤) ≡ A

(A ∧ ⊥) ≡ ⊥

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)

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

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

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′.

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′

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′.

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.

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.

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

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

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.

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.

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

Allgemeingultigkeit/Folgerung:

Zusammenfassung

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

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

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 .

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.

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.

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.

Zusammenfassung

• Erfullbarkeit, Allgemeingultigkeit

• Erster Kalkul: Wahrheitstafelmethode

• Folgerung, Aquivalenz

• Wichtige Aquivalenzen

• Ein zweiter Kalkul: Logische Umformung

• Unerfullbarkeit/Allgemeingultigkeit/Folgerung

2. Aussagenlogik

Teil 3

06.05.2013

Unser Ziel

Kalkul(e) zur systematischen Uberprufung von Erfullbarkeit

(fur Formeln und/oder Formelmengen)

Dazu brauchen wir “Normalformen”

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

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

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

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

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

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)

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)

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.

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 )

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

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.

Umformung in KNF

Vier Schritte:

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

4. “Nach innen schieben” von ∨

Verwende Distributivitat von ∨ uber ∧

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

Umformung in DNF

Vier Schritte:

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

4. “Nach innen schieben” von ∧

Verwende Distributivitat von ∧ uber ∨

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)

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

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)︸︷︷︸

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

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

• Klausel in KNF von An: 2n

Beweis durch Induktion

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

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)

︸︷︷︸

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

︸︷︷︸

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

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} }

KNF: Mengenschreibweise

Bedeutung der leeren Menge

• Leere Klausel

= leere Menge von Literalen

= leere Disjunktion

• Leere Menge von Klausels

= leere Konjunktion

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)

Das SAT-Problem (Erfullbarkeitsproblem)

Definition: SAT-Problem

Gegeben: Eine aussagenlogische Formel F

Frage: Ist F erfullbar?

NB: F allgemeingultig gdw. ¬F nicht erfullbar

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

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

2. Aussagenlogik

Teil 4

07.05.2012

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

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)

Definition: SAT-Problem

Gegeben: Eine aussagenlogische Formel F

Frage: Ist F erfullbar?

Theorem (ohne Beweis)

SAT ist ein NP-vollstandiges Problem

Zur Erinnerung:

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

• 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

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

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

Definition:

Theorem

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

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

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.

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?

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.

Beispiel

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

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

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.

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 .

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.

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)

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.

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

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

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

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.

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 ⊤.

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

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

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

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.

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

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

Zusammenfassung

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

• Horn-Formeln

• Erfullbarkeitstest fur Hornformeln

2. Aussagenlogik

Teil 5

14.05.2012

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 |

Unser Ziel

1. Formeln in KNF (Mengen von Klauseln)

Resolution

2. Formelmengen

Semantische Tableaux

1. Resolution

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 ∨ R

¬Z ∨ P

{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.

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}

Verallgemeinerung?

Syllogismus (in der ersten Vorlesung erwahnt):

P P → C

Mengenschreibweise: 1-Resolution (unit resolution)

{P} {¬P} ∪ C

{¬P} {P} ∪ C

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

Der aussagenlogische Resolutionkalkul

Wesentliche Eigenschaften

• Widerlegungskalkul: Testet auf Unerfullbarkeit

• Voraussetzung: Alle Formeln in konjunktiver Normalform

• Eine einzige Regel

• Operiert auf Klauseln (in Mengenschreibweise)

Resolutionskalkul

Definition: Resolutionsregel (einzige Regel des Kalkuls)

C1 ∪ {P} {¬P} ∪ C2

C1 ∪ C2

• P eine aussagenlogische Variable

• C1,C2 Klauseln (konnen leer sein)

Definition:

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

Resolution: Beispiel

Gegeben die Klauselmenge:

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

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

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

{¬P1}

{P1} {¬P1}

Insgesamt: M ⊢Res⊥

also: M unerfullbar

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}}

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)

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

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

Ohne Mengenschreibweise

Resolutionsregel:

C1 ∨ P ¬P ∨ C2

C1 ∨ C2

Faktorisieren:C ∨ L ∨ L

C ∨ L

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

P2 ∨ P2

¬P2 ∨ ¬P2

P1 ¬P1

Resolution: Beispiel

Gegeben die Klauselmenge:

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

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

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

{¬P1}

{P1} {¬P1}

Insgesamt: M ⊢Res⊥

also: M unerfullbar

Resolution

Ziele:

• Formalisieren, was M ⊢Res⊥ bedeutet

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

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

j1, j2<i).

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

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)

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⊥.

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

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.

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.

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⊥

2. Aussagenlogik

Teil 6

28.05.2012

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.

Resolution: Korrektheit und Vollstandigkeit

letzte Vorlesung

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

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⊥

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⊥

Theorem.

Es gilt auch:

Theorem.

Fur jede Menge M von Klauseln gilt:

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.

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.

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

{¬P} {P} ∪ 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 ⊥.

Unser Ziel

Resolution bis jetzt

2. Formelmengen

Unser Ziel

Resolution

2. Formelmengen

Der aussagenlogische Tableaukalkul

Wesentliche Eigenschaften

• Widerlegungskalkul: Testet auf Unerfullbarkeit

• Beweis durch Fallunterscheidung

• Top-down-Analyse der gegebenen Formeln

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

Formeltypen

Konjunktive Formeln: Typ α

• ¬¬F

• F ∧ G

• ¬(F ∨ G)

• ¬(F → G)

Disjunktive Formeln: Typ β

• ¬(F ∧ G)

• F ∨ G

• F → G

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

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

Regeln des (aussagenlogischen) Tableaukalkuls

Konjunktiv

p ∧ q

β1 | β2

Disjunktiv

p ∨ q

Widerspruch

Instanzen der α und β-Regel

Instanzen der α-Regel

P ∧ Q

¬(P ∨ Q)

¬(P → Q)

Instanzen der β-Regel

P ∨ Q

¬(P ∧ Q)

¬P | ¬Q

P → Q

¬P | Q

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

(3) ¬Q

(6) ¬(Q ∨ ¬R)

(7) ¬Q

(8) ¬¬R

(4) ¬R

(10) P

(11) ¬(Q ∨ ¬R)

��

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

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

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)

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.

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

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.

Beispiel

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

��

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

2. Aussagenlogik

Teil 7

3.06.2013

Klauseltableau

M Menge von Klauseln

Anderungen

• Keine α-Regel

• Erweiterungsregel kann Verzweigungsgrad > 2 haben

• Alle Knoten im Tableau enthalten Literale

Klauseltableau: Beispiel

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

gggggg

VVVVVV

uuuu KK

uuuu LL

ssss PP

pppp II

⊥ P Q R ¬P ¬Q ⊥

⊥ ⊥ ⊥ ⊥ ⊥

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.

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

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

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

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.

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.

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.

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.

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”

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

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.

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.

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

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)

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)

¬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

Beobachtung

Konstruktion des Konnektionstableaus

• bei Beginn mit Klausel (1)

• mit Regularitat

• mit starker Konnektionsbedingung

Nahezu deterministische Beweiskonstruktion

(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

M V P F

2. Aussagenlogik

Teil 8

4.06.2013

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

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

VioricaSofronie-Stokkermans...

Documents

Transcript of VioricaSofronie-Stokkermans...

Kampf der Roboter Part1

Aussagen Logik

Jedem seine Logik!

StartupHub Berlin /Part1

Georg Wilhelm Friedrich Hegel - Die Wissenschaft der Logik. Die subjektive Logik (1834)

Slv big white 2016 de part1

Franz von Kutschera Regensburg · Gottlob Frege, der Begründer der formalen Logik in ihrer heutigen Gestalt, hatte, beginnend mit der „Begriffsschrift" (Halle 1879) eine Formalisierung

Maytoni catalog2016 part1

1 Computergestützte Verifikation 23.4.2002. 2 Inhalt System Abstraktion Spezifikation Simulation Formalisierung Model Checker Gegenbeispiel Modell log.

Fuzzy-Logik Eine Einführung in unscharfe Logik Nils Becker, November 2012 1.

eglo 2012 part1

Zur Formalisierung von urbaner Informalität ...

Design Thinking in a Nutshell - Part1

Logik f¨ur Informatiker 1. Grundlegende Beweisstrategiensofronie/logik-ss-2012/slides/... · Logik f¨ur Informatiker 1. Grundlegende Beweisstrategien Viorica Sofronie-Stokkermans

Logik, Mengen, Relationen

Formalisierung der Semanto-Pragmatik für eine Japanische ... · Formalisierung der Semanto-Pragmatik für eine Japanische Grammatik Jens Rickmeyer — Winfried Boeder zu seinem 65.

Facebook handbuch part1

INHALTSVERZEICHNIS POLYKONTEXTURALE LOGIK. …thinkartlab.com/pkl/media/DISSEM-final.pdf · 1 INHALTSVERZEICHNIS POLYKONTEXTURALE LOGIK. Zur Konzeption, Formalisierung und Validierung.

Logik für Informatiker - KIT · Vorlesung Logik für Informatiker 6. Aussagenlogik – Resolution – Bernhard Beckert Universität Koblenz-Landau Sommersemester 2006 Logik für

Jedem seine Logik! - Conrad Electronic · Jedem seine Logik! Die dritte Generation von Logik-Controllern für Ihre branchenspezifischen Anwendungen. Größerer Speicher für Ihre