Unter Theorem Proving versteht man ganz allgemein die Vorgehensweise, Behauptungen auf der Grundlage von Beweissystemen und mit Hilfe von Programmen (daher auch Automatisiertes Theorem Proving, ATP) zu verifizieren. Die Sprache, in der Vermutungen, Hypothesen und Axiome (allgemein spricht man von Formeln) verfasst werden, ist eine logische Sprache, oft basierend auf der klassischen Logik erster Ordnung, aber möglicherweise auch basierend auf einer nicht-klassischen Logik und/oder einer Logik höherer Ordnung. Diese Sprachen lassen exakte formale Aussagen der notwendigen Informationen zu, die anschließend mit Hilfe des ATP-Systems behandelt werden können. Dieser Formalismus ist die grundlegende Stärke des ATP: Es gibt einerseits keine Zweideutigkeiten in den Aussagen über das Problem, wie es bei informellen sprachlichen Beschreibungen häufig vorkommt. Anwender sind gezwungen, das vorliegende Problem präzise zu beschreiben und dieser Vorgang an sich führt bereits zu einem klareren Verständnis des Problemumfelds. Außerdem ermöglicht dies dem Anwender auch, das Problem in einer für das ATP-System passenden Art und Weise zu formulieren.
Die von ATP-Systemen erzeugten Beweise beschreiben exakt, wie und warum die Vermutung aus den Axiomen und Hypothesen folgt. Die Beweisführung erfolgt für jedermann nachvollziehbar und ist sogar anderen Programmsystemen zugänglich. Der entstandene Beweis ist dabei nicht nur ein überzeugendes Argument dafür, dass die Vermutung eine logische Folgerung der Axiome und Hypothesen ist, sondern er beschreibt häufig auch einen Prozess, der für eine Problemlösung implementiert werden kann. Im Beispiel des Zauberwürfels, das in Theorem Proving (Motivation) angeführt wird, würde der Beweis etwa die Folge von Zügen beschreiben, die nötig sind, um die Aufgabe zu lösen.
ATP-Systeme sind äußerst mächtige Programmsysteme, mit denen selbst schwierigste Probleme gelöst werden können. Wegen dieses gewaltigen Funktionsumfangs muss ihre Anwendung und ihre Ausführung von Experten für den jeweiligen Anwendungsbereich gesteuert werden, damit die entsprechenden Aufgaben in angemessener Zeit bearbeitet werden können.
Daher werden ATP-Systeme trotz ihres Namens oft von solchen Anwendungsexperten in interaktiver Weise angewandt. Die Interaktion kann sich einerseits auf einer sehr detaillierten Stufe abspielen, wobei der Anwender die einzelnen Folgerungen des Systems steuert, oder aber auf einer wesentlich höheren Abstraktionsebene, auf der der Anwender bestimmt, welche zwischengeschalteten Lemmata bewiesen werden müssen, um eine Vermutung zu beweisen. Dabei entsteht oft eine synergetische Beziehung zwischen den ATP-Anwendern und den Systemen selbst: Das System benötigt eine exakte Problembeschreibung in einer logischen Form, so dass der Benutzer gezwungen ist, das Problem sorgfältig zu durchdenken, um eine adäquate Formulierung zu ereichen.
Das System versucht, das Problem zu lösen und erzeugt mit dem Beweis - sofern er gelingt - eine sinnvolle Ausgabe. Falls der Beweis misslingt, kann der Anwender steuernd eingreifen und versuchen, Zwischenergebnisse zu beweisen, oder die Formeln untersuchen, um zu überprüfen, ob das Problem richtig beschrieben wurde. Anschließend beginnt der Prozess von vorne.
|
Glossar 
Forschungsprojekte 
Anbieterverzeichnis 
Datenbanksuche 
Highlights 
Eintrag kommentieren
