OTTER wurde von William McCune, Mitglied der Abteilung für Mathematik und Computerwissenschaften des Argonne National Laboratory entwickelt. Es gibt mehrere vogehenden Versionen von OTTER: Version 0.9 - Mai 1988, Version 1.0 - Januar 1989, Version 2.0 - März 1990, Version 2.2 - Juli 1991 und die bis jetzt letzte Version 3.0.4. Im Vergleich zu anderen Programme für Automatisches Beweisen bietet OTTER mehr Geschwindigkeit und Vielseitigkeit.

OTTER läuft sehr gut auf einer Workstation wie Sun oder auf einem IBM kompatiblen PC aber man kann auch eine Macintosh Version des Programms erhalten. OTTER ist in C programmiert worden. Den Code des Programmes und einige Beispielprogramme kann man kostenlos aus dem Internet herunterladen: http://www.mcs.anl.gov/home/mccune/ar/otter/

Um über OTTER zu sprechen muß ich erst den Begriff 'Automatisches Beweisen' ganz kurz erläutern. Also:

Was ist "Automatisches Beweisen"?
("Automated Theorem Proving")

Um zu verstehen was Automatisches Beweisen ist, müssen wir den Begriff Beweisen definieren. Beweisen ist der Prozeß ausgehend von gegebenen Fakten durch anwenden von gegebenen Regeln Schlußfolgerungen erstellen zu können.

OTTER stützt sich auf dieser Art von Beweisen -logisches Beweisen- und nicht auf probabilistisches Beweisen, auf Schlußfolgerungen die sehr wahrscheinlich wahr werden wenn die gegebenen Fakten wahr sind. Die einzigen angenommenen Schlußfolgerungen sind die, welche unmittelbar logisch den gegebenen Fakten folgen.

Ziel des automatischen Beweisen ist es Programme zu schreiben welche als Assistenten dienen beim lösen von Probleme und beantworten von Fragen die einen Beweis verlangen.

"Das einzige Mittel, unsere Schlußfolgerungen zu verbessern, ist, sie ebenso anschaulich zu machen, wie es die der Mathematiker sind, derart, daß man seinen Irrtum mit den Augen findet und, wenn es Streitigkeiten unter Leuten gibt, man nur zu sagen braucht: 'Rechnen wir!' ohne eine weitere Förmlichkeit, um zu sehen, wer recht hat." G.W.Leibniz (1646-1716)

Wie kann ich einem solchen Programm beibringen, welche Aufgabe es auszuführen hat?

Der erste Schritt ist ihm beizubringen WAS zu beweisen , oder WELCHE die Frage zu beantworten ist.

Dafür muß ich ihm die gegebenen Fakten liefern, die den Umfeld der Aufgabe bilden. Das heißt, ich muß ihm wirklich alles, auch das einfachste, offensichtlichste Faktum liefern. Ein automatisches Beweisprogramm hat ein sehr kleines gegebenes Wissen.

Um sich mit einem Programm zu verständigen, ist die menschliche Sprache natürlich unzulänglich, also, brauche ich eine Sprache welche von meinem Programm akzeptiert, verstanden wird.

Nachdem ich dem Programm das Problem beschrieben habe, muß es nach neuen Fakten suchen, indem es ausgehend von den gegebenen Fakten Schlußfolgerungen zieht. Das funktioniert in Kürze so:

Das Programm wendet auf den gegebenen Fakten bekannte Regeln an, sogenannte Inferenzregeln (inference rules). Dadurch entstehen neue Fakten welche genauso gültig (wahr) sind wie die am Anfang gegebenen, weil sie ja logisch den Anfangsfakten folgen. Deshalb können sie im nächsten Schritt auch als gegeben in Betracht gezogen werden.

Indem die Menge der wahren Fakten zunimmt, vergrößert sich eigentlich die Information, das Wissen unseres Programmes.

Wie kann ich dem Programm den Weg zum Erfolg zeigen?

Fakten und Regeln reichen aber nicht aus um auf die gewünschte Antwort zu kommen. Wenn ich Regeln auf Fakten exhaustiv anwende, wird die Menge meiner Fakten exponentiell wachsen. Die meisten davon sind aber irrelevant für meine Aufgabe. Dadurch rückt die gesuchte Antwort wird immer weiter weg anstatt sich zu nähern.

