Elemente der künstlichen Intelligenz 4. Teil: Automatisches Beweisen

Einführung in die Problematik

In der letzten Folge haben wir zusammen die ersten logischen Terms umgeformt und dabei gesehen, daß Sprachen wie PROLOG und LISP die logischen Termumformungen weitgehend übernehmen können. Viel interessanter ist natürlich das Problem, dem Computer die selbständige Führung eines mathematischen Beweises unter Benutzung logischer Termumformungen zu übertragen. Einem mathematisch wenig gebildeten Menschen bereitet es meist erhebliche Schwierigkeiten, einem mathematischen Beweis auch nur zu folgen. Einen mathematisch korrekten Beweisgang werden sich deshalb wohl auch die wenigsten Leser Zutrauen. Sie werden sicher zustimmen, wenn man ein Gerät, das diese Beweise selbständig durchführt, als intelligent bezeichnet. Und da die Logik die „Haus- und Hofwissenschaft“ der Informatiker ist, ist es nicht weiter verwunderlich, wenn auf dem Gebiet der automatischen Beweisführung Spektakuläres geleistet wurde.

Grundlagen der Aussagenlogik

Zunächst brauchen wir natürlich wieder einige Begriffe aus der Aussagenlogik. Ich darf bei dieser Gelegenheit wieder einmal auf das wirklich ausgezeichnete Buch von D. R. Hofstadter (siehe Literaturhinweise) hinweisen, in dem Sie eine sehr eigenwillige, gut lesbare Einführung in die Aussagenlogik finden. Generell ist es die Aufgabe eines Beweises, zu zeigen, daß eine wohlgeformte Aussage (d. h. eine Aussage, deren syntaktischer Aufbau den Regeln der Aussagenlogik genügt) immer den Wahrheitswert wahr erhält, egal welchen Wahrheitswert die einzelnen in der Aussage vorhandenen Variablen annehmen. Z. B. ist die Aussage a v ~ a immer wahr, egal welchen Wert a annimmt. Um zu beweisen, daß diese Aussage immer wahr ist, würde es genügen, wenn man die Wahrheitstafel der Aussage niederschreibt. Bei komplizierten Aussagen führt dieses Verfahren schnell an die Grenzen der Anschaulichkeit. Dann ist es einfacher, durch erlaubte Umformungen zum gewünschten Ergebnis zu kommen. Nehmen wir an, daß die Ausdrücke a und b wohlgeformt sind. Dann sind es auch alle mit Hilfe der Junktoren ~ ,&,v gebildeten Ausdrücke: ~ a, a v b, a & b. Außerdem ist natürlich ein atomarer Ausdruck wohlgeformt. Weiterhin gelten die folgenden Äquivalenzen, d. h., der Ausdruck rechts von = kann ersetzt werden durch den Ausdruck links von = und umgekehrt:

1. ~ ~a = a
   Gesetz der doppelten Verneinung

2. ~(a v b) = ~a & ~b
   De Morgan’sches Gesetz

3. ~ (a & b) = ~ a v ~ b
   De Morgan’sches Gesetz

4. a v (b & c) = (a v b) & (a v c )
   Distributivgesetz

5. a -> b = ~avb
   Implikation

Die resultierenden Ausdrücke sind dann wieder wohlgeformt. Weiterhin benötigt man zur Herleitung neuer Aussagen noch sogenannte Schlußregeln:

1. Modus Ponens (bejahende Abtrennungsregel)

A —> b a b

Beispiel: Wenn es regnet, dann ist der Rasen feucht.
Es regnet.
Der Rasen ist feucht.

2. Modus Tollens (verneinende Abtrennungsregel)
   a —> b ~b ~a

Beispiel: Wenn es regnet, dann ist der Rasen feucht.
Der Rasen ist nicht feucht.
Es regnet nicht.

3. Kettenschluß

a —> b b —> c a —> c

