Aussagenlogik: Syntax von Aussagen - uni- · PDF file 2014. 5. 5. · Aussagenlogik:...

Click here to load reader

  • date post

    18-Jan-2021
  • Category

    Documents

  • view

    1
  • download

    0

Embed Size (px)

Transcript of Aussagenlogik: Syntax von Aussagen - uni- · PDF file 2014. 5. 5. · Aussagenlogik:...

  • 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: Äquivalenz. ¬A: negierte Formel. A Atom, falls A eine Variable ist. A Literal, falls A Atom oder negiertes Atom.

    Prioritätsreihenfolge (bzgl Klammerung): ¬,∧,∨,⇒, ⇐⇒ .

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

  • Aussagenlogik: Semantik

    Zunächst pro Operation op ∈ {¬,∧,∨,⇒,⇔} eine Funktion fop gemäß folgender Tabelle.

    ∧ ∨ ⇒ NOR NAND ⇔ XOR 1 1 1 1 1 0 0 1 0 1 0 0 1 0 0 1 0 1 0 1 0 1 1 0 1 0 1 0 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 für 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, allgemeingültig in der Aussagenlogik) gdw. für alle Interpretationen I gilt: I |= A.

    • A ist ein Widerspruch (widersprüchlich, unerfüllbar) gdw. für alle Interpretationen I gilt: I(A) = 0.

    • A ist erfüllbar (konsistent) gdw. es eine Interpretationen I gibt mit: I |= A.

    • ein Modell für eine Formel A ist eine Interpretation I mit I(A) = 1.

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

  • Beispiele für Tautologie usw.

    • X ∨ ¬X ist eine Tautologie.

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

    • X ∧ ¬X ist ein Widerspruch.

    • X ∨ Y ist erfüllbar.

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

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

  • Komplexitäten

    Eingabe: Eine aussagenlogische Formel A

    1. Ist A erfüllbar? ist NP-vollständig.

    2. Ist A Tautologie ? ist co-NP-vollständig.

    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. für 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

  • Kalkül: Korrektheit und Vollständigkeit

    Kalkül: 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 vollständig (complete), gdw. H |= H impliziert, dass H `A H

    Kalküle (z.B.): Wahrheitstafeln BDDs und Varianten Resolution Tableau DPLL-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

  • Äquivalenz

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

    F ∼ G gdw für 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 Sätze

    ∧ und ∨ sind kommutativ, assoziativ, und idempotent:

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

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

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

    (F ,G,H sind aussagenlogische Formeln)

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

  • Äquivalenzen:

    ¬(¬A)) ⇐⇒ A (A⇒ B) ⇐⇒ (¬A ∨B) (A ⇐⇒ B) ⇐⇒ ((A⇒ B) ∧ (B ⇒ A)) ¬(A ∧B) ⇐⇒ ¬A ∨ ¬B (DeMorgansche Gesetze) ¬(A ∨B) ⇐⇒ ¬A ∧ ¬B A ∧ (B ∨ C) ⇐⇒ (A ∧B) ∨ (A ∧ C) Distributivität A ∨ (B ∧ C) ⇐⇒ (A ∨B) ∧ (A ∨ C) Distributivität (A⇒ B) ⇐⇒ (¬B ⇒ ¬A) Kontraposition A ∨ (A ∧B) ⇐⇒ A Absorption A ∧ (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, ¬Y Klausel (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 für 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. Distributivität (und Assoziativität, Kommutativität) iterativ an- wenden, um ∧ nach außen zu schieben (

    ” Ausmultiplikation“).

    F ∨ (G∧H)→ (F ∨G)∧ (F ∨H) (Das duale Distributivgesetz würde eine 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 äquivalent zur eingegebenen Formel

    Dieser CNF-Algorithmus ist worst-case exponentiell

    Anzahl der Literale in der Klauselform wächst exponentiell

    Gründe:

    • 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 führt zum Iterieren des Verdoppelns, wenn Bi 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 erfüllbar gdw. FCNF erfüllbar! (Erfüllbarkeits-Erhaltung)

    Evtl: F 6∼ FCNF

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

  • Schnelle CNF-Herstellung

    Die Idee: komplexe Subformeln durch Variablen abkürzen.

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

    Lemma F [G] ist erfüllbar gdw. (G ⇐⇒ A) ∧ F [A] erfüllbar 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 Länge eines Pfades im Syntaxbaum

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

    Länge 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 Erfüllbarkeitsproblem für Klauselmengen

    • Die Problemklasse ist NP-vollständig

    • k-SAT ist das Erfüllbarkeitsproblem für Klauselmengen mit nur Klauseln der Länge k.

    • 2-SAT ist polynomiell entscheidbar,

    • k-SAT für k > 2 ist NP-hart.

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

  • SAT und Erfüllbarkeit durch Abzählen

    Satz Wenn für ein k ≥ 2 in der Klauselmenge S alle Klauseln die Länge k haben,

    und es sind h < 2k Klauseln,

    dann ist S erfüllbar.

    Beweis durch Abzählen der Interpretationen.

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

    erfu