Aussagenlogik: Syntax von Aussagen

engl.: Propositional Logic

A ::= X | (A ∧A) | (A ∨A) | (¬ A) | (A⇒ A) | (A⇔ A) | 0 | 1

A ∧B: Konjunktion (Verundung).A ∨B: Disjunktion (Veroderung).A⇒ B: Implikation .A⇔ B: Aquivalenz.¬A: negierte Formel.A Atom, falls A eine Variable ist.A Literal, falls A Atom oder negiertes Atom.

Prioritatsreihenfolge (bzgl Klammerung): ¬,∧,∨,⇒, ⇐⇒ .

AD, SS 2014, Folien Aussagenlogik, Seite 1, 5. Mai 2014

Aussagenlogik: Semantik

Zunachst pro Operation op ∈ {¬,∧,∨,⇒,⇔}eine Funktion fop gemaß folgender Tabelle.

∧ ∨ ⇒ NOR NAND ⇔ XOR1 1 1 1 1 0 0 1 01 0 0 1 0 0 1 0 10 1 0 1 1 0 1 0 10 0 0 0 1 1 1 1 0

AD, SS 2014, Folien Aussagenlogik, Seite 2, 5. Mai 2014

Interpretation

Definition

Eine Interpretation I ist eine Funktion:I : {aussagenlogische Variablen} → {0,1}.

I: Aussage → Wahrheitswert:

• I(0) := 0, I(1) := 1

• I(¬A) := f¬(I(A))

• I(A op B) := fop(I(A), I(B)), wobei op ∈ {∧,∨,⇒,⇔ . . .}

I(F ) = 1, entspricht I |= F . ( I ist ein Modell fur F , F gilt in I, I

macht F wahr)

AD, SS 2014, Folien Aussagenlogik, Seite 3, 5. Mai 2014

Definition: Tautologie usw.

• A ist eine Tautologie (Satz der Aussagenlogik, allgemeingultig in

der Aussagenlogik) gdw. fur alle Interpretationen I gilt: I |= A.

• A ist ein Widerspruch (widerspruchlich, unerfullbar) gdw. fur alle

Interpretationen I gilt: I(A) = 0.

• A ist erfullbar (konsistent) gdw. es eine Interpretationen I gibt mit:

I |= A.

• ein Modell fur eine Formel A ist eine Interpretation I mit I(A) = 1.

AD, SS 2014, Folien Aussagenlogik, Seite 4, 5. Mai 2014

Beispiele fur Tautologie usw.

• X ∨ ¬X ist eine Tautologie.

• (X ⇒ Y )⇒ ((Y ⇒ Z)⇒ (X ⇒ Z)) ist eine Tautologie.

• X ∧ ¬X ist ein Widerspruch.

• X ∨ Y ist erfullbar.

• I mit I(X) = 1, I(Y ) = 0 ist ein Modell fur X ∧ ¬Y

AD, SS 2014, Folien Aussagenlogik, Seite 5, 5. Mai 2014

Komplexitaten

Eingabe: Eine aussagenlogische Formel A

1. Ist A erfullbar? ist NP-vollstandig.

2. Ist A Tautologie ? ist co-NP-vollstandig.

D.h. Zur Beantwortung beider Fragen sind nur worst-case

EXPTIME-Algorithmen bekannt.

AD, SS 2014, Folien Aussagenlogik, Seite 6, 5. Mai 2014

Folgerungsbegriffe

• semantische Folgerung: |=.

A |= B gdw. fur alle Interpretationen I:

I(A) = 1⇒ I(B) = 1

