 | ||||||||||||||||||||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||||||||||||||||||||
Glossar 
Forschungsprojekte 
Anbieterverzeichnis 
Datenbanksuche 
Highlights | |||||||||||||||||||||
| Wissensbrowser starten | |||||||||||||||||||||
| |||||||||||||||||||||
| |||||||||||||||||||||
|
| ||||||
|  | |  | |  | |
| ||||||
| ||||||
|  | | ||||
| ||||||
Verfahren |
|
Beispiel für Automatisches Beweisen II |
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| Beschreibung | |||||||||
| |||||||||
Ein Ablauf der Anwendung der oben definierten Regeln sieht folgendermaßen aus: Im ersten Schritt wird ein Knoten mit der Beschriftung ε erzeugt. Es wird nun die erste Klausel als Start-Klausel ausgewählt. Ihre Literale werden zu zwei neuen, vorerst offenen, Söhnen (siehe Abbildung 1).
 Nun wird versucht, die linke Klausel zu schließen. Sie trägt die Beschriftung p(X,Y) . Wir wenden also die Erweiterungsregel an. Dies führt zu zwei neuen Knoten ¬p(a,Z) und ¬p(Z,a) (siehe Abbildung 2). >center> 
Der erste Knoten wird geschlossen und mit *E markiert. Die Substitution X\a wird auf den Baum angewendet. Der zweite "offene" Knoten kann durch den Reduktionsschritt geschlossen werden: Das Literal ¬p(Z,a) ist zu seinem Vater p(a,Y) komplementär. Daher können sie unifiziert werden und die daraus resultierende Substitution Z\a wird angewandt. Der Knoten wird geschlossen und mit *R markiert. Der linke Teil des Baums kann analog analog verarbeitet werden. Daraus resultiert ein geschlossender Baum (Abbildung 3).1  Zurück zum Überblick Automatisches Beweisen im Bereich der Softwareentwicklung Nächster Gliederungspunkt DARWIN | |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
Eintrag kommentieren | ||||
| ||||
 | Übergeordnet | | ||
| ||||
|
| | ||
| ||||
| ||||
| ||||
| ||||
| Beispiel für Automatisches... | ||||
| ||||
| ||||
| ||||
| ||||
| Literaturhinweise | | ||
| ||||
|
| | ||
| ||||
| ||||
| | | ||
| ||||||||||||||
|
