 |
| | | | | Beschreibung | | Automatische Beweiser arbeiten genau wie Interaktive Beweiser auf Syntax-Ebene. Sie überprüfen die Korrektheit einer Formel indem, sie auf eine Zielklausel hin syntaktisch umformen. Dies geschieht mit Regeln die in einem Kalkül zusammengefasst sind. Das verwendete Kalkül muss hierbei Abgeschlossen und Stichhaltig sein. Das heißt, dass wenn ein Beweis existiert dieser auch gefunden wird und jeder gefundene Beweis auch korrekt ist.
Automatische Beweiser basieren jeweils auf einem speziellen Kalkül. THO1 basiert auf dem Model Elimination Calculus, DARWIN basiert auf dem Model Evolution Calculus und  OTTER2 basiert auf dem Resolution Calculus. Die Kalküle werden z.T. durch weitere Regeln ergänzt um die Ausdrucksstärke zu erhöhen. So können beispielsweise Regeln ergänzt werden um Gleichheit mit überprüfen zu können, oder um effizientere Ableitungen zu erhalten. Model Elimination und und Model Evolution sind Kalküle mit Tableau. Resolution hingegen formt die Formel auf eine Zielklausel hin um.
SETHO, wie oben bereits erwähnt verwendet den Model Elimination Calculus. Dieser Kalkül besitzt alle nötigen Eigenschaften, jedoch benötigt er z.T. für sehr einfache Beweise bereits eine ganze Reihe von Schritten. Um die Länge des Beweises zu vermindern, wurde er bei SETHO mit zusätzlichen Regeln erweitert, die schnellere Ableitungen ermöglichen.1
Automatische Beweiser, im Gegensatz zu Interaktiven Beweisern erledigen das Beweisen vollkommen automatisch. Somit braucht der Anwender nicht in jedem Fall Kenntnisse der zugrunde liegenden Logik zu haben. Der Nachteil ist jedoch, das bislang nur Automatische Beweiser für Prädikaten-Logik erster Ordnung oder Teilmengen davon erstellt wurden, denn nur für diese gibt es effiziente Algorithmen um zu entscheiden ob eine Formel universell wahr ist. Dies hängt mit der Ausdrucksstärke von Prädikaten-Logik erster Ordnung zusammen. Die Prädikaten-Logik erster Ordnung ist bereits nur noch semi-entscheidbar. Dies kann gezeigt werden indem das Leerband-Halteproblem von Turingmaschinen auf das Entscheidungsproblem von Formeln der Prädikaten-Logik erster Ordnung reduziert wird.3 Logiken höherer Ordnung sind unentscheidbar. Daher versucht man den semi-entscheidbaren Raum weitest möglich abzudecken mit den Algorithmen für Prädikaten-Logik erster Ordnung und Erweiterungen. Implementierungen für eingeschränkte Modelle der monadischen Prädikaten-Logik zweiter Ordnung sind auch denkbar. Denn diese ist entscheidbar sofern sie nur die Mengenoperatoren und einige Operatoren auf Wörtern verwendet.
Automatische Beweiser für Prädikaten-Logik erster Ordnung können nicht ohne weiteres erweitert werden, um Formeln aus anderen Logiken zu validieren ohne die Formel zu übersetzen.1 Sie arbeiten vollkommen automatisch. Jegliche Einstellungen müssen vorher gemacht werden. Außerdem haben sie die Möglichkeit eine Zeitbeschränkung einzurichten, so dass der Beweisvorgang gestoppt wird, sollte er diese Beschränkung überschreiten. Die Automatischen Beweiser verbrauchen sehr viel Zeit, wenn es sich bei der Formel um eine nicht erfüllbare Formel handelt. Aufgrund der semi-Entscheidbarkeit der Prädikaten-Logik erster Ordnung, können niemals alle nicht erfüllbaren Formeln falsifiziert werden. Allerdings terminieren die Automatischen Beweiser bereits bei den meisten trivialen nicht erfüllbaren Formeln nicht. Automatische Beweiser sind hoch effiziente Implementierungen von Suchalgorithmen. Sie haben keinerlei Benutzerumgebung, wie es die Interaktiven Beweiser haben. Im Gegensatz zu anderen deduktiven Verfahren, wie z.B. Model Checking, sind Automatische Beweiser in der Lage, einen Beweis zu konstruieren.
Zurück zum Überblick Automatisches Beweisen im Bereich der Softwareentwicklung
Nächster Gliederungspunkt Anforderungsanalyse beim Automatischen Beweisen
| |
| | | | | | | | | | | | | Zu dieser Seite wurden noch keine Kommentare oder Bewertungen abgegeben. |
|
| | | | | | | | Automatische Beweiser | | | | |  | Untergeordnet | | | | | | | | | Literaturhinweise | | | | | | | | | | | | | |
|
Glossar 
Forschungsprojekte 
Anbieterverzeichnis 
Datenbanksuche 
Highlights 
Eintrag kommentieren