• syntaktische Folgerung (`, Herleitung)

Regelsystem zum Herstellen von Aussagen ( Folgerungen)

A ` B

AD, SS 2014, Folien Aussagenlogik, Seite 7, 5. Mai 2014

Kalkul: Korrektheit und Vollstandigkeit

Kalkul: Ein (i.a. nicht-deterministischer) Algorithmus A, der aus einer

Menge von Formeln H eine neue Formel H berechnet. (H `A H)

• A ist korrekt (sound), gdw. H →A H impliziert H |= H

• A ist vollstandig (complete), gdw. H |= H impliziert, dass H `A H

Kalkule (z.B.): WahrheitstafelnBDDs und VariantenResolutionTableauDPLL-Verfahren

AD, SS 2014, Folien Aussagenlogik, Seite 8, 5. Mai 2014

Deduktionstheorem

Eine wichtige Eigenschaft der Aussagenlogik:

Satz {F1, . . . , Fn} |= G gdw. F1 ∧ . . . ∧ Fn ⇒ G ist Tautologie.

AD, SS 2014, Folien Aussagenlogik, Seite 9, 5. Mai 2014

Aquivalenz

F,G sind aquivalent (F ∼ G), gdw. wenn F ⇐⇒ G ist Tautologie

F ∼ G gdw fur alle I: I |= F gdw. I |= G gilt.

Beachte z.B. X ∧ Y 6∼ X ′ ∧ Y ′

AD, SS 2014, Folien Aussagenlogik, Seite 10, 5. Mai 2014

Aussagenlogische Satze

∧ und ∨ sind kommutativ, assoziativ, und idempotent:

F ∧ G ⇐⇒ G ∧ FF ∧ F ⇐⇒ F

F ∧ (G ∧H) ⇐⇒ (F ∧ G) ∧HF ∨ G ⇐⇒ G ∨ F

F ∨ (G ∨H) ⇐⇒ (F ∨ G) ∨HF ∨ F ⇐⇒ F

(F ,G,H sind aussagenlogische Formeln)

AD, SS 2014, Folien Aussagenlogik, Seite 11, 5. Mai 2014

Aquivalenzen:

¬(¬A)) ⇐⇒ A(A⇒ B) ⇐⇒ (¬A ∨B)(A ⇐⇒ B) ⇐⇒ ((A⇒ B) ∧ (B ⇒ A))¬(A ∧B) ⇐⇒ ¬A ∨ ¬B (DeMorgansche Gesetze)¬(A ∨B) ⇐⇒ ¬A ∧ ¬BA ∧ (B ∨ C) ⇐⇒ (A ∧B) ∨ (A ∧ C) DistributivitatA ∨ (B ∧ C) ⇐⇒ (A ∨B) ∧ (A ∨ C) Distributivitat(A⇒ B) ⇐⇒ (¬B ⇒ ¬A) KontrapositionA ∨ (A ∧B) ⇐⇒ A AbsorptionA ∧ (A ∨B) ⇐⇒ A Absorption

AD, SS 2014, Folien Aussagenlogik, Seite 12, 5. Mai 2014

Normalform DNF

disjunktive Normalform (DNF).

Disjunktion von Konjunktionen von Literalen.

(L1,1 ∧ . . . ∧ L1,n1) ∨ . . . ∨ (Lm,1 ∧ . . . ∧ Lm,nm)

AD, SS 2014, Folien Aussagenlogik, Seite 13, 5. Mai 2014

Normalform CNF

konjunktive Normalform (CNF) =Konjunktion von Disjunktionen von Literalen.

(L1,1 ∨ . . . ∨ L1,n1) ∧ . . . ∧ (Lm,1 ∨ . . . ∨ Lm,nm)

Auch: Klauselform oft:”

Menge von Mengen“-Schreibweise

Literal L z.B. X, ¬YKlausel (Lm,1 ∨ . . . ∨ Lm,nm) z.B. (X ∨ ¬Y )

{Lm,1, . . . , Lm,nm}

Klauselmenge(L1,1 ∨ . . . ∨ L1,n1

)∧ . . .∧ (Lm,1 ∨ . . . ∨ Lm,nm)

z.B. {{X,¬Y }, {Y }}

AD, SS 2014, Folien Aussagenlogik, Seite 14, 5. Mai 2014

Transformation in eine Klauselmenge

Notwendig fur Resolution und DPLL

1. Elimination von ⇔ und ⇒:

F ⇔ G → (F ⇒ G) ∧ (G⇒ F )F ⇒ G → ¬F ∨G

2. Negation ganz nach innen schieben:

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

3. Distributivitat (und Assoziativitat, Kommutativitat) iterativ an-wenden, um ∧ nach außen zu schieben (

”Ausmultiplikation“).

F ∨ (G∧H)→ (F ∨G)∧ (F ∨H) (Das duale Distributivgesetz wurdeeine disjunktive Normalform ergeben.)

AD, SS 2014, Folien Aussagenlogik, Seite 15, 5. Mai 2014

Transformation in eine Klauselmenge, Resultat

Konjunktion von Disjunktionen (Klauseln) von Literalen:

(L1,1 ∨ . . . ∨ L1,n1)

∧ (L2,1 ∨ . . . ∨ L2,n2)

∧. . .∧ (Lk,1 ∨ . . . ∨ Lk,nk

)

oder in (Multi-)Mengenschreibweise:

{{L1,1, . . . , L1,n1},

{L2,1, . . . , L2,n2},

. . .{Lk,1, . . . , Lk,nk

}}

AD, SS 2014, Folien Aussagenlogik, Seite 16, 5. Mai 2014

Transformation: Eigenschaften

Resultat-CNF ist aquivalent zur eingegebenen Formel

Dieser CNF-Algorithmus ist worst-case exponentiell

Anzahl der Literale in der Klauselform wachst exponentiell

Grunde:

• die Elimination von ⇔:Betrachte die Formel (A1 ⇔ A2)⇔ (A3 ⇔ A4)

• Ausmultiplikation mittels Distributivgesetz:

(A1∧. . .∧An)∨B2∨. . .∨Bm → ((A1∨B2)∧. . .∧(An∨B2))∨B3 . . .∨Bn

Dies verdoppelt B2 und fuhrt zum Iterieren des Verdoppelns, wennBi selbst wieder zusammengesetzte Aussagen sind.

AD, SS 2014, Folien Aussagenlogik, Seite 17, 5. Mai 2014

Schnelle CNF-Herstellung (Tseitin)

F → FCNF -transformation in Zeit O(n ∗ log(n)).

Eigenschaft: F erfullbar gdw. FCNF erfullbar!(Erfullbarkeits-Erhaltung)

Evtl: F 6∼ FCNF

AD, SS 2014, Folien Aussagenlogik, Seite 18, 5. Mai 2014

Schnelle CNF-Herstellung

Die Idee: komplexe Subformeln durch Variablen abkurzen.

F [G] −→ (A ⇐⇒ G) ∧ F [A] (A neue Variable)

Lemma F [G] ist erfullbar gdw. (G ⇐⇒ A) ∧ F [A] erfullbar ist.

Hierbei muss A eine Variable sein, die nicht in F [G] vorkommt.

AD, SS 2014, Folien Aussagenlogik, Seite 19, 5. Mai 2014

Schnelle CNF-Herstellung

Def: Tiefe einer Aussage :=

maximale Lange eines Pfades im Syntaxbaum

Def: Sub-Tiefe einer Unter-Aussage H in F :=

Lange des Pfades

von der Wurzel zur Subformel H im Syntaxbaum

AD, SS 2014, Folien Aussagenlogik, Seite 20, 5. Mai 2014

Schneller CNF-Algorithmus

• Die Formel sei H1 ∧ . . . ∧Hn

• Wenn Hj eine Tiefe ≥ 4 hat, dann ersetze alle Subfor-

meln G1, . . . , Gm von Hj mit Sub-Tiefe 3 in Hj, und die

keine Atome sind, durch neue Variablen Ai: D.h.

Hj = H ′j[G1, . . . , Gm] −→H ′j[A1, . . . , Am] ∧ (G1 ⇐⇒ A1) ∧ . . . ∧ (Gm ⇐⇒ Am)

• Iteriere diesen Schritt• Danach wandle die verbliebenen Formeln in CNF um.

AD, SS 2014, Folien Aussagenlogik, Seite 21, 5. Mai 2014

SAT und k-SAT

• SAT ist das Erfullbarkeitsproblem fur Klauselmengen

• Die Problemklasse ist NP-vollstandig

• k-SAT ist das Erfullbarkeitsproblem fur Klauselmengen mit nur

Klauseln der Lange k.

• 2-SAT ist polynomiell entscheidbar,

• k-SAT fur k > 2 ist NP-hart.

AD, SS 2014, Folien Aussagenlogik, Seite 22, 5. Mai 2014

SAT und Erfullbarkeit durch Abzahlen

Satz Wenn fur ein k ≥ 2 in der Klauselmenge S

alle Klauseln die Lange k haben,

und es sind h < 2k Klauseln,

dann ist S erfullbar.

Beweis durch Abzahlen der Interpretationen.

Beispiel k = 3 und maximal 7 Klauseln, dann ist die Klauselmenge

erfullbar.

AD, SS 2014, Folien Aussagenlogik, Seite 23, 5. Mai 2014

Resolutionsverfahren fur Aussagenlogik

statt Test auf Allgemeingultigkeit von F :

Testen von ¬F auf Widerspruch.

etwas allgemeiner:

Lemma

A1 ∧ . . . ∧An ⇒ F ist allgemeingultig

gdw.

A1 ∧ . . . ∧An ∧ ¬F widerspruchlich ist.

AD, SS 2014, Folien Aussagenlogik, Seite 24, 5. Mai 2014

Resolutionsverfahren fur Aussagenlogik

Resolution operiert auf Klauselmengenerzeugt aus zwei (Eltern-)Klauseln eine Resolventedie zur Klauselmenge hinzugefugt wird

A ∨B1 ∨ . . . ∨Bn

¬A ∨C1 ∨ . . . ∨ Cm

B1 ∨ . . . ∨Bn ∨ C1 ∨ . . . ∨ Cm

Resolution wird iteriert.

Falls leere Klausel als Resolvente: Erfolgreich beendet

Resolution auf Klauselmengen: als Menge von MengenC → C ∪ {R}

AD, SS 2014, Folien Aussagenlogik, Seite 25, 5. Mai 2014

Terminierung der aussagenlogischen Resolution

Satz Die Resolution auf einer aussagenlogischen Klauselmenge

terminiert, wenn ein Resolutionsschritt nur erlaubt ist

bei Vergroßerung der Klauselmenge.

Grund: Es gibt nur endlich viele mogliche Klauseln, da Resolution keine

neuen Variablen einfuhrt.

AD, SS 2014, Folien Aussagenlogik, Seite 26, 5. Mai 2014

Vollstandigkeit der Resolution

Satz Fur eine unerfullbare Klauselmenge findet Resolution nach endlich

vielen Schritten die leere Klausel.

Beweis: . . .

Die Komplexitat der Resolution im schlimmsten Fall:

Satz Es gibt eine Folge von Formeln (die sogenannten Taubenschlag-

formeln bzw. pigeon hole formula, Schubfach-formeln), fur die die

kurzeste Herleitung der leeren Klausel mit Resolution eine exponen-

tielle Lange (in der Große der Formel) hat.

(A. Haken 1985) (siehe auch E. Eder 1992))

