 |
| | | | | Beschreibung | | DARWIN ist ein Automatischer Beweiser der neuesten Generation. Er basiert auf dem Model Evolution Kalkül. Der Model Evolution Kalkül ist ein Kalkül, der die DPLL Prozedur (benannt nach ihren Erfindern Davis, Putnam, Logemann und Loveland) so erweitert, dass die komplette Prädikaten-Logik erster Ordnung validiert werden kann.
Die Idee diesen Kalkül zu verwenden hängt damit zusammen, dass die DPLL Prozedur sehr beliebt ist bei SAT-Solvern. Daher sind dort bereits viele performante Techniken entwickelt worden um die DPLL Prozedur zu implementieren. Außerdem sind bei DARWIN viele der Techniken verwendet worden, die auch bei anderen Automatischen Beweisern Anwendung finden, wie z.B. Termindizierung, "subterm sharing", "redundancy elimination".1
DPLL versucht ein Modell einer Formel zu finden indem initial angenommen wird, alle Literale seien falsch. Inkrementell werden diese nun verändert, bis die Interpretation ein Modell der Formel ist, oder alle Kombinationen durchprobiert wurden ohne ein Modell gefunden zu haben. Das Ziel des Model Evolution Kalküls ist es ein Herbrand Modell einer gegebenen Menge Φ von Klauseln zu konstruieren. Hierzu verwaltet der Kalkül während der Ableitung einen Kontext Λ , eine endliche Menge von Literalen (eventuell in negierter Form). Dieser Kontext ist eine endliche und kompakte Repräsentation einer Herbrand Interpretation IΛ. Diese Interpretation ist ein Kandidat für ein Modell von Φ. Es ist allerdings nicht unbedingt ein Modell von Φ, denn es kann sein, dass einige Klauseln von Φ nicht erfüllt werden. Hier kommen die Regeln des Kalküls ins Spiel. Sie entdecken den Missstand und versuchen dann IΛ. so zu verändern, dass es zu einem Modell von Φ wird. Zusätzlich enthält der Kalkül noch Regeln um dieses Verfahren zu beschleunigen indem die Menge der Klauseln vereinfacht wird.1
Der verwendete Kalkül ist sehr kompliziert. Die produzierten Beweise sind daher nur unter erheblichem Aufwand nachzuvollziehen (Anforderung 4). Dafür werden jedoch Ergebnisse schnell geliefert (Anforderung 1). Die Ausdruckstärke umfasst die Gesamte Prädikaten-Logik erster Ordnung, daher ist Anforderung 2 erfüllt (in der Domäne der Automatischen Beweisern). Über die Verlässlichkeit (Anforderung 3) lässt sich zu diesem Zeitpunkt der Entwicklung noch nichts sagen. Das Projekt befindet sich noch in einer Prototypenphase.
Zurück zum Überblick Automatisches Beweisen im Bereich der Softwareentwicklung
Nächster Gliederungspunkt Beispielanwendung Amphion | |
| | | | | | | | | | | | | Zu dieser Seite wurden noch keine Kommentare oder Bewertungen abgegeben. |
|
| | | | |  | Übergeordnet | | | | | | | | | | | DARWIN | | | | | | Literaturhinweise | | | | | | | | | | |
|
Glossar 
Forschungsprojekte 
Anbieterverzeichnis 
Datenbanksuche 
Highlights 
Eintrag kommentieren
