 |
| | | | | Beschreibung | | Als Beispiel sei an dieser Stelle Model Elimination näher betrachtet. Im Gegensatz zu dem Resolution Kalkül arbeitet die in SETHO verwendete Version des Model Eliminations Kalküls mit einer Baumstruktur, anstatt neue Formeln aus den alten zu generieren. Dieser Baum sieht so aus, dass die Knoten mit Literalen beschriftet sind. Die Beschriftungen von Geschwistern gehören zu der selben Instanz einer Klausel. Wenn eine Menge von Klauseln {C1,..., Cn} ist, dann konstruieren wir T als Baum für S durch 3 Deduktionsregeln.1
1. Initial besteht der Baum nur aus der Wurzel mit der Beschriftung ε . Eine Start-Klausel c ∈ S wird ausgewählt und ihre Literale bilden die Kinder der Wurzel. Alle Blätter werden als "offen" markiert.
2. Erweiterungsschritt: Wähle ein "offenes" Blatt L aus T. Wähle nun ein Literal c ∈ S so, dass ein Literal L' aus unifiziert werden kann mit L und komplementär zu L ist (σL=¬σL' ). Füge jetzt die Literale aus als neue Kinder von L ein. Markiere den neuen Knoten als "geschlossen", die anderen als "`offen"'. Wende die Substitution σ auf den ganzen Baum an.
3. Model Elimination Reduktionsschritt: Wenn ein Knoten N mit der Beschriftung L einen Vorgängerknoten mit der Beschriftung L' hat, so das L und L' komplementär mit dem größten allgemeinen Unifikator σ sind, dann wende σ auf den ganzen Baum an und markiere N als "geschlossen".
Wenn ein geschlossener Baum, also ein Baum bei dem alle Knoten als "geschlossen" markiert sind, für S konstruiert werden kann, dann ist S nicht erfüllbar.
In Schumann ist ein Beispiel für die Anwendung dieses Kalküls gegeben:
Es wird folgende Formel betrachtet: ∀x∀y : (p(x,y) ∨ p(y,x)) → ∀v∃z(p(v,z) ∧ p(z,v)). Diese Formel sagt aus, dass wenn ein Paar von Objekten aus einem Wertebereich die Binäre Operation p(x,y) oder ihr Inverses p(y,x) erfüllt wird, gibt es für jedes Objekt aus diesem Wertebereich ein Objekt gibt, so dass beide Relationen erfüllt werden. Die negierte Version dieser Formel sieht in CNF (clausal normal form) folgendermaßen aus: (p(x,y) ∨ p(y,x)) ∧ (¬p(a,z) ∨ ¬p(z,a)). Hierbei ist a eine  Skolemkonstante. Eine Skolemkonstante entsteht bei der Umformung in CNF. Diese Umformung sorgt für eine Darstellung der Formel ohne Quantoren. In der CNF sind alle Variablen implizit allquantifiziert. Variablen, die existenzquantifiziert waren, werden durch Skolemkonstanten ausgedrückt. Sollte eine Quantifizierung der Form ∀X1... ∀Xn∃y vorgelegen haben, so wird anstatt einer Skolemkonstante eine Skolemfunktion a(X1,...,Xn) geschrieben. In der Syntax von SETHO sieht das dann folgendermaßen aus:
p(x,y) ; (y.x) ←.
← p(a,z) , p(z,a).
Zurück zum Überblick Automatisches Beweisen im Bereich der Softwareentwicklung
Nächster Gliederungspunkt Beispiel für Automatisches Beweisen II
| |
| | | | | | | | | | | | | Zu dieser Seite wurden noch keine Kommentare oder Bewertungen abgegeben. |
|
| | | | |  | Übergeordnet | | | | | | | | | | | Beispiel für Automatisches... | | | | | | Literaturhinweise | | | | | | | | | | |
|
Glossar 
Forschungsprojekte 
Anbieterverzeichnis 
Datenbanksuche 
Highlights 
Eintrag kommentieren