AD, SS 2014, Folien Aussagenlogik, Seite 27, 5. Mai 2014

Davis-Putnam-Logemann-Loveland Algorithmus

DP (·)

1 a. Wenn leere Klausel in C: RETURN true.b. Wenn C leere Klauselmenge: RETURN false.

2. wenn 1-Klausel {P} (bzw. {¬P}) ex:a Losche Klauseln in denen P (bzw. ¬P ) vorkommt.b Losche Literale ¬P (bzw. P ) in Klauseln

ergibt Klauselmenge C′. RETURN DP (C′)3. Wenn isolierte Literale existieren:

Losche Klauseln, in denen isolierte Literale vorkommen.resultierende Klauselmenge: C′. RETURN DP (C′)

4 Sonst: wahle eine ex. Variable P aus.RETURN DP (C ∪ {P}) ∧DP (C ∪ {¬P})

AD, SS 2014, Folien Aussagenlogik, Seite 28, 5. Mai 2014

Beispiel fur DP

P, Q¬P, Q RP, ¬Q, R¬P, ¬Q, RP, Q, ¬R¬P, Q, ¬RP, ¬Q, ¬R¬P, ¬Q, ¬R

Fall 1: Addiere die Klausel {P}. nach einigen Schritten:

Q, R¬Q, RQ, ¬R¬Q, ¬R

