Kapitel 5 - Automatisches Beweisen
 
 
 

Wir wollen nun einen Algorithmus kennen lernen, mit dessen Hilfe sozusagen rein "mechanisch" die Gültigkeit einer Formel überprüft werden kann. Der Resolutionskalkül dient dabei, neben der Methode der Wahrheitstafeln der Aussagenlogik sowie den rein syntaktischen Deduktionskalkülen der Aussagen- und Prädikatenlogik, als weiteres syntaktisches Entscheidungsverfahren für die Frage nach der Gültigkeit logischer Ausdrücke.

Die Aufgabe des Resolutionskalküls besteht konkret darin, die Unerfüllbarkeit (Kontradiktion) einer gegebenen Formelmenge nachzuweisen. Der Resolutionskalkül hat die Eigenschaft der Korrektheit (Widerspruchsfreiheit), indem er keine erfüllbare Formel als vermeintlich unerfüllbar deklariert. Er ist darüber hinaus insofern vollständig, als er jede unerfüllbare Formel als solche nachweist.

Mit Hilfe der Resolution werden v. a. zwei Fragestellungen abgehandelt:

1. Ist eine gegebene Formel p eine Tautologie? Dies gilt genau dann, wenn ¬ p eine Kontradiktion ist.

2. Folgt aus einer Formelmenge { p1, ..., pn } die Formel q? Diese Fragestellung ist identisch mit der Frage, ob p1 ... pn ¬ q unerfüllbar ist. Wieso? Man bedenke, dass gilt: P q iff ( p1 p2 ... pn ) q ( i { 1, ..., n }: pi P ).

 
5.1 Resolution in der Aussagenlogik zurück

Definition 5.1.1 Ein Literal ist eine atomare Formel oder deren Negation.

Voraussetzung für die aussagenlogische Resolution ist, dass die betrachtete Formel in KNF vorliegt. Dabei werden Formeln in KNF für die Zwecke der Resolution in der sog. Klauselform notiert. Aus

F = ( L11 ... Ln11 ) ... ( L 1k ... Lnkk )

erhält man die Klauselform

F = {{ L11, ..., Ln11}, ..., { L 1k, ..., Lnkk }}

