 |
| | | | | Beschreibung | | Interaktive Beweiser sind Computerprogramme, die in der Lage sind, Formeln einer bestimmten Logik zu verarbeiten und den Benutzter dabei zu unterstützen, die Gültigkeit der Formel festzustellen. Dies geschieht auf Syntax-Ebene. Hierfür werden Regeln aus einem Kalkül auf die entsprechende Formel angewandt. Dies geschieht Schritt für Schritt, stets in Interaktion mit dem Benutzter. Mit solchen Interaktiven Beweisern ist es möglich Beweise für Formeln zu finden, die in Logiken mit höherer Ordnung geschrieben sind. Außerdem bieten sie oft die Möglichkeit an bereits geführte Beweise mit einzubeziehen, wenn neue Formeln bewiesen werden sollen. Der Vorteil beim Einsatz von Interaktiven Beweisen ist die Unterstützung und Kontrolle bei den Umformungen. Interaktive Beweiser formen Formeln durch Anwendung von Regeln aus einem Kalkül um und überprüfen dadurch ihre Gültigkeit. Diese Umformung geschieht durch den Benutzer, der angibt, welche Regeln des Kalküls verwendet werden. Der Interaktive Beweiser sorgt dann dafür, dass die Regel angewendet wird und zeigt die zu bearbeitende Restformel an. Interaktive Beweiser sind meist leicht auf andere Logiken erweiterbar, indem einfach ein neuer Kalkül als Regelmenge mit eingebunden wird (Anforderung 5).
Leider gibt es auch einige Nachteile. So ist es meist nötig jeden Schritt per Hand auszuführen, wodurch das Finden von komplizierten Beweisen oft viel Zeit benötigt (Anforderung 1). Oft ist das Bedienen auch nicht ohne größere Kenntnisse möglich. Der Benutzer muss stets Kenntnisse über den verwendeten Kalkül haben. Außerdem ist es z.T. nötig auch die Implementierung des Interaktiven Beweisers zu kennen, da es sonst nur schwer möglich ist, einen bestimmten Beweis damit umzusetzen.
Bekannte Interaktive Beweiser sind  Isabelle , NuPrl, PVS und HOL. PVS und Isabelle wurden z.B. für die Verifikation von Compilern, Protokollen und Hardware bereits erfolgreich eingesetzt.1
Als Beispiel sei hier der Beweis für A → A in Isabelle angeführt. Dies ist offensichtlich eine Tautologie. In Isabelle muss zuerst ein Goal definiert werden. Dies geschieht durch goal thy "A --> A";. Hierbei ist thy die verwendete Theorie, in diesem Fall Prädikaten-Logik erster Ordnung. Das zweite Argument ist die zu überprüfende Formel. Nun wenden wir die Regel impI an, die besagt: Um A → A zu validieren, validiere A unter der Annahme, dass A gilt. by (rtac impI 1); sorgt dafür, dass die Regel angewendet wird. Hier sieht man deutlich, dass auch triviale Schritte bei Interaktiven Beweisern explizit durchgeführt werden müssen. Wir lösen nun also auf, indem wir unser Annahmen einbringen. by (atac 1);. Nun kann dieses Theorem abgespeichert werden mit z.B. mit qed "selfimp";. Diese Regel wird nun den bereits in thy vorhanden Regeln hinzugefügt und kann bei späteren Beweisen mit selfimp referenziert werden. Isabelle ist in der Lage, Beweise als LaTeX-Dokumente auszugeben. Hierzu können auch bestimmte Formatierungen und Kommentare mit in den Beweis eingebaut werden. Dies ist ein großer Vorteil von Interaktiven Beweisern.
Aus der Natur von Interaktiven Beweisern ergibt sich bereits eine gute Lesbarkeit der Beweise (Anforderung 4). Die Ausdrucksstärke ist im Vergleich zu anderen Methoden sehr hoch (Anforderung 2). Es ist mit Interaktiven Beweisern möglich Beweise in höherordriger Logik zu führen. Dies geht jedoch zu lasten der Zeit, die für einen Beweis benötigt wird (Anforderung 1). Die produzierten Beweise sind korrekt (in ihrem Kalkül). Der Interaktive Beweiser überprüft die Korrektheit, der durchgeführten Schritte während des Führens des Beweises.
Zurück zum Überblick Automatisches Beweisen im Bereich der Softwareentwicklung
Nächster Gliederungspunkt Automatische Beweiser
| |
| | | | | | | | | | | | | Zu dieser Seite wurden noch keine Kommentare oder Bewertungen abgegeben. |
|
| | | | |  | Übergeordnet | | | | | | | | | | | Interaktive Beweiser | | | | | | Literaturhinweise | | | | | | | | | | |
|
Glossar 
Forschungsprojekte 
Anbieterverzeichnis 
Datenbanksuche 
Highlights 
Eintrag kommentieren
