Theoretische Informatik - Einführung, Formale Logik, Aussagenlogik PDF

051013 VO Theoretische Informatik Einführung, Formale Logik in der Informatik, Aussagenlogik Ekaterina Fokina  Section 1 VO Theoretische Informatik - Ausblick  Abstraktion Abstraktion ist ein zentrales Konzept...

051013 VO Theoretische Informatik Einführung, Formale Logik in der Informatik, Aussagenlogik Ekaterina Fokina  Section 1 VO Theoretische Informatik - Ausblick  Abstraktion Abstraktion ist ein zentrales Konzept in der Informatik: Abstraktion Reduktion der vorhanden Information auf die für das aktuelle Problem wesentliche Information. oft auch: die Reduktion auf ein allgemeineres bzw. einfacheres Konzept. Beispiel Statt eine Landkarte zu betrachten verwendet man eine Graphen mit den Distanzen zwischen den relevanten Zielen.  Modell Modell Vereinfachte abstrakte Darstellung eines komplexen Systems (eines Ausschnitts der Realität“) ” um dieses einfacher zu verstehen und zu analysieren. Es werden nur die für den Zweck relevanten Aspekte darstellt. Analyse von Systemen Modell kommt nach der Realität. Modell wird angepasst, bis es die Realität wiedergibt. Kritischer Vergleich der Voraussagen des Modells mit der Realität. Planung/Spezifikation von Systemen Modell kommt vor dem System. System wird angepasst und korrigiert, bis es dem Modell entspricht. Kritischer Vergleich des Systemverhaltens mit dem Modell.  Natürliche Sprachen Natürliche Sprachen sind universell, vielseitig, ausdrucksstark, und wandlungsfähig, aber auch komplex, mehrdeutig, und ungenau. und daher nicht gut geeignet zur Modellierung und Spezifikation.  Natürliche Sprachen (Mehrdeutigkeit) Mehrdeutigkeit einzelner Wörter: Rodel. Sackrodelb Rodelschlittena vs. anderes Beispiel: Schimmel (Pilz oder Pferd?) a Bild Von Basti007 - Eigenes Werk, CC BY 3.0, https://commons.wikimedia.org/w/index.php?curid=20206926 b Bild Gemeinfrei, https://commons.wikimedia.org/w/index.php?curid=971442.  Natürliche Sprachen (ungenau) Beispiel Der Satz: “Jede Frau liebt einen Mann” kann unterschiedlich interpretiert werden Jede Frau liebt mindestens einen Mann. Jede Frau liebt genau einen Mann. Alle Frauen lieben den selben Mann.  Formale Sprachen Kernaspekte formaler Sprachen: Syntax: Welche Äußerungen sind in der Sprache gültig? Semantik: Was bedeuten diese gültigen Äußerungen? Ausdrucksstärke: Was kann in der Sprache ausgedrückt werden? Formale Sprachen in der THI-Vorlesung Logische Sprachen (Teil 1) Aussagenlogik Prädikatenlogik Prolog (Logische Programmierung) Reguläre Ausdrücke (Teil 2) Formale Grammatiken (Teil 2) Automaten & Turing Maschinen (Teil 2)  Heute Logik in der Informatik: ein Überblick Aussagenlogik: Syntax Semantik Grundbegri↵e Eigenschaften Formalisieren in Aussagenlogik: Beispiele  Section 2 Formale Logik in der Informatik  Formale Logik in der Informatik Das Gebiet der Logik beschäftigt sich mit den Prinzipien des korrekten Schließens. hat Überschneidungen mit vielen Wissenschaftsdisziplinen: Philosophie, Mathematik, Rechtswissenschaften,... , und Informatik. Wir interessieren uns für formale Logik (auch mathematische Logik) Basiert auf Formalen Sprachen. Studiert die Gültigkeit von Ableitungs- und Folgerungsbeziehungen.  Ergänzende/Weiterführende Literatur Die Vorlesung folgt dem Buch von Kreuzer & Kühling Martin Kreuzer, Stefan Kühling (2006). Logik für Informatiker. Addison-Wesley Verlag, ISBN-13: 978-3827372154 Freie Ressourcen: Wikibooks Logic for Computer Science. http://en.wikibooks.org/wiki/Logic for Computer Science In der Fachbereichsbibliothek: Jürgen Dassow (2005). Logik für Informatiker. Vieweg+Teubner Verlag, ISBN-13: 978-3519005186 Hartmut Ehrig et al. (2001). Mathematisch-strukturelle Grundlagen der Informatik. (Teil III & IV) Springer Verlag, ISBN-13: 978-3540419235  Worum geht es in der Logik? Es geht um das Ziehen von Schlussfolgerungen die Gültigkeit von Begründungen die Widerspruchsfreiheit zwischen Aussagen Die formale Logik befasst sich nicht mit dem Wahrheitsgehalt/Inhalt einer Aussage an sich, sondern mit Regeln die es erlauben aus wahren Aussagen richtige Schlüsse zu ziehen.  Worum geht es in der Logik? Beispiel Aussage 1: Jeder Mensch hat 2 Augen. Aussage 2: John ist ein Mensch. Schlussfolgerung: Also hat John 2 Augen. Beispiel Aussage 1: Jeder Mensch hat 4 Augen.3 Aussage 2: John ist ein Mensch. Shetle Schlussfolgerung: Also hat John 4 Augen. Beobachtungen: 1 Wir haben die gleiche (gültige) Regel zum Schlussfolgern verwendet. 2 Aber bei falschen Prämissen haben wir als Schluss eine falsche Aussage bekommen, obwohl die Regel korrekt ist. Bemerkung Im Allgemeinen kann es auch passieren, dass der Schluss zufälligerweise korrekt ist, auch wenn die Prämissen falsch sind. Dazu später in der Vorlesung.  Worum geht es in der Logik? Die formale Logik beschäftigt sich damit unter welchen Bedingungen man aus der Gültigkeit von Voraussetzungen auf die Gültigkeit von Folgerungen schließen kann. Dazu nutzen wir in der Informatik unterschiedliche logische Systeme (oft auch als unterschiedliche ”Logiken” bezeichnet).  Logische Systeme Bestandteile eines logischen Systems: 1 Syntax: Legt fest, welche formalen Ausdrücke als Formeln des logischen Systems gelten. Üblicherweise startet man von sogenannten atomaren Formeln und legt Regeln fest, wie aus diesen weitere Formeln zusammengesetzt werden dürfen. 2 Semantik: Regeln, die festlegen, wie Formeln Wahrheitswerte zugeordnet werden können. Dem syntaktischen Element einer Formel wird damit eine Bedeutung gegeben. 3 Kalkül: Ein System von Regeln zum (systematischen) Ableitung neuer wahrer Formeln.  Logische Systeme, Beispiele In der Vorlesung werden wir zwei logische Systeme kennen lernen Aussagenlogik Prädikatenlogik Es gibt aber noch unzählige andere logische Systeme (mit Bedeutung in der Informatik) Mehrwertige Logiken und Fuzzylogik Nichtmonotone Logiken (z.B.: Reitersche Default-Logik) Modallogik...  Anwendungen in der Informatik Boolesche Ausdrücke in Programmiersprachen (if Anweisungen) Formale Spezifikation Verifikation von Programmen Logische Programmierung Datenbanksysteme Wissensrepräsentation und Künstliche Intelligenz Berechenbarkeits- und Komplexitätstheorie...  Section 3 Aussagenlogik  Aussagenlogik - Einleitung Eine Aussage ist Ein Satz in der natürlichen Sprache (z.B. “Das Auto ist rot.”) Ist entweder wahr (W) oder falsch (F) Beispiel 4 ist größer als 10“ F ” 101 ist eine Primzahl“ W ” Junge Pferde nennt man Welpen“ F ” 4 ist größer als 10, oder 10 ist größer als 4“ W ” 4 ist größer als 10, und 10 ist größer als 4“ F ” Die Vorlesung ist im AudiMax“ ? ” Es gibt unendlich viele Primzahlzwillinge“ ? ”  Aussagenlogik - Einleitung Es gibt Aussagen, die aus der logischen Verknüpfung von mehreren einfacheren Aussagen bestehen. Wir wollen diese mit atomaren Aussagen und logischen Operatoren darstellen. Eine einfache/atomare Aussage ist eine Aussage die nur einen Sachverhalt enthält (unteilbare Aussage). Insbesondere enthält sie keine aussagenlogischen Verknüpfungen wie: nicht, und, oder, wenn... dann, genau dann wenn Als logische Operatoren / Verknüpfungen betrachten wir die Negation ¬A (NOT), > etwas gilt nicht - die Konjunktion A ^ B (AND), die Disjunktion A _ B (OR), und die Folgerung/Implikation A ! B. - wenn dann  Aussagenlogik - Einleitung Beispiel Die Aussage Das Auto ist rot und das Fahrrad ist grün“ besteht aus ” zwei atomare Aussagen: 1 Das Auto ist rot“ ” 2 Das Fahrrad ist grün“ ” Mit einer Konjunktion können wir die ursprüngliche Aussage aus den Atomen aufbauen. Das Auto ist rot“ ^ Das Fahrrad ist grün“ ” ” Beispiel Aussage: Gestern hat es in Wien geregnet“ ” Die Aussage ist atomar. Sie enthält zwar mehrere Informationen (Zeit, Ort, Wetter), beschreibt aber nur einen Sachverhalt und kann nicht in mehrere Aussagen aufgespalten werden.  Aussagenlogik - Einleitung bei oder muss min. Beispiele: Teil wahr sein, es können aber alle Beispiel Teile wahr sein 4 ist größer als 10, oder 10 ist größer als 4“ ” 4 ist größer als 10” _ “10 ist größer als 4“ ” Beispiel Wenn es regnet ist die Straße nass.“ ” Es regnet” ! “Die Straße ist nass.“ ” Beispiel Wenn ich nicht lerne, scha↵e ich die Prüfung nicht.“ ” (¬ “Ich lerne.”) ! (¬ Ich scha↵e die Prüfung.“) ” ( Ich lerne.”) _ (¬ Ich scha↵e die Prüfung.“) ” ”  Implikation Grundfrage: Wie hängen Aussagen zusammen? Implikation A ! B (,,A impliziert B”, ,,wenn A dann B”, ,,A hinreichend für B”, ,,B notwendig für A”) Beispiele der Form A ! B: 1 x = 1 ! x · y = y. 2 a, b sind Katheten und c Hypothenuse in einem rechtwinkeligen z Ausge Dreieck ! a2 + b 2 = c 2. weil sinnlos , Aber auch: x = 0 ! a + b = b + a 3 > - Hier: A, B sind jeweils nicht immer wahr, aber A ! B ist immer wahr. Genauer: A ! B ist falsch falls: A wahr ist und B falsch ist. Sonst ist A ! B immer wahr!  Implikation Beispiel Wenn es regnet, wird die Straße nass.  Äquivalenz Grundfrage: Wie hängen Aussagen zusammen? wenne Ach wahr , einendenz Äquivalenz A $ B (,,A genau dann, wenn B”) > - A $ B definiert als: A ! B und B ! A gelten gleichzeitig. Beispiele der Form A $ B: 1 x = 1 $ x 2 = 1: Gilt nicht, da zwar A ! B aber B 6! A. 2 x + y = 1 $ y + x = 1 + 2 · 0: Gilt (denn 1 = 1 + 2 · 0). von ein 1 y= 1 x=  Aussagen Die ,,wichtigsten” Aussagen in der Logik sind Äquivalenzen und Implikationen. Äquivalenz zwischen einer komplizierten und einer einfachen Aussage: x2 5x + 6 = 0 $ (x = 2 _ x = 3). Implikation drückt ,,Wissen über Spezialfälle” aus: Theorem (Nullstellensatz v. Bolzano) Sei f eine Funktion stetig auf [a, b] und f (a)  0  f (b). Dann gibt es ein y sodass a  y  b und f (y ) = 0.  Beispiel durch 10 teilbar ist Sei A eine Aussage “n ist ein Vielfaches von 10”. Welche von den folgenden Aussagen sind notwendig für A? Hinreichend für A? Äquivalent zu A? B. n ist ein Vielfaches von 5; C. n ist durch 20 teilbar; D. n ist gerade und durch 5 teilbar; E. n = 100 F. n2 ist durch 100 teilbar.  Aussagen Grundfrage: Wie hängen Aussagen zusammen? Wie findet man gültige Zusammenhänge? Mittels Beweis! Beweis ist eine Kette von wahren Implikationen.  Beweise Jeder Beweisschritt soll o↵ensichtlich sein: Entweder logisch evident, oder schon vorher bewiesen bzw. bekannt.  Beweise Man unterscheidet 2 Arten von Beweisen von A ! B: Direkter Beweis. Unter der Annahme A wird durch logisches Schließen B hergeleitet. Indirekter Beweis (Widerspruchsmethode). Unter Annahme von A und ¬B wird ein Widerspruch (z.B. 0 = 1) hergeleitet.  Beweise Direkter Beweis. Unter der Annahme A wird durch logisches Schließen B hergeleitet. Beispiel: Sei x, y rationale Zahlen. Z.z.: x + y ist auch rational. Beweis. Wir nehmen an, dass die Voraussetzung wahr ist: x, y sind rational. Wenn x rational ist, dann x = mp , wo m, p ganze Zahlen sind. Wenn y rational ist, dann y = qn , wo n, q ganze Zahlen sind. Dann x + y = mq+np pq. Deshalb ist x + y auch rational. Die Behauptung ist also wahr. Die ganze Implikation ist also wahr.  Beweise Indirekter Beweis. Unter Annahme von A und ¬B wird ein Widerspruch (z.B. 0 = 1) hergeleitet. Beruht auf Wahrheit von ((A ^ ¬B) ! 0 = 1) ! (A ! B) (Mittels Wahrheitstabelle nachrechnen!) Beispiel: Wir wollen beweisen, dass die Summe von drei aufeinanderfolgenden natürlichen Zahlen immer durch 3 teilbar ist. A=”n ist eine natürliche Zahl”. B= ”n + (n + 1) + (n + 2) ist durch 3 teilbar”. Wir nehmen an, dass A ^ ¬B wahr ist: n ist eine natürliche Zahl und n + (n + 1) + (n + 2) ist durch 3 nicht teilbar. n + (n + 1) + (n + 2) = 3n + 3 = 3(n + 1). ich Dann ist n + 1 keine natürliche Zahl. -wenn e Also, 3(n + 1) ist durch 3 nicht teilbar. Dann ist auch n keine natürliche Zahl. Widerspruch!  Aussagenlogik - Formale Logik Zur Erinnerung: In der formalen Logik müssen wir alle Bestandteile eines logischen Systems genau definieren. Auf den folgenden Folien: Formale Syntax: Wir definieren, was genau eine Aussagenlogische Formel ist. Formale Semantik: Wir geben Aussagenlogischen Formeln eine Bedeutung. Später: Kalkül & Schlussregeln  Subsection 1 Die Syntax der Aussagenlogik  Induktive Definition A... Menge von Atomen /Grundelementen Funktionen f (x, y ), g (x1 ,... , xn ),... Induktive Definition einer Menge / Sprache L L ist die kleinste Menge für die folgendes gilt: A✓L Wenn x, y 2 L dann ist auch f (x, y ) 2 L Wenn x1 ,... , xn 2 L dann ist auch g (x1 ,... , xn ) 2 L Beispiel Die Menge G der geraden Zahlen ist induktiv wie folgt definiert. 02G Wenn x 2 G dann ist auch x + 2 2 G Wichtig: G ist die kleinste Menge, die beide Bedingungen erfüllt.  Aussagenlogische Formeln - Syntax Nun wollen wir formal definieren, was wir unter Aussagenlogischen Formeln (auch Boolesche Ausdrücke, nach George Boole) verstehen. Definition (Aussagenlogische Formel) Wir betrachten eine Menge von atomaren Formeln (Variablen) Var. Die aussagenlogischen Formeln sind jetzt induktiv definiert. Jede atomare Formel aus Var ist eine Formel Sind F und G Formeln dann sind auch ¬F , (F ^ G ), (F _ G ), und (F ! G ) Formeln. FVar bezeichnet die Menge der aussagenlogischen Formeln, die aus den Atomen Var gebildet werden können.  Aussagenlogische Formeln - Syntax Beispiel Für die atomaren Formeln Var = {x, y , z} können wir z.B. die folgende Formel bilden: ((x ! y ) ^ (z _ ¬x)) Zunächst können wir Formeln F1 = x und F2 = y bilden und dann F3 = (F1 ! F2 ) = (x ! y ) Mit F4 = z und F5 = ¬F1 = ¬x bilden wir dann F6 = (F4 _ F5 ) = (z _ ¬x) Schlussendlich erhalten wir (F3 ^ F6 ) = ((x ! y ) ^ (z _ ¬x))  Subsection 2 Die Semantik der Aussagenlogik  Semantik der Aussagenlogik Die Semantik der Aussagenlogik wird über Wahrheitswerte “wahr” (1) und “falsch” (0) definiert. Die Aussagenlogik ist damit eine zweiwertige Logik 1. Ein x 2 Var steht für irgendeine Aussage. Der Wahrheitswert von x hängt also davon ab für welche konkrete Aussage x steht. Der Wahrheitswert einer Formel wird in Abhängigkeit von den Wahrheitswerten der atomaren Formeln berechnet. Jeder Formel wird dann entweder der Wert 1 oder 0 zugeordnet. Definition Eine Belegung ist eine Funktion ↵ : Var ! {1, 0} die jeder atomaren Formel entweder den Wert 1 oder 0 zuweist. Diese Wahrheitswerte setzten sich auf beliebige Formeln fort. 1 Außerhalbdieser Vorlesung gibt es sogenannte mehrwertige Logiken, die mehr als zwei Wahrheitswerte betrachten.  Semantik der Aussagenlogik einFalsch sind Ausse Definition eine b Sei ↵ eine Belegung für Atome in Var. Wir definieren die Erweiterung ↵ der Belegung ↵ auf alle Formeln in FVar wie folgt: für atomare Formeln F 2 Var : ↵ b(F ) = ↵(F ) für Formeln F(, G 2 FVar : 1 Wenn ↵ b(F ) = 1 und ↵ b(G ) = 1 b(F ^ G ) = ↵ 0 sonst ( 1 Wenn ↵ b(F ) = 1 oder ↵ b(G ) = 1 b(F _ G ) = ↵ 0 sonst ( 1 Wenn ↵ b(F ) = 0 b(¬F ) = ↵ 0 sonst für Formeln F , G 2 FVar : ↵ b(F ! G ) = ↵ b(¬F _ G )  Negation Beispiel Die Vorlesung ist nicht im AudiMax. Die Aussage ist falsch wenn die Vorlesung im AudiMax ist und wahr andernfalls. Negation Der Wahrheitswert von ¬F ergibt sich aus dem Wahrheitswert von F entsprechend der folgenden Wahrheitstafel: ˆ (F ) ↵ ˆ (¬F ) ↵ 0 1 1 0 Andere Bezeichnungen/Symbole: not, non, F , ⇠ F , F̄ , NF ,...  Konjunktion Beispiel Ich sehe mir einen Film an und esse Popcorn. Ist nur wahr wenn beide Aussagen wahr sind. Konjunktion ˆ (F ) ↵ ˆ (G ) ↵ ˆ (F ^ G ) ↵ 0 0 0 0 1 0 1 0 0 1 1 1 Andere Bezeichnungen/Symbole: and, et, F · G , FG , F &G , KFG ,...  Disjunktion Beispiel Ich sehe mir einen Film an oder esse Burger. Ist wahr wenn mind. eine der beiden Aussagen wahr ist. Disjunktion ˆ (F ) ↵ ˆ (G ) ↵ ˆ (F _ G ) ↵ 0 0 0 0 1 1 1 0 1 1 1 1 Andere Bezeichnungen/Symbole: or, vel, F + G , F |G , AFG ,...  Implikation Beispiel Wenn Fritz Fußball spielt, dann spielt auch Barbara Fußball. Ist nur falsch wenn Fritz spielt aber Barbara nicht spielt Implikation ˆ (F ) ↵ ˆ (G ) ↵ ˆ (F ! G ) ↵ 0 0 1 0 1 1 1 0 0 1 1 1 Andere Bezeichnungen/Symbole: implies, only if, F G , F ) G , CFG ,...  Semantik der Aussagenlogik - Zusammenfassung Für Formeln F , G 2 FVar : b(F ) ↵ b(G ) ↵ b(F ^ G ) ↵ b(F ) ↵ b(G ) ↵ b(F _ G ) ↵ 0 0 0 0 0 0 0 1 0 0 1 1 1 0 0 1 0 1 1 1 1 1 1 1 b(F ) ↵ b(G ) ↵ b(F ! G ) ↵ b(F ) ↵ b(¬F ) ↵ 0 0 1 0 1 0 1 1 1 0 1 0 0 1 1 1 Da alle Formeln nur aus solchen Verknüpfungen aufgebaut sind, ist damit b für alle Formeln definiert. ↵  Semantik der Aussagenlogik - Äquivalenz Operator Wir können jetzt weitere zusätzliche Operator definieren. Beispiel Fritz spielt Fußball genau dann wenn Barbara auch Fußball spielt. Ist wahr wenn beiden spielen oder keiner der beiden spielt. Äquivalenz (F $ G ) b(F ) ↵ b(G ) ↵ b(F $ G ) ↵ 0 0 1 0 1 0 1 0 0 1 1 1 F $ G ist also eine Kurzschreibweise von (F ! G ) ^ (G ! F ). Andere Bezeichnungen/Symbole: i↵, eq, F ⌘ G , F , G , EFG ,...  Ausschließende Disjunktion (XOR) Beispiel Ich sehe mir entweder einen Film an oder spiele Fußball (aber nicht beides). Ist wahr wenn genau eine der beiden Aussagen wahr ist. Ausschließende Disjunktion Wir notieren die Ausschließende Disjunktion von zwei Aussagen F , G als F G. b(F ) ↵ b(G ) ↵ b(F ↵ G) 0 0 0 0 1 1 1 0 1 1 1 0 Andere Bezeichnungen/Symbole: Antivalenz, xor, F 6⌘ G , F 6, G , F 6$ G , JFG ,...  Implikation (Umkehrung) Beispiel Fritz spielt Fußball, wenn Barbara Fußball spielt. Ist nur falsch wenn Fritz nicht spielt aber Barbara spielt Implikation Wir notieren die Implikation von zwei Aussagen F , G als F G. b(F ) ↵ b(G ) ↵ b(F ↵ G) 0 0 1 0 1 0 1 0 1 1 1 1 Andere Bezeichnungen/Symbole: if, F ⇢ G , F ( G ,...  NAND & NOR Beispiel Es ist nicht der Fall, dass das Kuvert signiert und zugeklebt ist. Weder Fritz noch Barbara spielen Tischtennis. Negierte Konjunktion & Negierte Disjunktion Negierte Konjunktion: F nand G Negierte Disjunktion: F nor G b(F ) ↵ b(G ) ↵ b(F ^ G ) ↵ b(F nand G ) ↵ b(F _ G ) ↵ b(F nor G ) ↵ 0 0 0 1 0 1 0 1 0 1 1 0 1 0 0 1 1 0 1 1 1 0 1 0 Andere Bezeichnungen/Symbole: NAND: She↵er-Strich, F " G , F |G , F /G , DFG ,... NOR: Peirce-Pfeil, F # G , XFG ,...  Logische Operatoren – Zusammenfassung Logische / Boolesche Operatoren Binäre Operatoren x nand y x nor y Unäre Op. x $y x !y y x 6! y y x y x ^y x _y Konstanten x6 x y x x ¬x > ? 0 0 0 1 0 1 1 0 1 1 0 0 0 1 1 0 0 1 0 1 1 0 0 1 1 0 0 1 1 0 1 0 0 1 1 0 0 1 0 1 1 0 1 1 1 0 1 0 1 0 1 1 0 0 n Es gibt 22 verschiedene n-stellige Boolesche Operatoren. Es gibt 2n Möglichkeiten für die Argumente Jeweils 2 Möglichkeiten (0,1) für das Ergebnis  Funktionale Vollständigkeit Definition (Funktionale Vollständigkeit) Wie nennen eine Teilmenge der Booleschen Funktionen funktional vollständig, wenn damit alle Booleschen Funktionen ausgedrückt werden können. Satz Die Menge {¬, ^, _} ist funktional vollständig. z.B.: x ! y = ¬x _ y Satz Die Menge {¬, ^} ist funktional vollständig.  Funktionale Vollständigkeit Satz Die Menge {¬, ^} ist funktional vollständig. Beweis: Wir wissen, dass die Menge {¬, ^, _} vollständig ist Es genügt also zu zeigen, dass _ mit Hilfe von ¬ und ^ ausgedrückt werden kann x _ y = ¬(¬x ^ ¬y ) – das können wir mit einer Wahrheitstafel überprüfen x y ¬x ¬y ¬x ^ ¬y ¬(¬x ^ ¬y ) 0 0 1 1 1 0 0 1 1 0 0 1 1 0 0 1 0 1 1 1 0 0 0 1  Semantik der Aussagenlogik - Modelle Definition Eine Belegung ↵ für Var ist ein Modell einer Formel F über Var , wenn b(F ) = 1, wir schreiben auch ↵ |= F. ↵ Die Semantik einer Formel ergibt sich aus der Menge ihrer Modelle. Definition Eine Belegung ↵ für Var ist ein Modell einer Menge F von Formeln wenn ↵b(G ) = 1 für jede Formel G 2 F, wir schreiben auch ↵ |= F.  Subsection 3 Aussagenlogik: Grundbegri↵e Definition Eine Formel F ist erfüllbar wenn F mind. ein Modell hat (sonst unerfüllbar). Definition Eine Menge F von Formeln ist konsistent (widerspruchsfrei) wenn es ein Modell für F gibt. inkonsistent(widersprüchlich) wenn es kein Modell für F gibt. Beispiel Belegung ↵ mit ↵(a) = 1, ↵(b) = 1, ↵(c) = 0 ↵ ist ein Modell von (a _ c) ^ (b _ c) Die Formel (a _ c) ^ (b _ c) ist daher erfüllbar Die Formelmenge {(a _ c), (b _ c)} ist konsistent Definition Eine Formel F ist allgemein gültig / eine Tautologie wenn jede Belegung auch ein Modell ist. Beispiele für Tautologien: (x _ ¬x) ((a _ c) _ ¬c) (c ! c) (((a ! b) ^ (b ! c)) ! (a ! c)) Definition Zwei Formeln F und G sind semantisch äquivalent wenn ↵ b(F ) = ↵ b(G ) & semantisch für alle Belegungen ↵. Wir schreiben F ⌘ G. äquivalent also , Beispiele für semantisch äquivalente Formeln: F & G haben diesewer eine (x ^ y ) und (y ^ x) (x ^ y ) ⌘ (y ^ x) (¬x _ y ) und (x ! y ) (¬x _ y ) ⌘ (x ! y ) ((a _ b) ^ (c _ ¬c)) und (a _ b) ((a _ b) ^ (c _ ¬c)) ⌘ (a _ b) Definition Eine Formel G folgt aus der Formel F / der Formelmenge F wenn jedes Modell von F / F auch Modell von G ist. Wir schreiben F |= G bzw. F |= G. Beispiele: Aus a folgt (a _ b). a |= (a _ b) Aus (¬a ^ b) folgt (a _ b). (¬a ^ b) |= (a _ b) Aus {a, b} folgt (a ^ b). {a, b} |= (a ^ b) Aus {a, a ! b} folgt b. {a, a ! b} |= b Aus {¬b, a ! b} folgt ¬a. {¬b, a ! b} |= ¬a G ist eine Tautologie () ; |= G. In diesem Fall schreiben wir |= G.  Grundlegende Begri↵e - Zusammenfassung ↵: Belegung für Var , F ,G : Formeln über Var F: Eine Menge von Formeln über Var Definition F ist konsistent (widerspruchsfrei) wenn es ein Modell für F gibt. F ist inkonsistent(widersprüchlich) wenn es kein Modell für F gibt. F ist erfüllbar wenn F mind. ein Modell hat (sonst unerfüllbar). F ist allgemein gültig / eine Tautologie wenn jede Belegung auch ein Modell ist. F ist semantisch äquivalent zu G wenn ↵ b(F ) = ↵ b(G ) für alle Belegungen ↵. Wir schreiben F ⌘ G. G folgt aus F /F wenn jedes Modell von F /F auch Modell von G ist. Wir schreiben F |= G bzw. F |= G.  Formalisieren in Aussagenlogik Unser ursprüngliches Ziel ist es (natürlich sprachliche) Aussagen zu formalisieren und logische Zusammenhänge zu identifizieren. Faustregel zur Formalisierung von Deutsch: Identifizieren von atomaren Aussagen: die kürzeste Aussage, in der keine logische Verknüpfung vorkommt (nicht, und, oder, wenn... dann usw.), und die entweder wahr oder falsch sein kann Dann ersetzt man atomare Aussagen mit Aussagenvariablen Wörter/Phrasen nicht, und, oder, wenn... dann, usw. werden durch die entsprechenden logischen Operationen ersetzt.  Formalisieren in Aussagenlogik - Beispiel 1 Aussage 1: Der Verkauf von Häusern sinkt, wenn die Zinsen steigen. Aussage 2: Auktionäre sind nicht glücklich, wenn der Verkauf von Häusern sinkt. Aussage 3: Die Zinsen steigen. Aussage 4: Auktionäre sind glücklich. Atomare Aussagen: S: der Verkauf von Häusern sinkt R: die Zinsen steigen H: Auktionäre sind glücklich Aussage 1: R !S agen Aussage 2: S ! ¬H u musssein? wen Aussage 3: R alseitig Aussage 4: H können Wir wollen wissen, ob die Aussagen miteinander konsistent sind. Deshalb betrachten wir deren Konjunktion (R ! S) ^ (S ! ¬H) ^ R ^ H.  Formalisieren in Aussagenlogik - Beispiel 1 Da wir wissen wollen ob die Aussagen miteinander konsistent sind betrachten wir deren Konjunktion (R ! S) ^ (S ! ¬H) ^ R ^ H. Wir testen ob die Formel erfüllbar ist und nutzen dazu Wahrheitstafeln. S R H (R ! S) (S ! ¬H) (R ! S) ^ (S ! ¬H) ^ R ^ H 0 0 0 1 1 0 0 0 1 1 1 0 0 1 0 0 1 0 0 1 1 0 1 0 1 0 0 1 1 0 1 0 1 1 0 0 1 1 0 1 1 0 1 1 1 1 0 0 Die Formel hat kein Model (ist unerfüllbar) und daher sind die Aussagen widersprüchlich.  Formalisieren in Aussagenlogik - Beispiel 2 Aussage 1: Wenn der Geiger das Konzert gibt, werden viele kommen, daistkeine amanAusseine , wenn die Preise nicht zu hoch sind. > - Aussage 2: Wenn der Geiger das Konzert gibt, werden die Preise nicht zu hoch sein. Schluss: Daher werden, falls der Geiger das Konzert bestreitet, viele kommen. Wir wollen wissen ob der Schluss korrekt ist. Atomare Aussagen: P: der Geiger gibt das Konzert“ ” C: viele werden kommen“ ” H: die Preise sind zu hoch“ ” Aussage 1: P ! (¬H ! C ) Aussage 2: P ! ¬H Schluss: P ! C Wir wollen wissen ob P ! C aus P ! (¬H ! C ) und P ! ¬H folgt.  Indirekter Beweis/Widerspruchsmethode Um {A, B} |= C zu zeigen, können wir zeigen, dass F = (A ^ B) ! C eine Tautologie ist. Die Formel F ist äquivalent zu F 0 = ¬A _ ¬B _ C. Um zu testen ob F 0 eine Tautologie ist können wir testen ob ¬F 0 unerfüllbar ist. ¬F 0 ⌘ A ^ B ^ ¬C. Wir erhalten also dass {A, B} |= C genau dann gilt wenn A ^ B ^ ¬C unerfüllbar ist.  Formalisieren in Aussagenlogik - Beispiel 2 Zurück zum Beispiel 2: Wir wollen wissen ob P ! C aus P ! (¬H ! C ) und P ! ¬H folgt. (Wir schreiben auch {P ! (¬H ! C ), P ! ¬H} |= P ! C.) Widerspruchsmethode: Um {A, B} |= C zu zeigen, zeigen wir dass A ^ B ^ ¬C unerfüllbar (widersprüchlich) ist. Wir betrachten also die Formel: (P ! (¬H ! C )) ^ (P ! ¬H) ^ ¬(P ! C ) Mittels Wahrheitstafel (oder dem später diskutierten Resolutionskalkül) stellen wir fest dass die Formel unerfüllbar ist. Daher ist der ursprüngliche Schluss auf P ! C korrekt.  Formalisieren in Aussagenlogik - Beispiel 3 (zum Selbststudium) Aussage 1: Tom kann am Wochenende nicht beides eine Wanderung und eine Radtour machen. Aussage 2: Wenn es am Wochenende regnet macht Tom eine Radtour. Aussage 3: Tom geht am Wochenende Wandern. Aussage 4 Es regnet nicht am Wochenende. Aufgabe (Teil 1): Formalisieren Sie die Aussagen mittels aussagenlogischer Formeln. Geben Sie die Bedeutung jeder Aussagenvariablen an. Atomare Aussagen: R: Es regnet am WE“ T: Tom macht eine Radtour am WE“ ” ” W: Tom macht eine Wanderung am WE“ ” Aussage 1: ¬(T ^ W ) oder (¬T _ ¬W ) Aussage 2: R !T Aussage 3: W Aussage 4: ¬R  Formalisieren in Aussagenlogik - Beispiel 3 (zum Selbststudium) Aufgabe (Teil 2): Kann man aus den ersten drei Aussagen auf Aussage 4 schließen? Beweisen Sie Ihre Vermutung mit einer geeigneten Methode aus der Vorlesung (geben Sie auch an welche Methode Sie verwenden). Wir verwenden die Widerspruchsmethode und betrachten die Konjunktion der drei Aussagen und des negierten Schluss: (¬T _ ¬W ) ^ (R ! T ) ^ W ^ R Ddiese Formel ist unerfüllbar (Wahrheitstafel). Daher ist der Schluss aus den drei Aussagen korrekt.  Fundamentale Sätze Satz Ein Formel F ist genau dann eine Tautologie wenn ¬F unerfüllbar ist. Beispiel: Tautologie: (c _ ¬c) unerfüllbar: ¬(c _ ¬c) ⌘ (¬c ^ c) Satz Zwei Formeln F , G sind semantisch äquivalent genau dann wenn F aus G folgt und G aus F folgt. F ⌘ G , G |= F und F |= G Satz Zwei Formeln F , G sind semantisch äquivalent genau dann wenn F $ G eine Tautologie ist F ⌘ G , |= F $ G Es gilt auch: F |= G , |= F ! G {F , G } |= H , F |= G ! H {F , G } |= H , |= (F ^ G ) ! H Satz (Kompaktheitssatz) Eine (unendliche) Menge von aussagenlogischen Formeln ist genau dann erfüllbar, wenn jede endliche Teilmenge erfüllbar ist.  Ersetzungssatz Beobachtung: Jede Teilformel kann durch eine semantisch äquivalente Formel ersetzt werden. Satz (Ersetzungssatz) Betrachtet man eine Formel G mit einer Teilformel F1 und bildet eine neue Formel G [F1 /F2 ] indem man (in G ) die Teilformel F1 durch eine semantisch äquivalente Formel F2 ersetzt, dann gilt G ⌘ G [F1 /F2 ]. Beispiel: G = ((¬a _ b) _ c) F1 = (¬a _ b) ist semantisch äquivalent zu F2 = (a ! b) G [F1 /F2 ] = ((a ! b) _ c) Ersetzungssatz: (¬a _ b _ c) ⌘ ((a ! b) _ c)  Äquivalenzen der Aussagenlogik Mit dem Ersetzungssatz kann man äquivalente Formeln verwenden um eine Formel zu vereinfachen. Einige hilfreiche Äquivalenzen: Idempotenz (F ^ F ) ⌘ F (F _ F ) ⌘ F Kommutativität (F ^ G ) ⌘ (G ^ F ) (F _ G ) ⌘ (G _ F ) Assoziativität ((F ^ G ) ^ H) ⌘ (F ^ (G ^ H)) ((F _ G ) _ H) ⌘ (F _ (G _ H)) Absorption (F ^ (F _ G )) ⌘ F (F _ (F ^ G )) ⌘ F Distributivität (F ^ (G _ H)) ⌘ ((F ^ G ) _ (F ^ H)) (F _ (G ^ H)) ⌘ ((F _ G ) ^ (F _ H)) Doppelnegation ¬¬F ⌘ F de Morgansche Regeln ¬(F ^ G ) ⌘ (¬F _ ¬G ) ¬(F _ G ) ⌘ (¬F ^ ¬G )  Zusammenfassung & Ausblick Bis jetzt haben wir Folgendes behandelt: Formale Definition von Syntax und Semantik der Aussagenlogik Fundamentale Begri↵e & Sätze Formalisieren in Aussagenlogik Weiter geht es mit: Kalkül der Aussagenlogik Schlussregeln Resolution Hornlogik, Einheitsresolution Prädikatenlogik: Syntax Semantik  Subsection 7 Schlussregeln der Aussagenlogik  Der Resolutionskalkül der Aussagenlogik Resolution ist ein Verfahren der formalen Logik, um zu Testen ob eine Formel / eine Menge von Formeln widersprüchlich/unerfüllbar ist. Diese Herleitung geschieht mittels eines Algorithmus ,! Maschinengestütztes Beweisen. Der Resolutionskalkül arbeitet auf Formeln in KNF (Konjunktiver Normalform). ,! Der erste Schritt ist die gegebenen Formeln in KNF zu bringen.  Äquivalenzen der Aussagenlogik Mit dem Ersetzungssatz kann man äquivalente Formeln verwenden um eine Formel zu vereinfachen. Einige hilfreiche Äquivalenzen: Idempotenz (F ^ F ) ⌘ F und (F _ F ) ⌘ F Kommutativität (F ^ G ) ⌘ (G ^ F ) und (F _ G ) ⌘ (G _ F ) Assoziativität ((F ^ G ) ^ H) ⌘ (F ^ (G ^ H)) und ((F _ G ) _ H) ⌘ (F _ (G _ H)) Absorption (F ^ (F _ G )) ⌘ F und (F _ (F ^ G )) ⌘ F Distributivität (F ^ (G _ H)) ⌘ ((F ^ G ) _ (F ^ H)) (F _ (G ^ H)) ⌘ ((F _ G ) ^ (F _ H)) Doppelnegation ¬¬F ⌘ F de Morgansche Regeln ¬(F ^ G ) ⌘ (¬F _ ¬G ) ¬(F _ G ) ⌘ (¬F ^ ¬G )  Äquivalenzen der Aussagenlogik Dank dieser Äquivalenzen können wir Formeln kompakter notieren: Klammerung zwischen aufeinander folgender ^ oder _ ist nicht notwendig: ,! Statt ((F ^ G ) ^ H) können wir (F ^ G ^ H) schreiben. Weiters werden wir Klammern um die ganze Formel nicht notieren: ,! Statt (F ^ G ) können wir F ^ G schreiben. Diese Äquivalenzen sind die Basis für Normalformen. Normalform Eine Normalform ist eine Einschränkung auf der Syntax sodass jede beliebige Formel in eine semantisch äquivalente Formel in Normalform umgewandelt werden kann. Vereinfacht die maschinelle Verarbeitung von logischen Formeln. (Viele Algorithmen verarbeiten nur eine bestimmte Normalform)  Konjunktive Normalform Literal: Unter Literalen verstehen wir Atome x 2 Var und negierte Atome ¬x für x 2 Var. Definition Eine Formel ist in konjunktiver Normalform (KNF), wenn sie eine Konjunktion von Disjunktionen von Literalen ist. F ist also von folgender Form (Li,j Literale): F = (L1,1 _ · · · _ L1,m1 ) ^ · · · ^ (Ln,1 _ · · · _ Ln,mn ) Beispiele: (¬a _ b) ^ (a _ ¬c _ d) ^ ¬b (¬a _ x _ ¬c _ d) ^ (¬b _ ¬y )  Disjunktive Normalform Definition Eine Formel ist in disjunktiver Normalform (DNF), wenn sie eine Disjunktion von Konjunktionen von Literalen ist. F ist also von folgender Form (Li,j Literale): F = (L1,1 ^ · · · ^ L1,m1 ) _ · · · _ (Ln,1 ^ · · · ^ Ln,mn ) Beispiele: (¬a _ b) ^ (a _ ¬c _ d) ^ ¬b (KNF) (¬a ^ b ^ c) _ (a ^ ¬c ^ d) (DNF) ¬a ^ b ^ c (DNF, KNF) ¬a _ b _ c (DNF, KNF) (¬a _ b _ c) ^ (a _ (b ^ d)) () Jede Formel kann mit Hilfe der präsentierten Äquivalenzumformungen in eine semantisch äquivalente KNF (DNF) transformiert werden.  Konjunktive und Disjunktive Normalform - Beispiele Zwei Beispiele wie man eine Formel in KNF umwandeln kann: (A ^ B) ! C ¬(A ^ B) _ C (Definition von !) (¬A _ ¬B) _ C (de Morgan) ¬A _ ¬B _ C (Assoziativität) C $ (A ^ B) (¬C _ (A ^ B)) ^ (C _ ¬(A ^ B)) (Definition von $) (¬C _ (A ^ B)) ^ (C _ (¬A _ ¬B)) (de Morgan) (¬C _ (A ^ B)) ^ (C _ ¬A _ ¬B) (Assoziativität) ((¬C _ A) ^ (¬C _ B)) ^ (C _ ¬A _ ¬B) (Distributivität) (¬C _ A) ^ (¬C _ B) ^ (C _ ¬A _ ¬B) (Assoziativität)  Konjunktive und Disjunktive Normalform - Algorithmus Diese Schritte lassen sich auch in einen Algorithmus fassen der eine Formel F in eine semantisch äquivalente KNF umzuwandeln. Algorithmus 1 Ersetze G $ H durch (G ! H) ^ (H ! G ) 2 Ersetze G ! H durch (¬G _ H) 3 Iteriere das Folgende solange wie möglich 1 Ersetze ¬¬G durch G 2 Ersetze ¬(G ^ H) durch (¬G _ ¬H) 3 Ersetze ¬(G _ H) durch (¬G ^ ¬H) 4 Iteriere das Folgende solange wie möglich 1 Ersetze (G _ (H ^ I )) und ((H ^ I ) _ G ) durch ((G _ H) ^ (G _ I )) Ersetze“ liest sich als Ersetze alle Teilformeln der Form“ ” ”  Der Resolutionskalkül der Aussagenlogik Der Resolutionskalkül erlaubt die Unerfüllbarkeit einer aussagenlogischen Formel zu beweisen. Viele andere Aufgaben können hierauf zurückgeführt werden: Testen ob eine endliche Menge von Formeln F widersprüchlich ist, dafür testet man die Konjunktion der Formeln auf Unerfüllbarkeit. Testen ob eine Formel F aus einer Formelmenge F folgt. Man testet F [ {¬F } auf Widersprüchlichkeit. Testen ob eine Formel F eine Tautologie ist. Man testet ¬F auf Unerfüllbarkeit.  Klauseln von Formeln Gegeben sei eine Formel F in KNF, also F = (L1,1 _ · · · _ L1,m1 ) ^ · · · ^ (Ln,1 _ · · · _ Ln,mn ) wobei die Li,j Literale sind. Konjunktion und Disjunktion sind idempotent, kommutativ und assoziativ. Daher können wir eine Formel in KNF auch als Menge von Mengen anschreiben. Die F zugeordnete Klauselmenge K (F ) ist K (F ) = {{L1,1 ,... , L1,m1 },... , {Ln,1 ,... , Ln,mN }} Eine einzelne Menge {Li,1 ,... , Li,mi } heißt Klausel von F. Eine Klausel entspricht einer Disjunktion von Literalen  Klauseln von Formeln Verschiedene Formeln können dieselbe Klauselmenge besitzen Beispiel Die Formeln F1 = (A _ B) ^ C , F2 = (C _ C ) ^ (A _ B) ^ C und F3 = C ^ (B _ A) besitzen alle die Klauselmenge {{A, B}, {C }}. Eine leere Klausel entspricht dem Wahrheitswert 0 (falsch). (Eine leere Disjunktion ist falsch) Eine Klauselmenge die eine leere Klausel enthält hat den Wahrheitswert 0. (Eine Konjunktion ist falsch wenn ein Eintrag falsch ist) Eine leere Klauselmenge entspricht dem Wahrheitswert 1. (Eine leere Konjunktion ist wahr)  Resolvente von Klauseln Idee: Wenn wir Klauseln {A, B} und {¬A, C } haben, dann kann nur entweder A oder ¬A wahr sein. Es folgt, dass B oder C wahr sein muss, d.h. die Klausel {B,C}. Definition Eine Klausel K3 heißt Resolvente der Klauseln K1 , K2 wenn es ein Literal L gibt sodass L 2 K1 , ¬L 2 K2 K3 = (K1 \ {L}) [ (K2 \ {¬L}) Wenn K3 Resolvente von K1 und K2 ist, verwenden wir auch folgende graphische Darstellung. K1 K2 K3  Resolvente von Klauseln - Beispiel Gegeben sei die Klauselmenge {{A, B, ¬C }, {A, ¬B, C }}. Zu den Klauseln dieser Klauselmenge gibt es die folgenden Resolventen: {A, B, ¬C } {A, ¬B, C } {A, B, ¬C } {A, ¬B, C } {A, C , ¬C } {A, B, ¬B} Folgendes ist aber FALSCH: {A, B, ¬C } {A, ¬B, C } {A}  Resolutionslemma Satz (Resolutionslemma) Für jede Formel F mit Klauselmenge K (F ): Ist K3 eine Resolvente zweier Klauseln K1 , K2 2 K (F ) so ist F semantisch äquivalent zu allen Formeln mit Klauselmenge K (F ) [ {K3 }. Wir können also neue Klauseln hinzufügen ohne die Semantik zu verändern. Weiters können wir Klauseln die Tautologien entsprechen (Klauseln die x und ¬x enthalten) weglassen ohne die Semantik zu verändern. Idee des Resolutionskalküls: Solange Resolventen bilden bis man entweder die leere Klausel enthält oder alle möglichen Resolventen gebildet wurden.  Resolutionskalkül Sei K = K (F ) die Klauselmenge einer Formel: Res(K ) = K [ {R | R ist Resolvente zweier Klauseln in K } Res 0 (K ) = K und für n 1 sei Res n (K ) = Res(Res n 1 (K )) [ Res 1 (K ) = Res n (K ) n 0 Satz Eine Formel F ist genau dann unerfüllbar wenn ; 2 Res 1 (K (F )). Hat F nur n Variablen dann hat Res 1 (K ) höchsten 4n Klauseln. ,! Res 1 (K ) kann mit (maximal) 4n Iterationen berechnet werden.  Resolutionskalkül - Erfüllbarkeitstest Gegeben sei eine Formel in KNF: 1 Bilde Klauselmenge K (F ) 2 Berechne Res 1 (K ), Res 2 (K ),... , Res n (K ) bis ; 2 Res n (K ) oder Res n 1 (K ) = Res n (K ). 3 Wenn ; 2 Res n (K ) F unerfüllbar“ ” anderenfalls F erfüllbar“. ”  Formalisieren in Aussagenlogik - Beispiel 2 VO1 Aussage 1: Wenn der Geiger das Konzert gibt, werden viele kommen, wenn die Preise nicht zu hoch sind. Aussage 2: Wenn der Geiger das Konzert gibt, werden die Preise nicht zu hoch sein. Schluss: Daher werden, falls der Geiger das Konzert bestreitet, viele kommen. Wir wollen wissen ob der Schluss korrekt ist. Atomare Aussagen: P: der Geiger gibt das Konzert“ ” C: viele werden kommen“ ” H: die Preise sind zu hoch“ ” Aussage 1: P ! (¬H ! C ) Aussage 2: P ! ¬H Schluss: P ! C Wir wollen wissen ob P ! C aus P ! (¬H ! C ) und P ! ¬H folgt.  Resolutionskalkül - Beispiel Wir betrachten die Formel aus dem Geiger-Beispiel: (P ! (¬H ! C )) ^ (P ! ¬H) ^ ¬(P ! C ) 1.Schritt: Wir bringen die Formel in KNF. (¬P _ (H _ C )) ^ (¬P _ ¬H) ^ ¬(¬P _ C ) Definition von ! (¬P _ H _ C ) ^ (¬P _ ¬H) ^ P ^ ¬C de Morgan, Assoziativität 2.Schritt: Bilden der Klauselmengen K (F ) = {{¬P, H, C }, {¬P, ¬H}, {P}, {¬C }}  Resolutionskalkül - Beispiel 3.Schritt: Resolventen berechnen Res 0 (K ) = {{¬P, H, C }, {¬P, ¬H}, {P}, {¬C }} Res 1 (K ) = Res 0 (K ) [ {{¬P, C }, {H, C }, {¬P, H}, {¬H}} Res 2 (K ) = Res 1 (K ) [ {{C }, {¬P}, {H}} Res 3 (K ) = Res 2 (K ) [ {{}} Da wir die leere Klausel erreicht haben ist die Formel unerfüllbar.  Resolutionskalkül - Beispiel Oft müssen wir nicht alle Resolventen berechnen um einen Widerspruch (die leere Klausel) zu finden: {¬P, H, C } {¬P, ¬H} {P} {¬C } {¬P, C } {C } ; Aber: Um zu zeigen dass eine Formel widerspruchsfrei ist muss man alle Resolventen berechnen!!!  Subsection 9 Einheitsresolution  Einheitsresolution Eine Einheitsklausel ist eine Klausel die nur aus einem (positiven oder negativen) Literal besteht. Beobachtung: Enthält die Klauselmenge eine positive Einheitsklausel {x} so muss x jedenfalls auf 1 gesetzt werden eine negative Einheitsklausel {¬x} so muss x jedenfalls auf 0 gesetzt werden um die Formel zu erfüllen. Einheitsresolution (unit propagation) Formel F in KNF, K = K (F ) Solange die Klauselmenge K eine Einheitsklausel enthält wähle eine Einheitsklausel {L} Entferne alle Klauseln in K die L enthalten Lösche ¬L aus allen Klauseln in K Wenn ; 2 K dann ist die Formel F unerfüllbar.  Einheitsresolution Sei K eine Klauselmenge dann schreiben wir ERes(K ) für die vereinfachte Klauselmenge die der Einheitsresolution-Algorithmus erzeugt. Satz (Erfüllbarkeitsäquivalenz) Eine Klauselmenge K ist genau dann erfüllbar wenn ihre Vereinfachung ERes(K ) durch Einheitsresolution erfüllbar ist. Wenn ; 2 ERes(K ) dann ist die Formel F unerfüllbar.  Einheitsresolution und allgemeine Klauselmengen Gegeben: Klauselmenge K (F ). Ziel: Testen ob die Klauselmenge K (F ) erfüllbar ist. Idee: Kombiniere Resolution mit Einheitsresolution Verfahren: Wandle den Erfüllbarkeitstest mittels Resolution wie folgt ab Zu Beginn starte Einheitsresolution um die Klauselmenge zu verkleinern. Wurde die leere Klausel berechnet, wird ist K (F ) unerfüllbar; sonst starte Resolution auf der verkleinerten Klauselmenge. Wann immer Resolution eine Einheitsklausel hinzufügt, starte Einheitsresolution um die Klauselmenge zu verkleinern bevor mit Resolution fortgesetzt wird.  Einheitsresolution und allgemeine Klauselmengen - Beispiel Beispiel Formel F = a ^ (¬a _ b _ c) ^ (b $ c) ^ (¬a _ ¬b _ ¬c) ^ (a _ b _ c) Klauselmenge K (F ) = {{a}, {¬a, b, c}, {b, ¬c}, {¬b, c}, {¬a, ¬b, ¬c}, {a, b, c}} mit Einheitsklausel {a} Einheits-Resolution mit {a} ergibt: {{b, c}, {b, ¬c}, {¬b, c}, {¬b, ¬c}} Ein Resolution-Schritt ergibt: {{b, c}, {b, ¬c}, {¬b, c}, {¬b, ¬c}, {b}} Einheits-Resolution mit {b} ergibt: {{c}, {¬c}} Einheits-Resolution mit {¬c} ergibt: {{}} Die Formel F ist also unerfüllbar.  Hornlogik Die Hornlogik ist eine Einschränkung der Aussagenlogik, d.h. es sind nur Formeln einer speziellen Form erlaubt. Benannt nach dem Logiker Alfred Horn. Kann mit speziellen Resolutions-Varianten sehr effizient ausgewertet werden. ,! Einheitsresolution, SLD-Resolution Dient als Grundlage der logischen Programmierung (Prolog). Bedeutung in der Komplexitätstheorie.  Hornlogik Definition Eine Klausel heißt Hornklausel wenn sie höchstens ein positives Literal enthält. Eine Formel F in KNF heißt Hornformel wenn K (F ) nur aus Hornklauseln besteht. Beispiel für eine Hornformel: (a _ ¬b _ ¬c) ^ (¬b _ ¬c) ^ c Unterschiedliche Arten von Hornklauseln: Tatsachenklauseln/Fakten: nur ein positives Literal, z.B. c Regeln: ein positives Literal, z.B. (a _ ¬b _ ¬c) ⌘ (b ^ c) ! a Zielklausel: nur negative Literale, z.B. (¬b _ ¬c)  Einheitsresolution Sei K eine Klauselmenge dann schreiben wir ERes(K ) für die vereinfachte Klauselmenge die der Einheitsresolution-Algorithmus erzeugt. Satz (Erfüllbarkeitsäquivalenz) Eine Klauselmenge K ist genau dann erfüllbar wenn ihre Vereinfachung ERes(K ) durch Einheitsresolution erfüllbar ist. Wenn ; 2 ERes(K ) dann ist die Formel F unerfüllbar. Wenn K eine Horn-Formeln ist gilt auch: Wenn ; 2 / ERes(K ) dann ist die Formel erfüllbar. Satz Eine Horn-Formel ist genau dann erfüllbar wenn in ; 2 / ERes(K ).  Hornlogik/Einheitsresolution - Beispiel 1 Beispiel Formel F = a ^ b ^ ((a ^ b) ! c) ^ (d ! e) Klauselmenge K (F ) = {{a}, {b}, {¬a, ¬b, c}, {¬d, e}} mit zwei Einheitsklausel {a}, {b} {{a}, {b}, {¬a, ¬b, c}, {¬d, e}} Resolviere {a} {{b}, {¬b, c}, {¬d, e}} Resolviere {b} {{c}, {¬d, e}} Resolviere {c} {{¬d, e}} Die Formel F ist erfüllbar.  Hornlogik/Einheitsresolution - Beispiel 2 Beispiel Formel F = a ^ b ^ ((a ^ b) ! c) ^ (¬a _ ¬b) ^ (d ! e) Klauselmenge K (F ) = {{a}, {b}, {¬a, ¬b, c}, {¬a, ¬b}, {¬d, e}} Zwei Einheitsklausel {a}, {b} {{a}, {b}, {¬a, ¬b, c}, {¬a, ¬b}, {¬d, e}} Resolviere {a} {{b}, {¬b, c}, {¬b}, {¬d, e}} Resolviere {b} {{c}, {}, {¬d, e}} Da wir die leere Klausel erhalten haben ist die Formel F unerfüllbar.  Hornlogik/Einheitsresolution - Beispiel 3 (zum Selbststudium) Betrachte die Formel F = (¬T _ ¬W ) ^ (R ! T ) ^ W ^ R Durch Auflösen der Inklusion (R ! T ) zu (¬R _ T ) erhalten wir K (F ) = {{¬T , ¬W }, {¬R, T }, {W }, {R}} {{¬T , ¬W }, {¬R, T }, {W }, {R}} Resolviere {W } {{¬T }, {¬R, T }, {R} Resolviere {¬T } {{¬R}, {R}} Resolviere {¬R} {{}} Da wir die leere Klausel erhalten haben ist die Formel F unerfüllbar.  Subsection 11 Limitierungen von Aussagenlogik  Limitierungen von Aussagenlogik Es gibt logische Zusammenhänge die sich mit Aussagenlogik nicht abbilden lassen. Beispiel Aussage 1: Fritz fährt Ski Aussage 2: Uli fährt Ski Obwohl beide Aussagen augenscheinlich von gleicher Natur sind, kann Aussagenlogik die gemeinsame Struktur nicht modellieren. Beispiel Aussage 1: Jeder Mensch ist wertvoll. Aussage 2: Hans ist ein Mensch. Wir würden also gerne schließen Hans ist wertvoll“. Das ist aber in ” Aussagenlogik nicht möglich.  Limitierungen von Aussagenlogik Limitierungen von Aussagenlogik Aussagen werden als Atome genutzt und nicht weiter analysiert ,! oft stecken mehrere Informationen in einer atomaren Aussage Die innere Struktur einer Aussage geht verloren. Es ist unmöglich/schwer auszudrücken, dass gewisse Beziehungen zwischen Objekten gelten; etwas für alle Objekte gilt; oder es ein Objekt mit einer Eigenschaft geben muss. Wir benötigen also eine ausdrucksstärkere Logik. Prädikatenlogik  Zusammenfassung & Ausblick Bisher Worum geht es in der Logik Aussagenlogik: Formale Definition von Syntax und Semantik der Aussagenlogik Fundamentale Sätze Formalisieren und Schließen in der Aussagenlogik Schlussregeln Resolutionskalkül der Aussagenlogik Hornlogik und Einheitsresolution Nächste Einheit: Ausblick Prädikatenlogik Einführung Prädikatenlogik Formale Syntax der Prädikatenlogik Formale Semantik der Prädikatenlogik Formalisieren in Prädikatenlogik