Das heißt, ich muß dieses Anwenden von Regeln auf Fakten sehr strikt kontrollieren. Dieses Vorgehen wird Strategie (strategy) genannt. In jedem Spiel (Schach, Poker...) ist Strategie essentiell für das Gewinnen. Das wird von dem Programm auf verschiedenen Weisen gleichzeitig durchgeführt:

-Kontrollieren in jedem Schritt des Auswählens von Fakten auf welche die Inferenzegeln angewendet werden sollen; -die Menge von Fakten nur mit denjenigen neugewonnenen Fakten bereichern welche, genaue, von vornherein festgelegte Kriterien erfüllen.

Wie wird Automatisches Beweisen in OTTER durchgeführt?

OTTER arbeitet nur auf Mengen von Klauseln. Wenn der Anwender seine Eingabe nicht als Menge von Klauseln eingibt, sondern als Formeln erster Ordnung, generiert OTTER gleich die dazu äquivalente Menge von Klauseln.

OTTER speichert vier Mengen von Klauseln:

1. usable

-enthält Klauseln auf denen die Inferenzregeln angewendet werden.

-set of support - Klauseln sind nicht für Inferenzregeln da, sondern um die Suche einzuschränken. Die sos-Liste gehört zu den vorher erwähnten Strategien.

-wirken bei der Suche nicht mit sondern werden für 'unit conflict' und 'forward subsumption' berücksichtigt; gehören also auch zu den Strategiemethoden.

-das sind Gleichheitssätze welche als Regeln beim Schreiben der neugewonnenen Klauseln mitwirken.

Die üblichste Art OTTER zu verwenden ist einen Beweis auf Widerspruch zu suchen. Das heißt ich versuche ein Theorem mit Hilfe von OTTER zu beweisen, indem ich das Problem unlösbar oder das Theorem als falsch annehme. Diese Art von Annahme wird durch das Einfügen von Informationen ins Inputfile von denen erwartet wird, daß sie falsch sind. Wenn das Programm über genügend Informationen verfügt, wird es auf einen Widerspruch kommen.
Die Vorgangsweise von OTTER im Suchen nach einem Widerspruch sieht folgendermaßen aus:

WHILE (SOS nicht leer ist und kein Widerspruch gefunden wurde) DO

1. Wähle 'lightest' Klausel in SOS als 'given' Klausel.

2. Versetze 'given' Klausel von SOS nach USABLE.

3. Gewinne neue Klauseln durch Inferenzregeln, wobei ein Elternteil jeder neuen Klausel die 'given' Klausel ist und die anderen, Klauseln die der USABLE - Liste gehören.

4. Klauseln welche die 'Aufbewahrungstests' (retention Tests) erfüllen, werden in die SOS Liste eingetragen.

Die Prozedur beim Behandeln der neu gewonnenen Klausel kann man folgendermaßen beschreiben (optionale Schritte werden mit * markiert):

1. Neunummerierung der Variablen.
*2. Ausgabe der new_cl.
3. Demodulation der new_cl.
*4. Orientierung der Gleicheitssätze.
*5. Anwenden von unit deletion.
6. Kürzen von identischen Literalen (die linke Kopie wird behalten).
*7. Anwenden von factor-simplification.
*8. Wegschmeißen der new_cl und exit wenn new_cl zu viele Literale oder Variablen enthält.
9. Wegschmeißen der new_cl und exit wenn new_cl eine Tautologie ist.
*10. Wegschmeißen der new_cl und exit wenn new_cl zu 'heavy' ist.
*11. Sortieren der Literalen.
*12. Wegschmeißen der new_cl und exit wenn new_cl in anderen Klauseln der SOS, USABLE oder PASSIVE
(forward subsumption) Liste logisch enthalten ist.
13. Integrieren der new_cl und Einfügen in SOS.
*14. Klausel erscheint im Output.
15. Wenn new_cl 0 Literale enthält, so haben wir den Widerspruch gefunden.
16. Wenn new_cl aus einem Literal besteht, dann suche im SOS, USABLE und PASSIVE nach 'unit conflict',
also nach den Widerspruch.
*17. Schreibe den Beweis wenn ein Widerspruch gefunden wurde.
*18. Versuche new_cl als Demodulator zu schreiben.