AD, SS 2014, Folien Aussagenlogik, Seite 29, 5. Mai 2014

Fall 1.1: Addiere {Q}: ergibt die leere Klausel.

Fall 1.2: Addiere {¬Q}: ergibt die leere Klausel.

Fall 2: Addiere die Klausel {¬P}. Nach einigen Schritten:

Q¬Q RQ ¬R¬Q ¬R

Weitere Schritte fur Q ergeben

R¬R

ergibt leere Klausel.

Smullyan: Wer ist der Pfefferdieb?

Ratsel von Raymond Smullyan:

Es gibt drei Verdachtige: Den Hutmacher, den Schnapphasen und die

(Hasel-)Maus. Folgendes ist bekannt:

• Genau einer von ihnen ist der Dieb.

• Unschuldige sagen immer die Wahrheit

• Schnapphase: der Hutmacher ist unschuldig.

• Hutmacher: die Hasel-Maus ist unschuldig

AD, SS 2014, Folien Aussagenlogik, Seite 31, 5. Mai 2014

Kodierung: H,S,M

1. H ∨ S ∨M2. H ⇒ ¬(S ∨M)3. S ⇒ ¬(H ∨M)4. M ⇒ ¬(H ∨ S)5. ¬S ⇒ ¬H6. ¬H ⇒ ¬M

