2005-10-26 Exkurs 1: Lineare Logik ======================= Die Regeln WEAK und CONTR wurden im Vollständigkeitsbeweis nicht verwendet, sind daher redundant. Das liegt daran, dass WEAK und CONTR schon in die anderen Regeln eingearbeitet sind. Ersetzen wir Ax durch ------- Ax' A ==> A dann brauchen wir WEAK um z.B. das Sequent A,B ==> A,C zu zeigen. Ersetzen wir AND-R duch G1 ==> D1, phi G2 ==> D2, psi ---------------------------------- AND-R' G1, G2 ==> D1, D2, phi AND psi dann brauchen wir CONTR um das Sequent A,B,C ==> (A AND C) AND (B AND C). Weiteres Beispiel: A AND B ==> A AND A braucht CONTR und WEAK. Die Logik mit AND-R' statt AND-R (und analog für die anderen Split Regeln) und Ax' statt Ax und ohne WEAK and CONTR, heißt lineare Logik (erfunden von Girard). Lineare Logik ist echt schwächer als propositionale Logik. Warum heisst diese Logik lineare Logik? Man kann die Konnektive in linearer Algebra interpretieren z.B. AND durch TENSOR (*). Lineare Abbildungen sind z.B. A * B -> B * A (A -> B) * A -> B Nicht linear ist z.B. A -> A * A da für lineare Abb. f lamdba f(x) = f (lambda x) gelten muss (für jedes Skalar lambda). Exkurs 2: Schnittregel ====================== Schnittregel (Verwendung von Lemmas) G ==> A G, A ==> D -------------------- CUT G ==> D CUT ist sicherlich korrekt, aber mit Hinblick auf Vollständigkeit nicht wirklich notwendig. Schnitte können aus einem Beweis enfernt werden. Syntaktische Schnittelimination: Aus einem Beweisbaum mit (CUT) kann auch syntaktisch ein Beweis ohne CUT konstruiert werden. Dazu verallgemeinert man CUT zu G1 ==> D1, A G2, A ==> D2 --------------------------- G1, G2 ==> D1, D2 Gentzen hat diesen Beweis geführt. Er wollte wissen, welche Aussagen der Arithmetik man nicht beweisen kann (Gödel hatte ja die Unvollständigkeit der Arithmetik bewiesen). Dazu ersetzte er das Induktionsaxiom durch die omega-Regel. Dadurch konnte er eine (ordinale) obere Schranke für Längen schnittfreie Beweise angeben: epsilon_0. Dies lies Folgerungen auf definierbare Funktionen zu. (Schwichtenberg, Handbook of Math. Logic) Resolution ========== Def. 1. Literal: Atom oder negiertes Atom (A, NOT A, NOT door_closed) 2. Klausel: Endliche Menge von Literalen, gelesen als Disjunktion { NOT lift_moves, door_closed, alarm_on } Spezialfall: Die leere Klausel, oft notiert als BOX, ist per Definition unerfüllbar. Allgemein: { NOT A1, ..., NOT Am, B1, ... Bn } entspricht A1 AND ... AND Am IMPLIES B1 OR ... OR Bn 3. Klauselmenge: Menge von Klauseln (kann auch unendlich sein), gelesen als Konjunktion (Memo: Gesetzes-/Vertragsklauseln muss man *alle* erfüllen!) Spezialfall: Die leere Klauselmenge ist per Definition erfüllbar. Resolution ist ein Verfahren, um festzustellen, ob eine Klauselmenge erfüllbar ist, oder nicht. Interessant z.B., weil für jede Formel phi eine Klauselmenge CC_phi angegeben werden kann, sodass phi Tautologie ist wenn CC_phi unerfüllbar ist. Triviale Reduktion: CC_phi = { BOX } falls phi Tautologie {} sonst 2. Versuch: Bilde KNF von NOT phi Problem: Ausmultiplizieren bläht exponentiell auf. Verfeinerte Spezifikation: CC_phi kann aus phi in PTIME berechnet werden. "Clausification" ("Verklausulierung") Geg.: phi Betrache NOT phi und führe für jede Teilformel psi von NOT phi ein neues Atom A_psi ein drücke durch Klauseln aus, dass "A_psi äquivalent phi". Bsp: phi = (A AND (B OR C) => A AND B OR A AND C) Atome für Teilformeln von NOT phi: Abkürzung A_{NOT phi} A1 A_phi A2 A_{A AND (B OR C)} A3 A_{B OR C} A4 A_{A AND B} A5 A_{A AND C} A6 A_{A AND B OR A AND C} A7 A B C Klauseln A1 <==> NOT A2 {A1, A2}, {NOT A1, NOT A2} A2 <==> (A3 => A7) {NOT A2, NOT A3, NOT A7}, {A2, NOT A7}, {A2, A3} A4 <==> B OR C {A4, B}, {A4, C}, {NOT A4, NOT B, NOT C} Oft liegen Probleme aber schon in Klauselform vor: Bsp: "Wenn Otto Wein trinkt, dann mag er keinen Fisch oder hält Mittagsschlaf" {NOT otto_wein, NOT otto_fisch, otto_mittagsschlaf } Resolution: Herleitung der leeren Klausel. Resolutionsregel: Aus zwei Klauseln der Form K1 OR A und K2 OR NOT A darf die Klausel K1 OR K2 hergeleitet werden. Algorithmus: INPUT CC /* Klauselmenge */ done := false while (not done) { Finde C1,C2 in CC, sodass C1=K1 OR A und C2=K2 OR NOT A und K1 OR K2 nicht in CC Falls möglich, füge K1 OR K2 zu CC hinzu. Falls nicht möglich: done := true } OUTPUT: Falls BOX in CC, "unerfüllbar", sonst "erfüllbar" Beispiel 1: INPUT CC = {A, NOT B, C} (1), {NOT A, NOT B, NOT C} (2) STEP1 CC += {A, NOT B, NOT A} (3, aus 1 und 2) STEP2 CC += {NOT B, C, NOT C} (4, aus 1 und 2) Beispiel 2: phi = (A AND (B OR C) => A AND B OR A AND C) NOT phi in Klauselform (schlauer) CC: A, B OR C, NOT A OR NOT B, NOT A OR NOT C -------------------- ++ NOT B NOT C C BOX Korrektheit und Vollständigkeit der Resolution ============================================== Satz (Vollständigkeit): Lässt sich aus CC durch wiederholte Anwendung der Resolutionsregel die leere Klausel herleiten, so ist CC unerfüllbar. Beweis: Die Resolutionsregel erhält die Erfüllbarkeit: Annahme: eta erfülle K1 OR A und K2 OR NOT A Fall 1 : eta erfüllt K1, dann auch K1 OR K2 Fall 2 : eta erfüllt A, dann erfüllt eta K2 und damit auch K1 OR K2 Satz (Korrektheit): Sei CC eine Klauselmenge, die unter Resolution abgeschlossen ist. Wenn CC nicht die leere Klausel BOX enthällt, so ist CC erfüllbar. Notation: Sei L ein Literal. CC[L] ist die Klauselmenge, die aus C entsteht durch * Weglassen aller K mit L in K * Entfernen des Literals NOT L aus allen Klauseln, (die NOT L enthalten). Weitere Notation: CC[A->tt] := CC[A] CC[A->ff] := CC[NOT A] eta[A] := eta[A->tt] eta[NOT A]:= eta[A->ff] Lemma: * Ist CC abgeschlossen unter Resolution, dann auch CC[L]. * Ist CC[L] erfüllbar durch eta, dann erfüllt eta[L] CC. * Sind CC[L] und CC[NOT L] unerfüllbar, dann auch CC. Beweis des Satzes: Wir nummerieren die Atome A1,A2,... (unendlich viele Atome sind erlaubt). Wir konstruieren eine Belegung eta, die CC erfüllt, durch sukzessive Konstruktion von eta(A1), eta(A2),... Da BOX nicht in CC, muss entweder 1. BOX nicht in CC[A1], oder 2. BOX nicht in CC[NOT A1]. (Begründung: Falls BOX in CC[L] muss {NOT L} in CC gewesen sein. Wenn also 1. und 2. gelten so kann man die leere Klausel aus L und NOT L herleiten. Dies wiederspricht der Annahme, dass CC unter Resolution abgeschlossen ist.) Wähle nun eta(A1) := v, so dass BOX nicht in CC[A1->v]. Fahre fort mit dieser neuen Klauselmenge und A2. Auf diese Weise entsteht eine Belegung eta, die alle Klauseln in CC wahrmacht. Folgerung (Kompaktheitssatz): Ist eine Menge M von aussagenlogischen Formeln unerfüllbar, so existiert schon eine unerfüllbare endliche Teilmenge von M. Beweis: Die Herleitung der leeren Klausel verwendet nur endlich viele Ausgangsklauseln.