Software-Projekt SW06

- N a v i g a t i o n - - - - - - - -

Theorem-Proving durch Evolutionäre Algorithmen unter besonderer Berücksichtigung des

Genetic Programming

- - - - - - - - - - - - - - - - - - - -

- - - - - - - -

Genetic Reasoning

Die Integration eines GP/HP-Systems in ein Mathematik-Programm (siehe Software-Projekt SW05) eröffnet die Möglichkeit, spezielle mathematische Fragestellungen mit diesen Problemlösungsmethoden zu bearbeiten. Faktisch bedeutet dies die Suche nach neuen Algorithmen zur Lösung mathematischer Probleme, unabhängig davon, ob bereits Algorithmen für diese Probleme existieren.

Eng verbunden mit dieser Sichtweise sind Versuche, evolutionäre Verfahren als Suchstrategien zu Theorembeweisen einzusetzen, wie das Genetic Reasoning von Nordin & Banzhaf, bei dem es sich um eine Anwendung des CGP Handelt. Ein Beweis wird als Programm betrachtet, das eine Aussage in Axiome transformiert, sodass die Ausführung des Programms dem Beweisablauf entspricht.

Eine Zielrichtung dieses Ansatzes ist die Prüfung der Eignung von GP für verschiedene Logikarten und Domänen. In der Arbeit "Genetic Reasoning" von Nordin & Banzhaf wurde neben der klassischen, zwei-wertigen Logik auch die drei-wertige Logik von Kleene betrachtet, während als Domänen Arithmetik und Programm-Verifikation betrachtet wurden. Die Anwendungsbreite dieses Ansatzes ist jedoch wesentlich breiter, wobei langfristig auf die Domäne "theoretische Physik" hingearbeitet werden soll.

Agenten-orientierter Ansatz

Ein Ansatz wäre die Integration eines GP-Systems in den agenten-orientierten Ansatz verteilter mathematischer Dienste von Franke et al., da das GP-System in einen Agenten leicht gekapselt werden kann, der anderen Agenten seine Suchdienste anbietet. Dieser Ansatz erscheint effizienter als die Erweiterung bestimmter Theorem-Prover durch evolutionäre Verfahren, da in einem solchen Szenario zunächst geeignete Theorem-Prover ausgesucht werden müssen. Eine Implementierung wäre demgegenüber nur ein technisches Problem, da viele der Theorem-Prover in Lisp geschrieben sind, und da entsprechende Lisp-Implementierungen von GP-Systemen vorliegen. Die Implementierung eines CGP/CHP-Theorem-Provers ist demgegenüber eine anspruchsvollere Aufgabe, da das zu lösende Problem zunächst reformuliert werden muss, um mit einer Basismenge von logischen Operatoren als Maschinenbefehlen gelöst zu werden.

OpenMath

Der agentenorientierte Ansatz von Franke et al. steht im Zusammenhang mit OpenMath, einer offenen Sprache zur repräsentation und Kommunikation von Mathematik. Die Architektur von OpenMath besteht aus einem Private-Layer, einem Abstract-Layer und einem Communication-Layer, wobei in dem Abstract-Layer OpenMath-Objekte repräsentiert werden. Ein Teilprojekt des Genetic Reasoning könnte auf dieser Architektur aufbauen, indem beispielsweise OpenMath-Objekte im Communication-Layer übersetzt werden, dass ein externes GP/HP- oder CGP/CHP-System Suchoperationen nach Programmen durchführen kann, die als Beweisvorschläge interpretiert werden können.

OpenMath-Objekte im Abstract-Layer können auch durch EA-Operationen manipulierbar werden, sodass komplexe Gesamtstrategien in Verbindung mit externen CGP/CHP-Systemen durchführbar werden, die eine Koevolution von Problem und Problemlösungsvorschlag beinhalten (siehe Software-Projekt SW10).

Theoremproving innerhalb Mathematikprogramme

Ein anderer Ansatz wäre als Erweiterung von GP-Systemen innerhalb von Mathematik-Programmen (siehe Software-Projekt SW05), da z.B. mit Theorema ein Theorem-Prover innerhalb Mathematica zur Verfügung steht, was jedoch aufgrund des kommerziellen Mathematikprogrammes Mathematica nicht im Vordergrund stehen soll.

Referenzen

Franke A., Hess S.M., Jung Ch. G., Kohlhase M., Sorge V.: Agent-Oriented Integration of Distributed Mathematical Services.

Nordin, Peter; Banzhaf, Wolfgang: Genetic Reasoning - Evolving Proofs with Genetic Search. Dept. of CS, University of Dortmund, SysReport 1996.

Nordin, Peter; Eriksson, Anders; Nordahl, Mats: Genetic Reasoning: Evolutionary Induction of Mathematical Proofs. In: Poli et al. (1999), S. 221 - 231.

Poli, R.; Nordin, P.; Langdon, W.B.; Fogarty, T.C. (eds.): Genetic Programming, Second European Workshop, EuroGP'99. Springer Verlag, LNCS 1598, S. 65 - 82, 1999.

Zum Seitenanfang

Dokument zuletzt geändert am 05.12.1999