Klauselmenge:

{{H,S,M}, {¬H,¬S}, {¬H,¬M}, {¬S,¬M}, {S,¬H}, {H,¬M}}

pfefferdieb = dp

"((H \/ S \/ M) /\(H => -(S \/ M))

/\(S => -(H \/ M)) /\ (M => -(H \/ S))

/\(-S => -H) /\ (-H => -M))"

Modell: S, -M, -H"

AD, SS 2014, Folien Aussagenlogik, Seite 32, 5. Mai 2014

DP-Implementierung Besonderheiten

Die Optimierung zu isolierten Literalen ist gut fur Widerspruchssuche,

aber nicht fur Modellsuche.

Beachte: die pureliterals-Optimierung ist nicht aktiviertin der dp-Implementierung, so dassdpalle eine exakte Losung angibt

AD, SS 2014, Folien Aussagenlogik, Seite 33, 5. Mai 2014

Eine Logelei aus der”

Zeit“

Abianer sagen die Wahrheit, Bebianer lugen. Aussagen:

1. Knasi: Knisi ist Abianer.2. Knesi: Wenn Knosi Bebianer, dann ist auch Knusi ein Abianer.3. Knisi: Wenn Knusi Abianer, dann ist Knesi Bebianer.4. Knosi: Knesi und Knusi sind beide Abianer.5. Knusi: Wenn Knusi Abianer ist, dann ist auch Knisi Abianer.6. Knosi: Entweder ist Knasi oder Knisi Abianer.7. Knusi: Knosi ist Abianer.

A <=> I

E <=> (-OE => U)

I <=> (U => -E)

O <=> (E /\ UE)

U <=> (UE => I)

OE <=> (A XOR I)

UE <=> O

AD, SS 2014, Folien Aussagenlogik, Seite 34, 5. Mai 2014

Logelei: Losung

Die Eingabe in den Davis-Putnam-Algorithmus ergibt:

abianer1Expr = "((A <=> I) /\ (E <=> (-OE => U)) /\ (I <=> (U => -E))

/\ (O <=> (E /\ UE)) /\ (U <=> (UE => I))

/\ (OE <=> -(A <=> I)) /\ (UE <=> O))"

abianer1 = dp abianer1Expr