Schritte 19-20 werden erst dann ausgeführt, nachdem die Schritte 1-18 für jede einzelne Klausel exekutiert wurden, welche aus der 'given' Klausel entstanden sind.

Es gibt zwei grundsätzliche Arten OTTER zu verwenden: interaktiv und autonom. Man kann aber die zwei Arten abwechselnd in demselben Beweis anwenden.

In dem autonomen Modus wird OTTER das Input nach einfachen syntaktischen Eigenschaften durchsuchen, und wird entscheiden, welche Inferenzregeln und welche Strategie anzuwenden ist. Wir können nicht erwarten, daß es jeden Beweis wirklich alleine findet aber es ist sicher ein guter Start auf der Suche nach einem solchen Beweis.

Wie gesagt, kann man keinen Beweis ohne Verwendung von Strategie erfolgreich durchführen. Eine Art Strategie schränkt die anzuwendenden Inferenzregeln ein; eine andere Art lenkt deren Anwendung. Von der ersteren Art ist die wichtigste die SOS - Strategie. OTTER verlangt unbedingt das Verwenden dieser Strategie.

Die Listen SOS und USABLE sind diejenigen, wo das Programm die Klauseln sucht, auf welche die Inferenzregeln angewendet werden. Damit das Programm imstande ist, einen Beweis weiterzuführen darf die SOS Liste nicht leer sein. Die Meldung 'SOS Liste leer' kann drei Ursachen haben: 1. irgendeine

Klausel fehlt von der SOS Liste oder 2. ein gesetzter Parameter schränkt das Programm ein den Beweis weiterzuführen oder 3. die Menge von Inputklauseln ist konsistent, enthält also keinen Widerspruch.

Eine ganz andere Art die Anwendung der Inferenzregeln einzuschränken ist ihre Anwendung zu lenken. Zu diesem Zweck und auch für das Filtern von neugewonnener Information können wir die WEIGHTING Strategie anwenden. Jeder Klausel wird explizit oder als default ein Gewicht zugewiesen. Dieses Gewicht dient als Kriterium zur Auswahl der 'given' Klausel (es wird die leichteste ausgewählt) aber auch zum entfernen von zu 'schweren' Klauseln.

Folgend möchte ich ein paar Sprichwörter (man kann sie nicht als Regeln bezeichnen) zitieren:

Für die Darstellung eines Problems für ein automatisches Beweisprogramm wird uns empfohlen:

1. Unit Klauseln den Nonunit Klauseln zu bevorzugen.

2. Gleichheitsprädikate zu verwenden.

3. Die Klauseln so kurz wie möglich zu schreiben.

4. Einfügen von zusammenhängender Information.

1. Verwenden der Paramodulation wenn Gleichheits units vorhanden sind.

2. Verwenden von UR-Resolution wenn unit Klauseln dabei sind, oder gewonnen werden sollen.

3. Verwenden der Hyperresolution wenn positive Klauseln erzielt werden.

4. Vermeiden von Binary Resolution.

1. Verwenden der SOS Strategie, indem wir in der SOS Liste diejenigen Klauseln einfügen die für die 'special hypothesis' und für die Leugnung dastehen.

2. Die Weight functionen sollen unsere Intuition widerspiegeln über wie man das gegebene Problem lösen könnte.

3. Einfügen von Demodulatoren zum Vereinfachen im Inputfile.

Zum Schluß, ein kurzes Rätsel um die Neugier des Lesers ein bißchen zu erwecken: (Auf einer SPARCstation 1+, kann OTTER dieses Rätsel in weniger als zwei CPU- Sekunden lösen. Dafür werden 281 Klauseln generiert, von welchen 214 aufbewahrt werden.)

DAS JOB RÄTSEL

Es gibt vier Personen: Roberta, Thelma, Steve und Pete.
Sie teilen sich 8 Jobs untereinander.
Jeder besitzt genau zwei Jobs.
Die Jobs sind: Chef, Wächter, Polizist, Pfleger, Priester, Lehrer, Schauspieler und Boxer.
Der Job des Pflegers besitzt ein Mann.
Der Ehemann des Chefs ist der Priester.
Rberta ist nicht Boxer.
Pete hat keine weitere Ausbildung als neun Klassen.
Roberta, der Chef und der Polizist gehen zusammen Golf spielen.

Rätsel: Wer besitzt welchen Job???

Alexandra Pascal 12/08/97