Ausdrücke und Klauseln im AK

Definitionen

Die Darstellung einer Klausel der Form

(Subscript[p, 1])∧  ...   ∧   (Subscript[p, n]) -> (Subscript[q, 1 ])∨  ...   ∨ (Subscript[q, m])

geschieht hier als ein Paar von Listen, d.h. in der Form

{{(Subscript[p, 1]),   ...  ,  (Subscript[p, n])}, {(Subscript[q, 1 ]),   ...  ,  
        (Subscript[q, m])}}

Der Widerspruch hat hier diese Klauseldarstellung:

{{}, {}}

Damit nimmt die cut Regel folgende Form an: Wenn zwei Klauseln eine Variable enthalten, einmal positiv, d.h. in der ersten Komponente und einmal negativ, d.h. in der zweiten Komponente, dann kann man die Variable dort streichen und die rechten und die linken Seiten zu einer neuen Klausel vereiningen. Dies macht die folgende in Mathematica Notation formulierte Regel:

generalCutRule = 
        cut[{{a1___, x_, e1___}, 
              l1_}, {l2_, {a2___, x_, e2___}}] :> {{a1, e1}~Union~l2, 
            l1~Union~{a2, e2}};

Alle Schnitte für eine gegebene Klauselmenge erhalten wir mit