Resultat:

"Modell: -OE, -O, -UE, E, U, -I, -A"

Damit sind Knesi und Knusi Abianer, die anderen sind Bebianer.

AD, SS 2014, Folien Aussagenlogik, Seite 35, 5. Mai 2014

Das n-Damen Problem: aussagenlogisch

n Damen auf ein Schachbrett der Seitenlange n

Bedingung: keine Bedrohung

Ein Programm zum Erzeugen der Klauselmenge erzeugt im Fall n = 4:

> generate_nqueens 4

[[1, 2, 3, 4], [5, 6, 7, 8], [9, 10, 11, 12], [13, 14, 15, 16], [1, 5, 9, 13],

.....

davisPutnam (generate_nqueens 4)

davisPutnamAlle (generate_nqueens 4)

dpqueensAlle 4

dpqueensAlle 6

dpqueensAlle 8

AD, SS 2014, Folien Aussagenlogik, Seite 36, 5. Mai 2014

Das n-Damen Problem: aussagenlogisch

Der Aufruf dpqueens 8 ergibt:

- - D - - - - -

- - - - - - D -

- D - - - - - -

- - - - - - - D

- - - - D - - -

- - - - - - -

- - - D - - - -

- - - - - D - -

AD, SS 2014, Folien Aussagenlogik, Seite 37, 5. Mai 2014

n-Damen Problem, Torus-Variante

Polya: es gibt eine Losung des n-Damen Torus-Problems wenn n ≥ 5

und n teilerfremd zu 6 ist. Losungen fur n = 5,7,11,13,17, ..

keine Losungen fur n = 4,6,8,9,10,12,14,15,16, . . ..

Eine Losung:

D - - - -

- - D - -

- - - - D

- D - - -

- - - D -

dpqueenscyl n

AD, SS 2014, Folien Aussagenlogik, Seite 38, 5. Mai 2014

n-Damen Problem, Torus-Variante

Fur n = 11 werden 4 Losungen ermittelt undfur n = 13 werden 174 Losungen ermittelt (allerdings nach einer Sym-metrieoptimierung).Eine generische Losung ist (Nr 33.):

D - - - - - - - - - - - -

- - D - - - - - - - - - -

- - - - D - - - - - - - -

- - - - - - D - - - - - -

- - - - - - - - D - - - -

- - - - - - - - - - D - -

- - - - - - - - - - - - D

- D - - - - - - - - - - -

- - - D - - - - - - - - -

- - - - - D - - - - - - -

- - - - - - - D - - - - -

- - - - - - - - - D - - -

- - - - - - - - - - - D -

AD, SS 2014, Folien Aussagenlogik, Seite 39, 5. Mai 2014

Sudoku: Losen mittels DP-Algorithmus

• Texteingabe

• Parser: Texteingabe −→ Klauselmenge aus Units

• Generator: Klauselmenge, die alle Bedingungen beschreibt.

• DP-Lauf

• Interpretation −→ Losung als Text.

AD, SS 2014, Folien Aussagenlogik, Seite 40, 5. Mai 2014

Sudoku: Losen mittels DP-Algorithmus

sudokuex20100419 =

["3--5-4--1",

"-1-----7-",

"--9-1-5--",

"4--3-9--7",

"--3---9--",

"1--8-7--6",

"--5-6-2--",

"-8-----4-",

"2--4-5--9"]

> length (sudokucnf sudokuex20100419)

12016

> sudokuexam20100419loesung = sudokul sudokuex20100419

> sudokuexam20100419trace

> sudokuexam20100419loesung

AD, SS 2014, Folien Aussagenlogik, Seite 41, 5. Mai 2014

Sudoku: Losen mittels DP-Algorithmus

> sudokuexam20100419loesung

326574891

514698372

879213564

468329157

753146928

192857436

945761283

681932745

237485619

DP-Rechenzeit: im Sekundenbereichspezialisierte Algorithmen Milli-Sekunden

AD, SS 2014, Folien Aussagenlogik, Seite 42, 5. Mai 2014