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.