Aussagenlogik: Syntax von Aussagen - uni-frankfurt.de · 2014. 5. 5. · Aussagenlogik: Semantik...

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


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)


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.


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


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.


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


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


Deduktionstheorem

Eine wichtige Eigenschaft der Aussagenlogik:

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


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 ′


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)


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


Normalform DNF

disjunktive Normalform (DNF).

Disjunktion von Konjunktionen von Literalen.

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


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


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


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

}}


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.


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


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.


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


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.


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.


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.


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.


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}


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.


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


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


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


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


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"


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


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


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.


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


Das n-Damen Problem: aussagenlogisch

Der Aufruf dpqueens 8 ergibt:

- - D - - - - -

- - - - - - D -

- D - - - - - -

- - - - - - - D

- - - - D - - -

- - - - - - -

- - - D - - - -

- - - - - D - -


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


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 -


Sudoku: Losen mittels DP-Algorithmus

• Texteingabe

• Parser: Texteingabe −→ Klauselmenge aus Units

• Generator: Klauselmenge, die alle Bedingungen beschreibt.

• DP-Lauf

• Interpretation −→ Losung als Text.



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



> sudokuexam20100419loesung

326574891

514698372

879213564

468329157

753146928

192857436

945761283

681932745

237485619

DP-Rechenzeit: im Sekundenbereichspezialisierte Algorithmen Milli-Sekunden


Aussagenlogik: Syntax von Aussagen - uni-frankfurt.de · 2014. 5. 5. · Aussagenlogik: Semantik...

Documents

Transcript of Aussagenlogik: Syntax von Aussagen - uni-frankfurt.de · 2014. 5. 5. · Aussagenlogik: Semantik...