 | ||||||||||||||||||||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||||||||||||||||||||
Glossar 
Forschungsprojekte 
Anbieterverzeichnis 
Datenbanksuche 
Highlights | |||||||||||||||||||||
| Wissensbrowser starten | |||||||||||||||||||||
| |||||||||||||||||||||
| |||||||||||||||||||||
|
| ||||||
|  | |  | |  | |
| ||||||
| ||||||
|  | | ||||
| ||||||
Verfahren |
|
Mögliche Anwendungen von Automatischen Beweisen |
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| Beschreibung | |||||||||
| |||||||||
| Andrei Voronkov hat eine Analyse der möglichen Anwendungen von Automatischem Beweisen für Prädikaten-Logik erster Ordnung, das sind z.B. Verifikation, Hilfestellung bei interaktiven Beweis-Assistenten oder "semantic web", durchgeführt. Er ist zu dem Schluss gekommen, dass sowohl neue Features als auch eine bessere Performance benötigt wird. Er prognostiziert, dass durch Verbesserung der existierenden Algorithmen und Datenstrukturen die Performance verbessert werden kann, jedoch werden weiterhin viele Probleme außerhalb der Möglichkeiten von Automatischem Beweisern liegen. Allerdings gibt es weitere Möglichkeiten die Performance zu verbessern durch zusätzliches implementieren von Theorien. So kann bereits an dem Beispiel der Behandlung von Gleichheit gesehen werden, dass durch geschicktes hinzufügen von Regeln die Performance deutlich gesteigert werden kann. Es gibt jedoch noch weitere Theorien, die in vieler Orts Anwendung finden. Diese Theorien für Automatisches Beweisen umzusetzen wird eins der zentralen Probleme der Zukunft sein, so Voronkov. Hierbei tut sich das Problem auf, dass sich Relationen und Funktionen der unterschiedlichen Theorien überschneiden. Hierfür müssen Strategien entwickelt werden um die Entscheidungs- und Unifikationsalgorithmen zu kombinieren. Oft gibt es auch das Problem, dass die Kombination mehrerer Theorien dazu führt das zentrale Eigenschaften, wie Abgeschlossenheit und Stichhaltigkeit verletzt werden. Hier müssen entsprechende Untermengen der Theorien gefunden werden, bei denen die Kombination der Theorien weiterhin aller wichtigen Anforderungen erfüllt.1
Zusätzlich kann eine Angleichung an die Interaktiven Beweiser geschehen. Dort ist es möglich mit induktiv definierten Datentypen zu arbeiten. Bislang ist dies bei Automatischem Beweisen nicht möglich. In diesem Bereich kann es auch Entwicklungen in Richtung von induktiven Definitionen von Funktionen auf induktiv definierten Datentypen geben oder beschränkte Formen des induktiven Argumentierens. Bislang kann es noch nicht wirklich sinnvoll ausgenutzt werden, das bestimmte Variablen oder Relation nur einen endlichen Wertebereich haben. Hier werden in Zukunft neue Strategien von Nöten sein um damit die Performance zu steigern. Ein ähnliches Problem stelle besondere Quantoren da. Die beispielsweise die Existenz von einer endlichen Anzahl von Elementen mit bestimmten Eigenschaften quantifizieren. Bislang ist eine Übersetzung dieser Quantoren in der Prädikaten-Logik erster Ordnung zwar möglich, jedoch werden die resultierenden Formeln zu groß um sie sinnvoll zu bearbeiten. Hier werden auch neue Wege benötigt um diese zu verarbeiten.1 Ein weiteres häufiges Problem ist das Arbeiten mit vielen Axiomen. Hierbei müssen irrelevante Axiome möglichst Effizient entdeckt werden, so dass die zu verarbeitende Formel schneller verarbeitet werden kann.1 Weiterhin muss die Möglichkeit verbessert werden Beweise zu überprüfen. Die modernen Automatischen Beweiser geben zwar z.T. sehr detaillierte Beweise heraus, jedoch werden bei keinem die Verbereitungsschritte wie Skolemization überprüft. Solange dies nicht möglich ist, sind die Automatischen Beweiser nicht verlässlich genug um sie in der Verfikation von sicherheitskritischen Systemen einzusetzen. Zurück zum Überblick Automatisches Beweisen im Bereich der Softwareentwicklung Nächster Gliederungspunkt Automatisches Beweisen (Fazit) | |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
Eintrag kommentieren | ||||
| ||||
 | Übergeordnet | | ||
| ||||
|
| | ||
| ||||
| ||||
| ||||
| ||||
| Mögliche Anwendungen... | ||||
| ||||
| ||||
| ||||
| ||||
| Literaturhinweise | | ||
| ||||
|
| | ||
| ||||
| ||||
| | | ||
| ||||||||||||||
|