Beispiel: Wenn Peter wütend ist, dann hat er Hunger.
Wenn Peter Hunger hat, dann ißt er Schokolade.
Wenn Peter wütend ist, dann ißt er Schokolade.

Die für uns interessante Form eines Beweises ist der sogenannte indirekte Beweis. Hier untersucht man die Negation des zu beweisenden Ausdrucks. Gelangt man durch Umformung der Negation zu einem Widerspruch, gilt also die negierte Aussage nicht, dann gilt nach dem Prinzip der doppelten Verneinung die originale Aussage. Schauen wir uns als Beispiel den Beweis des Kettenschlusses an:

Zunächst negieren wir den Term:

~((a -> b) & (b -> c) -> (a -> c)) =
~(~ ((~ a v b) & (~ b v c)) v (~ a v c))

Diesen Term bringen wir in die konjunktive Normalform, d. h. wir formen ihn so um, daß er nur noch einzelne, durch & verbundene Terme enthält:

~((~ (~ a v b) v ~ (~ b v c)) v (~ a v c)) =
(~ a v b)&(~ b v c) & ~(~a v c) =
(~ a v b)&(~ bvc)& a & ~c
(Term in konkjunktiver Normalform.

Diese konjunktive Normalform eines logischen Termes heißt auch Klauselform, die einzelnen durch & verbundenen Terme Klauseln (also z. B. (~ a v b)). Das Prinzip der Resolution besteht nun darin, zu zeigen, daß sich zwei Klauseln widersprechen, d. h. daß in einem logischen Term ein Unterterm der Form ...& x & ~x & ... vorhanden ist. Das im folgenden Kapitel erläuterte Resolutionsprinzip geht von diesem leicht zu beweisenden Theorem aus:

(a v x) & (~ a v y) —> xvy
(Resolutionsschritt)

Damit würde sich der Term in kon-unktiver Normalform darstellen lassen als:

(~a v b)&(~b v c)&a & ~c = (a v 0) & (~ a v b) & (~ b v c) & ~ c —>
(0 v b) & (~ b v c) & ~c = b & (~b v c) & ~c —> c & ~c (Widerspruch!)

Listing 1: Definition einiger Operatoren

Das Resolutionsprinzip

Das Resolutionsprinzip stellt sich also folgendermaßen dar.

1. Negiere den zu beweisenden Term.
2. Überführe den negierten Term in die Klauselform (konjunktive Normalform)
3. Führe wenn möglich den Resolutionsschritt durch.
4. Durchforste die Menge der Klauseln auf Widerspruch.
5. Wenn ein Widerspruch entdeckt wurde, dann ist die nicht negierte Aussage bewiesen.

Das in Listing 1 dargestellte PROLOG-Programm führt die hier beschriebene Resolution durch. Es benutzt einen in PROLOG geschriebenen Musterinterpreter aus dem sehr interessanten Buch von I. Bratko. Das Programm ist von mir so verändert worden, daß man jederzeit die Schlußweise der Maschine verfolgen kann. Gleichzeitig möchte ich an Hand dieses Programms die hervorragenden Eigenschaften von PROLOG bei der Definition eigener Operatoren erläutern.

Musterorientierte Programmierung

Unter musterorientierter Programmierung versteht man ein Programmschema, das nicht so starr reagiert wie die konventionellen Programmiermethoden. Normalerweise besteht ein Programm aus festen Modulen, deren Ablauf explizit vorgegeben ist. Ein musterorientiertes Programm besteht dagegen aus einer Sammlung von musterorientierten Modulen. Jedes Modul besteht aus zwei Teilen:

1. einem Bedienungsmuster,
2. Aktionen, die ausgeführt werden sollen, wenn das Bedingungsmuster erfüllt ist.

Die Ausführung eines Moduls wird in Gang gesetzt, wenn ein passendes Muster in der Datenbasis entdeckt wird. Musterorientierte Programmierung kann damit also so etwas wie ein natürliches Modell für parallele Datenverarbeitung angesehen werden, da jedes Modul auf einem separaten Prozessor implementiert werden kann, der auf die gemeinsame Datenbasis wirkt. Die Erfüllung von Bedingungsmustern erinnert natürlich sofort an den PROLOG-Unifizierungsprozeß. In der Tat ist der PROLOG-Interpreter nichts anderes als ein musterorientiertes Programmsystem. Im Beispielprogramm Listing 1 werden die Module in der Form

[Bedingungen] — [aktionen]

dargestellt. Hierin bedeutet [Bedingungen] eine Liste von Bedingungen in klausaler Form und [aktionen] eine Liste mit Prädikaten, die im Falle eines erfolgreichen Tests ausgeführt werden sollen. Das Prädikat Start setzt dann das musterorientierte Programm in Aktion, indem es das goal Bedingungen — Aktionen im Prädikat Start zu unifizieren versucht. Hat der PROLOG-Interpreter eine Instanz gefunden, dann wird ein Test ausgeführt, der alle Klauseln in der Bedingungsliste zu unifizieren versucht. Ist das gelungen, dann werden die in der Liste Aktionen aufgeführten Prädikate zur Unifizierung gebracht. Wenn alle Prädikate unifiziert worden sind, bleibt nur noch die leere Liste als Aktionsliste zurück. Dann wird durch erneuten Aufruf von Start nach dem nächsten Muster in der Datenbasis gesucht. Ist kein weiteres Muster vorhanden, hat der PROLOG-Interpreter einen Mißerfolg und beendet das Prädikat Start.

Das Prädikat op/3

Zur Funktionsweise des Programms in Listing 1 trägt in ganz besonderer Weise die Möglichkeit bei, in PROLOG eigene Operatoren zu vereinbaren. Dies geschieht mit Hilfe des Prädikates op/3. Die Syntax des Aufrufs ist op(Priorität,Assoziativität,Name). Hierin bedeutet Priorität eine Zahl zwischen 1 und 1200. Die Bedeutung dieser Zahl wird klar, wenn man sich an die Eselsbrücke Punktrechnung geht vor Strichrechnung erinnert. In PROLOG erkennt man diese Eselsbrücke in Form der Vereinbarung op(500,yfx,+) bzw. op(400,yfx,A) wieder. Man sieht: Je Kleiner die Priorität ist, desto eher wird der entsprechende Operator ausgewertet.

Die Assoziativität beschreibt gleichzeitig die Stelligkeit und Position des neu definierten Öperators. Die Assoziativität darf nur einen der folgenden Werte haben:

fx, fy, xfx, xfy, yfx, yfy, xf, yf

f steht für Funktor und kennzeichnet seine Stellung innerhalb eines Terms: fx und fy geben an, daß der neue Operator in Präfix-Notation zu gebrauchen ist. xfx, xfy, yfy und yfx kennzeichnen einen in Infix-Notation zu verwendenden Operator. xf und yf schließlich sind die Assoziativität eines Postfix-Operators. Wie man sieht, sind + und * also Infix-Operatoren, d. h. PROLOG erwartet das Additionszeichen bzw. Multiplikationszeichen zwischen zwei Zahlen oder Termen. Und was bedeutet x und y? Ein x gibt an, daß auf der betreffenden Seite alle Terme Operatoren mit niedrigerer Priorität haben müssen. Ein y läßt dagegen auch Operatoren mit niedriger oder gleicher Priorität zu. Um das zu verdeutlichen, schauen wir uns einen beliebigen arithmetischen Term an:

Dieser arithmetische Term ist äquivalent zu ((3AX) + 7)-(Y/4). Ein Blick in TAb. 1 zeigt uns, warum auch PROLOG diese Interpretation mit uns teilt. Der erste Operator, auf den der Interpreter bei der Bearbeitung des Termes stößt, ist ★. Auf der linken Seite ist alles klar, der einzige Operand ist das numerische Atom 3. Mehrdeutig könnte es auf der rechten Seite werden, wenn nicht die Assoziativität des ★-Operators den Wert yfx hätte. Damit besteht die Forderung, daß rechts vom ★-Zeichen nur Operatoren kleinerer Priorität stehen dürfen. + hat aber die Priorität 500 - und die ist um 100 größer als die Priorität 400, welche ★ besitzt. Folglich wird nur der Term 3^X bewertet und berechnet. Das Ergebnis steht nun zur Verfügung und

Tabelle 1

Abb.1: Argumentbindung durch unterschiedliche Prioritäten

der Interpreter nimmt diesen Wert als linke Seite des folgenden +-Operators. Da die rechte Seite nur kleinere und nicht gleiche Priorität haben darf, gehört der auf - folgende Term nicht zur rechten Seite. Das Ergebnis ist als (3 ★ X) + 7. Dieses Ergebnis wiederum stellt nun die linke Seite des folgenden Subtraktionsoperators dar. Und da / eine niedrigere Priorität besitzt als -, gehört der Term Y/4 in die rechte Seite des Subtraktionsoperators. Also wird jetzt erst der Term Y/4 bewertet. Die linke Seite des Divisionsoperators endet bei dem -Zeichen, da dieses eine höhere Priorität besitzt. Also wird jetzt nur der Wert Y/4 berechnet. Das Ergebnis ist jetzt der rechte Teil des Subtraktionsoperators, der jetzt folgende Operation durchzuführen hat: ((3AX) + 7) - (Y/4). Abb. 1 zeigt diese Situation nochmals graphisch.

Im Programm Listing 1 werden nun die folgenden Operatoren definiert:

—> Der Aktionsoperator für musterorientierte Programmierung. Er trennt die Bedingungsliste von der Aktionsliste.

~ Der Negationsoperator. Negiert die logischen Terme.

& Der Konjunktionsoperator. Verknüpfung zweier Terme durch logisches und.

v Der Disjunktionsoperator. Verknüpft zwei logische Terme durch oder.

—> Der Implikationsoperator a —> b heißt: Wenn a gilt, dann gilt auch b.

Die Prioritäten der entsprechenden Operatoren ergeben sich entsprechend den Regeln der Logik, wonach die Negation vor der Konjunktion vor der Disjunktion vor der Implikation zu berücksichtigen ist. Die Negation wird als Präfixoperator definiert (~ steht immer vor dem logischen Term, der negiert wird), die übrigen Operatoren werden als Infixoperatoren definiert (d. h. sie stehen zwischen zwei Termen). Nach der Definiton dieser Operatoren ist PROLOG in der Lage, logische Terme korrekt zu bearbeiten.

Das Prädikat forma um/2

Diese Prädikate enthalten das Wissen um die Umformung logischer Terme.

So bedeutet z. B. forme_um(~(~X), X)., daß der Term ~(~X) durch den vereinfachten Term X ersetzt werden kann (Prinzip der doppelten Negation). Ähnliche Umformungen finden sich für die Eliminierung der Implikation, die De Morgan’schen Gesetze und die Distributivgesetze. Falls ein Term noch Unterterme enthält, die umgeformt werden können, sorgen die drei letzten Instanzen dieses Prädikates für die entsprechende Umformung. Die Übersetzung eines Termes in Klauselform wird durch das Prädikat übersetze/1 vorgenommen. Dieses übersetzt einen Term in der Klauselform, indem es jeden einzelnen Term umformt. Ist keine weitere Umformung nach den Regeln forme_um mehr möglich, wird die so gefundene Formel in die Datenbasis aufgenommen.

:-beweise((mann(marcus) & pompejaner(marcus) & (pompejaner(X) => römer(X)) & herrscher(cäsar) & (römer(X) => (loyal(X,cäsar) v haßt(X,cäsar))) & (mann(X) v herrscher(Y) v versucht_mord(X,Y) => ~ loyal(X,Y)) & versucht_mord(marcus,cäsar)) => haßt(marcus,cäsar)).

Listing 2: Die geschichtliche Frage an den Computer

Die Produktionsregeln für das Resolutionsverfahren

Die Produktionsregeln, nach denen die Terme in konjunktiver Normalform abgearbeitet werden, sind in Form der oben beschriebenen Muster in der Datenbank enthalten. So lautet die Regel, die den Widerspruch in der Datenbank entdeckt:

Wenn also in der Datenbank sowohl die Klausel X als auch ihre Negation enthalten ist, dann liegt ein Widerspruch vor und die Aktionsliste druckt die entsprechende Mitteilung aus und stoppt die weitere Ausführung des Programms. In den Produktionsregeln taucht u. a. das Prädikat fertig/3 auf. Es dient dazu, einen Überlauf in der Datenbank zu verhindern. Die Resolution produziert ja neue Klauseln: (a v b) & (~ a v c) —> (b v c). Bei Existenz zweiter Klauseln der Form (a v b) & (~ a v c) wird folglich eine neue Klausel (b v c) produziert und in die Datenbank aufgenommen. Da aber die alten Klauseln (a v b) und (~ a v c) nicht aus der Datenbank entfernt werden, würde beim nächsten Aufruf der Resolution wieder die gleiche Klausel produziert werden. Um das zu verhindern, wird bei der ersten Produktion einer Klausel das Prädikat fertig((a v b),( ~ a v c),a). in die Datenbank aufgenommen, was eine nochmalige Resolution obiger Klauseln verhindert, die Resolution von Untertermen aber noch zuläßt. Falls schließlich alle logischen Terme in der Datenbasis umgeformt sind und keine weitere Resolution mehr möglich ist, dann trifft PROLOG schließlich auf die leere Bedingungsliste und weiß, daß kein Widerspruch in der Datenbasis gefunden wurde. In diesem Fall ist der Beweis des zu beweisenden Satzes gescheitert! Zur Übung sollten Sie sich den Beweis (a — b)&(b — c) — (a—c) einmal vom Programm vorführen lassen. Anschließend schauen wir uns die Arbeitsweise des Programms einmal an einem berühmten Beispiel an: Der Frage nämlich, ob Marcus Cäsar haßte.

Haßte Marcus Cäsar?

Dieses Beispiel stammt von Elaine Rieh und ist eine gute Demonstration für die Instanzierung von Variablen in logischen Termen während des Beweises. Hier die Postulate, von denen im Beweis ausgegangen wird:

mann(marcus). Marcus war ein Mann.

pompejaner(marcus). Marcus war ein Pompejaner.
pompejaner(X) —> römer(X). Alle Pompejaner waren Römer.
herrscher(cäsar). Cäsar war ein Herrscher.
römer(X) —> loyal(X,cäsar) v haßt (X,cäsar). Alle Römer waren entweder Cäsar gegenüber loyal oder sie haßten ihn.
mann(X) & herrscher(Y) & versucht_mord(X,Y)-> ~loyal(X,Y).
Wenn ein Mensch einen Herrscher zu ermorden versucht, dann ist er ihm nicht loyal gegenüber, versucht_mord(marcus, cäsar). Markus versuchte Cäsar zu ermorden.

Listing 2 zeigt nun die Eingabe, die für den Beweis nötig ist, daß Marcus Cäsar haßte, und Abb. 2 zeigt die Arbeit des Programmes.

(Dr. Sarnow)

Literaturhinweise:

1.) Bratko, Ivan. PROLOG Programming for artificial Intelligence.
Addison Wesley Publishing. 1986.

2.) Hofstadter, Douglas R. Gödel, Escher, Bach: ein endlos geflochtenes Band.
Ernst Klett Verlage. 1985.

3.) Rieh, Elaine. Artificial Intelligence.
McGraw-Hill 1983.

Abbildung 2: Haßte Markus Cäsar? Ein neuzeitlicher Lösungsweg!