Humboldt-Universität zu Berlin, Institut für Informatik,


Meine Mathematica Implementation des Cut-Abschlusses einer Klauselmenge erfordert die Eingabe der Klauseln als geordnete Paarmenge von Variablen der linken und Variablen der rechten Seite einer Klausel. Fehlende Variablen sind als leere Menge einzugeben. Die Klausel falsum ist damit gleich {{},{}}.

Der vollständige Quelltext liefert keinen besonders effizienten Algorithmus, ist aber schön kurz, oder?

generalCutRule = cut[{{a1___, x_, e1___}, l1__}, {l2__, {a2___, x_, e2___}}] -> {{a1, e1}~Union~l2, l1~Union~{a2, e2}}

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

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

Die geordneten Klauseln (36) für die Übungsaufgabe 4 aus der Serie 7 sieht man nach Ausführung von

cutAbschluß[klauselMengeSerie7A4]


Für die Aufgabe zum Diätgeheimnis des 100-jährigen aus Uwe Schönings Buch Logik für Informatiker ergibt sich als Schnittregelabschluß

cutAbschluß[{{{b, f}, {}}, {{}, {b, e, f}}, {{}, {e, f}}, {{b}, {f}}}] =

{{{}, {e, f}}, {{}, {b, e, f}}, {{b}, {}}, {{b}, {e}}, {{b}, {f}}, {{b}, {b, e}}, {{b}, {e, f}}, {{f}, {e, f}}, {{b, f}, {}}, {{b, f}, {e}}}

Die Ableitung von (p -> p) aus axa ist gefunden und natürlich mit Mathematica. Es geht ganz leicht, entweder mit den axa-Regeln 3 und 14, 15 oder mit 1, 2 und 3. Die Vorführung gibt's in der Übung! Als Anregung zum Nachdenken und Testen noch zwei Einzeiler :-).

abla[{L_, R_}, L_] := R

able[H_, p_?AtomQ, A_] := (H /. p -> A) /; varQ[p] && ! FreeQ[H, p]