Jedes Element von F heißt Klausel und besteht ausschließlich aus Literalen, die allesamt Disjunktionsglieder sind. Die Klauseln selbst sind Konjunktionsglieder. Wegen der Mengennotation sind die Formeln (( p1 ¬ p2) ( p3 p3 )), ( p3 ( ¬ p2 p1 )) sowie ( p3 (( ¬ p2 ¬ p2 ) p1 ) allesamt mit der Klauselmenge {{ p3 }, { p1, ¬ p2 }} identisch.

Definition 5.1.2 Seien K1, K2 Klauseln. Dann heißt R Resolvent von K1 und K2, falls es ein Literal L gibt mit L K1 und L K2 und R folgende Form hat:

R = ( K1 - { L } ) ( K2 - { } )

wobei gilt:

¬ p : falls L = p
p : falls L = ¬ p

Resolvent und zugehörige Klauseln können leicht als Diagramm veranschaulicht werden.

Anmerkung 5.1.1 Aus letzterer Definition geht hervor, dass auch die leere Menge als Resolvent auftreten kann. Diese wird mit dem speziellen Symbol gekennzeichnet. Eine Klauselmenge, die als Element enthält, ist dann unerfüllbar. Um diese Behauptung motivieren zu können, bedürfen wir eines Beweises des Resolutionslemmas.

Satz 5.1.1 (Resolutionslemma) Sei F eine Formel in KNF, dargestellt als Klauselmenge. Ferner sei R ein Resolvent zweier Klauseln K1, K2 in F. Dann sind F und F { R } äquivalent.

Beweis: (1) Falls || F { R } || = 1, dann auch || F || = 1, da die Klauseln der Klauselform Konjunktionsglieder sind.

(2) Sei umgekehrt || F || = 1 iff für alle K F gilt: || K || = 1. Der Resolvent R habe die Form R = ( K1 - { L } ) ( K2 - { } ), K1, K2 F, L K1, K2. Es gilt nun:

1. Falls || L || = 1, dann gilt: || || = 0. Ferner gilt annahmegemäß || K2 = 1. Also gilt erst recht || K2 - || = 1 und somit || R || = 1, da R ja nichts anderes als eine Disjunktion ist, für welche allgemein gilt, dass, falls nur ein Disjunktionsteil den Wahrheitswert 1 hat, dadurch die gesamt Disjunktion wahr wird.

2. Falls || || = 1, dann ist || L || = 0, also ist, wegen || K1 || = 1, annahmegemäß, sicherlich || K1 - { L } = 1, und also || R || = 1.

Beispiel 5.1.1 Die Klauselmenge {{ p3, ¬ p4, p1 }, { p4, ¬ p1 }} hat die beiden Resolventen { p3, p1, ¬ p1 } sowie { p3, p4, ¬ p4 }. Die Klauselmenge {{ p1 }, { ¬ p1 }} hat genau einen Resolventen: Die leere Menge, die wir im Zusammenhang der Resolution mit symbolisieren.

Definition 5.1.3 Sei F eine Klauselmenge. Dann ist Res ( F ) definiert als

Res ( F ) = F { R | R ist Resolvent zweier Klauseln in F }.

Ferner gilt:

Res0 ( F ) = F

Resn+1 ( F ) = Res ( Resn ( F )), n ≥ 0

Res* ( F ) = Un≥0 Resn ( F )

Der entscheidende Satz für die aussagenlogische Resolution lautet nun:

Satz 5.1.2 Eine Klauselmenge F ist unerfüllbar genau dann, wenn Res* ( F ).

Beweis: Wir wollen hier nur kurz die Korrektheit der Resolution betrachten: Die leere Klausel kann nur durch Resolution zweier Klauseln K1, K2, mit K1 = { L } und K2 = { }, entstanden sein. Mit dem Resolutioslemma gilt aber:

F ≡ Res1 ( F ) ≡ Res2 ( F ) ≡ ... ≡ Resn ( F ) ≡ ...

Wenn Res* ( F ), dann muss es ein n ≥ 0 geben, so dass Resn ( F ) auch K1, K2 Resn ( F ). Keine Belegung mit Wahrheitswerten erfüllt aber zugleich K1 = { L }und K2 = { }, so dass wegen Resn ( F ) ≡ F unerfüllbar ist.

Definition 5.1.4 Eine Deduktion der leeren Klausel aus einer Klauselmenge F ist eine Folge K1, K2, ..., Km von Klauseln mit der Eigenschaft:

1. Km = und für jedes i { 1, ..., m } gilt: Entweder ist Ki Element von F, oder Resolvent aus Klauseln Kj, Kk mit j, k > i.

Anmerkung 5.1.2 Eine Klauselmenge ist also genau dann unerfüllbar, falls die leere Klausel aus ihr deduziert werden kann. Die selbe Klausel kann innerhalb des Deduktionsprozesses in mehreren Resolutionsschritten verwendet werden.

Der Aufwand einer solchen Deduktion kann, ebenso wie beim Verfahren der Wahrheitstafeln, exponentiell sein, das heißt die Deduktion der leeren Formel kann zu exponentiell vielen Formeln führen. Aus diesem Grunde ist das Resolutionsverfahren nicht per se "effizienter" als die Methode der Wahrheitstafeln.

Beispiel 5.1.2 Sei F = {{ ¬ p, q }, { ¬ q }, { p }} eine Klauselmenge. Wir deduzieren dann:

1. Klausel: { ¬ p, q },

2. Klausel: { ¬ q },

3. Resolvent aus (1) und (2): { ¬ p },

4. Klausel: { p },

5. Resolvent aus (3) und (4): .

 
5.2 Resolution in der Prädikatenlogik zurück

In der Prädikatenlogik kann nicht unmittelbar der Resolvent zweier Klauseln { P ( f ( a )) } und P ( x ) bestimmt werden, da beide Klauseln zwar genau die selben Prädikate enthalten, diese jedoch unterschiedlich prädizieren. Wir bedürfen zu aller erst des "Gleichnamigmachens" beider Klauseln, etwa dadurch, dass in der zweiten Klausel x durch f ( a ) ersetzt wird. Diese Art der Substitution nennt man Unifikation in der PL. Wir hätten auch zuerst x durch f ( y ) und dann y durch a ersetzen können, nur wäre diese Substitutionskette "länger", sozusagen "komplexer". Ferner sehen wir, wie wichtig es ist, dass die "unifizierten" Ausdrücke allquantorfizierte Variablen enthalten.

Definition 5.2.1 Eine Substitution sub heißt Unifikator einer Menge von Literalen L = { L1, L2, ..., Lk }, falls L1 sub = L2 sub = ... = Lk sub. Das heißt durch Anwendung der Substitution auf jedes Literal von L entsteht ein und dasselbe Literal. Man schreibt hierfür auch | L sub | = 1 und sagt L sei unifizierbar.

Ein Unifikator sub einer Literalmenge L heißt allgemeinster Unifikator von L, falls für jeden Unifikator sub' von L gilt, dass es eine Substitution s gibt, so dass sub' = sub s ist (dieser Ausdruck besagt, dass für jedes Literal gilt Li sub' = Li sub s).

Anmerkung 5.2.1 Der allgemeinste Unifikator kann algorithmisch hergeleitet werden:

Unifikationsalgorithmus

Eingabe: nicht-leere Literalmenge L.

sub =def [ ] (die leere Substitution).

while | L sub | > 1 do begin

Durchsuche die Literale in L sub von rechts nach links, bis die erste Position gefunden wird, an der sich mindestens zwei Literale unterscheiden (etwa L1 und L2);

if keines der beiden verschiedenen Zeichen ist ein Variable

then stoppe mit der Ausgabe "nicht unifizierbar";

else sei x eines der verschiedenen Zeichen, sei x eine Variable und t der im anderen Literal betroffene Term (t kann auch eine Variable sein / enthalten);

if x kommt in t vor;

then stoppe mit der Ausgabe "nicht unifizierbar";

else sub =def sub [ x / t ] (die Hintereinanderausführung von sub und [ x / t ] );

end

Gib sub als allgemeinsten Unifikator von L aus.

Anmerkung 5.2.2 In jedem Schleifendurchlauf ersetzt letzterer Algorithmus, fall es nicht infolge der Stopp-Bedingung terminiert, eine Variable x, die nach Ausführung der Substitution also nicht mehr in der Literalmenge L vorkommt. Es können also höchstens so viele Schleifendurchläufe auftreten, wie zu Beginn verschiedene Variablen in L vorhanden sind.

Zur Erleichterung der Sprechweise führen wir noch folgende Definition ein:

Definition 5.2.2 Die Nichtübereinstimmungsmenge D ( L ) einer Menge von Literalen ist die Menge aller Teilformeln bzw. Terme von Elementen von L, die jeweils an der selben Stelle innerhalb von Literalen (Atome oder deren Negation) von L am weitesten links vorkommen und jeweils mit verschiedenen Symbolen beginnen. L besteht dabei nur aus Literalen, die aus identischen Prädikaten aufgebaut sind.

Beispiel 5.2.1 Sei die Literalmenge

L = { ¬ P ( f ( f ( u, v ), g ( a, y )), h ( z )), ¬ P ( f ( f ( u, v ), w ), h ( f ( a, b ))) }

gegeben.

1. D ( L ) = { z, f ( u, v ) }. Wir bilden also die Substitution sub = [ z / f ( u, v ) ], wenden diese auf L an und erhalten:

L' = { ¬ P ( f ( f ( u, v ), g ( a, y )), h ( f ( u, v ))), ¬ P ( f ( f ( u, v ), w ), h ( f ( a, b ))) }

2. D ( L' ) = { w, g ( a, y ) }. sub wird als erweitert um [ w / g ( a, y )], was folgendes ergibt:

L' = { ¬ P ( f ( f ( u, v ), g ( a, y )), h ( f ( u, v ))), ¬ P ( f ( f ( u, v ), g ( a, y )), h ( f ( a, b ))) }

3. D ( L'' ) = { a, u }, also wird sub erweitert durch [ u / a ] ( u ist eine Variable, a eine Konstante):

L''' = { ¬ P ( f ( f ( a, v ), g ( a, y )), h ( f ( a, v ))), ¬ P ( f ( f ( a, v ), g ( a, y )), h ( f ( a, b ))) }

4. Schließlich ist D ( L''' ) = { b, v }. Mit der Substitution [ v, b ] erhält man:

L''' = { ¬ P ( f ( f ( a, b ), g ( a, y )), h ( f ( a, b ))) }

Unser allgemeinster Unifikator hat also die Gestalt:

sub = [ z / f ( u, v ) ] [ w / g ( a, y ) ] [u / a ] [ v / b ]

Definition 5.2.3 (Prädikatenlogische Resolution) Seien K1, K2 und R prädikatenlogische Klauseln. Dann ist R ein prädikatenlogischer Resolvent von K1, K2, falls gilt:

1. Es werden, falls nötig, mittels der Substitution s1, s2 Variablenumbenennungen vorgenommen, so dass K1 s1 und K2 s2 keine gemeinsamen Variablen mehr enthalten.

2. Es gibt eine Menge von Literalen L1, ..., Lm K1s1 ( m ≥ 1 ) und L1', ..., Ln' K2s2 ( n ≥ 1 ), so dass L = { 1, ..., m, L1', ..., Ln' } unifizierbar ist. Es sei sub allgemeinster Unifikator der Menge L.

3. R hat dann die Form:

R = (( K1s1 - { L1, ..., Lm } ) ( K2s2 - { L1', ..., Ln' } )) sub

Anmerkung 5.2.3 Die erste Bedingung letzterer Definition benötigen wir, damit wir mit der zweiten Stopp-Bedingung des Unifikationsalgorithmus keine Schwierigkeiten bekommen. Arbiträre Variablenbezeichner sollen der Resolution nicht im Wege stehen. Ferner ist eine solche Umbenennung wegen Satz 4.5.1 zulässig.

Die Definition der Menge L in der zweiten Definitionsbedingung ist vor dem Hintergrund zu verstehen, dass die Literale unifizierbar sein müssen, also als identische Zeichenketten auftreten müssen.

Wir bemerken ferner, dass die aussagenlogische Resolution einen Spezialfall der prädikatenlogischen Resolution darstellt, insofern als für diese s1 = s2 = [ ] sowie m = n = 1 gilt.

Es gilt nun wieder, was hier nicht eigens formal eingeführt werden muss, dass eine Klauselmenge dann unerfüllbar ist, falls sie die leere Klausel enthält. Der Deduktionsbegriff der Resolution wird dann ganz analog wie in der aussagenlogischen Resolution eingeführt.

Satz 5.2.1 Sei F eine Formel in SNF mit der Matrix F' in KNF. Dann gilt: F ist unerfüllbar genau dann, wenn Res* ( F' ).

Anmerkung 5.2.4 Für eine Menge prädikatenlogischer Formeln P kann nun die Formel P p (als anzunehmende Tautologie) via Resolution wie folgt bewiesen werden:

1. Ersetzen von , das heißt Bildung von ¬ P p.

2. Bildung der negierten Form, das heißt P ¬ p.

3. Transformation von P und ¬ p in SNF.

4. Überführung in Klauselform.

5. Unifikation und Resolution.