allCuts[
        klauselMenge_] := ReplaceList[#, 
                generalCutRule] & /@ (Outer[cut, #, #, 1] &[
                  klauselMenge] // Flatten[#, 1] &) // Flatten[#, 1] & // 
        Union[#, klauselMenge] &;

Der Code ist nicht besonders effizient (Symmetrie ist zum Beispiel nicht berücksichtigt), aber kurz!

cutAbschluß[klauselMenge_] := 
      FixedPoint[allCuts, klauselMenge];

Und das war schon alles was wir brauchen.

Beispiele

Das Geheimnis des 100-jährigen (aus Uwe Schöning's Buch Logik für Informatiker)
Aufgabentext siehe auch hier AL-100J.html

Bier - b
Eis - e
Fisch - f

klauselMenge100J = {
{{b, 
            f}, {}}, 
{{}, {b, e, 
            f}}, 
{{}, {e, 
            f}}, 
{{b}, {f}}
}

cutAbschluß[klauselMenge100J] // MatrixForm

% // Length

Was es damit auf sich hat siehe weiter unten.

cutAbschlußRed[klauselMenge100J]

% // Length

Was ist die Folgerung? (Gute Aussichten ;-)

UA 1 Serie 2 2002 (L)

klauselMengeSerie2UA1L = {
{{p, r, 
              t}, {}}, 
{{}              , {q, s}}, 
{{p, s}      , {}}, 
{{p, 
              t}      , {}}, 
{{}              , {s, t}}, 
{{p, 
              r}      , {}}, 
{{}              , {p, s}}};

Aus der Klauselstruktur folgt, q  und ¬r gehen nicht zu erzeugen. Und wenn ¬q bzw. r in einer Klausel sind, wird man die durch Schneiden nie wieder los. Also betrachten wir die reduzierte Klauselmenge

klauselMengeRedSerie2UA1L = {
{{p, 
              s}      , {}}, 
{{p, 
              t}      , {}}, 
{{}              , {s, t}}, 
{{}              , {p, 
              s}}};

caRa = 
      cutAbschluß[klauselMengeRedSerie2UA1L] // MatrixForm

caRa // Length

Die Klauseln die nur aus Literalen bestehen erhalten wir so:

Cases[caRa, {{}, {x_}} | {{x_}, {}}]

Durch Inspektion sehen wir, auch ¬q bzw. r können mit den erhaltenen Literalen nicht erhalten werden.

Oder vollständig ohne Tricks:

caa = cutAbschluß[klauselMengeSerie2UA1L]

caa // Length

Cases[caa, {{}, {x_}} | {{x_}, {}}]

Schlußfolgerung: 
Solingen: Ja, 
Passau: Nein, 
Rest: Vielleicht

UA 2 Serie 2 2002 (L)

klauselMengeSerie2UA2L = {
{{p, 
            q}      , {}}, 
{{q, 
            s}      , {}}, 
{{s}            , {t}}, 
{{p}            , {s, 
            t}}, 
{{q}            , {s, 
            t}}, 
{{r}            , {s, 
            t}}, 
{{r}            , {p, 
            q}}, 
{{p, 
            t}      , {q}}, 
{{p}            , {s, q}}
};

Wir überprüfen zuerst, ob der Widerspruch und welche Literale ableitbar sind.
Aus der Klauselstruktur folgt, ¬r geht nicht zu erzeugen. Und wenn r in einer Klausel ist, wird man r durch Schneiden nie wieder los. Also betrachten wir die reduzierte Klauselmenge:

klauselMengeRedSerie2UA2L = {
{{p, 
              q}      , {}}, 
{{q, 
              s}      , {}}, 
{{s}            , {t}}, 
{{p}            , {s, 
              t}}, 
{{q}            , {s, 
              t}}, 
{{p, 
              t}      , {q}}, 
{{p}            , {s, q}}
};

Den vollständigen Cutabschluß brauchen wir nicht zu berechnen, denn Fälle in denen nur Tautologien entstehen, bringen keine neuen Erkenntnisse. Also Paare in denen eine Variable links und rechts vorkommt, brauchen nur bei dieser Variable geschnitten werden, wenn es nicht noch ein zweites solches Variablenpaar gibt.

(caRa = cutAbschluß[klauselMengeRedSerie2UA2L]) // 
      MatrixForm

caRa // Length

Davon sind aber noch eine Reihe Klauseln Tautologien, d.h. eine Variable kommt sowohl links als auch in der rechts vor, nämlich diese:

caReq = 
      Cases[caRa, {{a1___, x_, e1___}, {a2___, x_, e2___}}]

caReq // Length

Also brauchen wir eigentlich nur die folgenden Klauseln wirklich zu berechnen:

Complement[caRa, caReq]

% // Length

Nun schauen wir nach, welche Literale im Cutabschluß sind und ob evtl. der Widerspruch abgeleitet wurde:

Cases[caRa, {{}, {x_}} | {{x_}, {}} | {{}, {}}]

Also ist nur p, nicht jedoch ¬p ableitbar.

Vollständig ohne Tricks:

caa = cutAbschluß[klauselMengeSerie2UA2L]

caa // Length

Cases[caa, {{}, {x_}} | {{x_}, {}} | {{}, {}}]

Für die restlichen Ausdrücke müssen wir jeweils den zu prüfenden Ausdruck negieren, in Klauselform (Subscript[C, 2]) (evtl mehrere Klauseln!) umformen und überprüfen, ob sich aus einer zu X äquivalenten Klauselmenge (Subscript[C, 1]) und der Vereinigung mit (Subscript[C, 2]) der Widerspruch ableiten läßt. Nur dann, folgt H aus X.

Wir bezeichnen die zu überprüfenden Ausdrücke von links nach rechts mit (Subscript[H, 1]), ..., (Subscript[H, 6]).

Für (Subscript[H, 1])= p und  (Subscript[H, 2])=¬p haben wir die Antwort schon gefunden.

Für (Subscript[H, 3])= (p∨r) gilt ¬(Subscript[H, 3]) \(TraditionalForm\`\( = \_sem\)\) ¬p∧¬r und mit dieser Klausel kann man den Widerspruch nicht herleiten, wenn er schon aus (Subscript[C, 1]) nicht herleitbar war, weil wieder ¬r nicht wegzukriegen ist.

klauselMengeSerie2UA2L = {
{{p, 
              q}      , {}}, 
{{q, 
              s}      , {}}, 
{{s}            , {t}}, 
{{p}            , {s, 
              t}}, 
{{q}            , {s, 
              t}}, 
{{r}            , {s, 
              t}}, 
{{r}            , {p, 
              q}}, 
{{p, 
              t}      , {q}}, 
{{p}            , {s, q}}
};

Jetzt folgt reine Hand- bzw. Kopfrechnung. Für (Subscript[H, 4]) müssen wir die Klauseln p und r zu (Subscript[C, 1]) hinzunehmen und reduzieren damit die Klauselmenge klauselMengeSerie2UA2L sofort zu

{
{{}}, {{p}}, 
{{}}, {{r}}, 
{{q}      , {}}, 
{{q, 
            s}      , {}}, 
{{s}            , {t}}, 
{{p}            , {s, 
            t}}, 
{{q}            , {s, 
            t}}, 
{{}            , {s, 
            t}}, 
{{}            , {p, 
            q}}, 
{{t}      , {q}}, 
{{}            , {s, 
            q}}
};

Im nächsten Schritt schneiden wir mit ¬q und erhalten

{
{{}}, {{p}}, 
{{}}, {{r}}, 
{{q}      , {}}, 
{{q, 
            s}      , {}}, 
{{s}            , {t}}, 
{{p}            , {s, 
            t}}, 
{{q}            , {s, 
            t}}, 
{{}            , {s, 
            t}}, 
{{}            , {p}}, 
{{t}      , {}}, 
{{}            , {s}}
};

Im nächsten Schritt schneiden wir mit ¬t und erhalten

{
{{}}, {{p}}, 
{{}}, {{r}}, 
{{q}      , {}}, 
{{q, 
            s}      , {}}, 
{{s}            , {}}, 
{{p}            , {s}}, 
{{q}            , {s}}, 
{{}            , {s}}, 
{{}            , {p}}, 
{{t}      , {}}, 
{{}            , {s}}
};

Und nun sehen wir schon, daß wir mit s und ¬s den Widerspruch nachweisen können. Also (Subscript[H, 4]) ist ableitbar.

Als nächstes zu (Subscript[H, 5]):

klauselnH5 = {
{{}            , {p, q, 
              r}}, 
{{p, 
              q}      , {}}, 
{{q, 
              s}      , {}}, 
{{s}            , {t}}, 
{{p}            , {s, 
              t}}, 
{{q}            , {s, 
              t}}, 
{{r}            , {s, 
              t}}, 
{{r}            , {p, 
              q}}, 
{{p, 
              t}      , {q}}, 
{{p}            , {s, q}}
};

cutAbschluß[klauselnH5]

% // Length

Dies hat wirklich etwas zu lange gedauert, also lassen wir das Erzeugen von Tautologien und definieren eine neue reduzierte cut-Regel!

generalCutRuleRed = 
      cut[{{a1___, x_, e1___}, 
            l1_}, {l2_, {a2___, x_, e2___}}] :> {{a1, e1}~Union~l2, 
            l1~Union~{a2, e2}} /; 
          Intersection[{a1, e1}~Union~l2, 
              l1~Union~{a2, e2}] == {};

allCutsRed[
        klauselMenge_] := ReplaceList[#, 
                generalCutRuleRed] & /@ (Outer[cut, #, #, 1] &[
                  klauselMenge] // Flatten[#, 1] &) // Flatten[#, 1] & // 
        Union[#, klauselMenge] &;

cutAbschlußRed[klauselMenge_] := 
      FixedPoint[allCutsRed, klauselMenge];

Das reduziert Zeit und Speicherplatz doch schon deutlich wie wir nachfolgend sehen ;-).

caKlauselnH5 = cutAbschlußRed[klauselnH5];

caKlauselnH5 // Length

Cases[caKlauselnH5, {{}, {x_}} | {{x_}, {}} | {{}, {}}]

Kein Widerspruch ableitbar. Sorry, ja, für eine Handrechnung ist dieser Fall wohl immer noch zu aufwendig. :-(.

klauselnH6 = {
{{q}            , {r}}, 
{{p, q}      , {}}, 
{{q, 
              s}      , {}}, 
{{s}            , {t}}, 
{{p}            , {s, 
              t}}, 
{{q}            , {s, 
              t}}, 
{{r}            , {s, 
              t}}, 
{{r}            , {p, 
              q}}, 
{{p, 
              t}      , {q}}, 
{{p}            , {s, q}}
};

caKlauselnH6 = cutAbschlußRed[klauselnH6];

% // Length

Cases[caKlauselnH6, {{}, {x_}} | {{x_}, {}} | {{}, {}}]

Also (Subscript[H, 6 ])  auch nicht ableitbar!

Also mit Mathematica war das doch gar nicht so schwer ;-).