Dokumentation der Praktikumsaufgabe „prove“
Das Programm wurde unter SUSE Linux SWI Prolog geschrieben.
In der Prolog Datei „prove.pl“ sind zwei Beweisklauseln realisiert prove und prove1, prove arbeitet mit der Klauselform(Konjunktive Normalform), prove1 arbeitet mit der dualen Klauselform(Disjunktive Normalform). Nur die Ausgangsformeln für die Resulution sind unterschiedlich, die Resulution ist dieselbe.
Bei der Erstellung des Programms hab ich darauf geachtet das die Normalform möglichst kurz ist(rausschneiden von Konstanten, doppelten Vorkommen), da die Zeit die die Resulution braucht um die Formel zu beweisen exponential mit der Zeit zunimmt.
Es wurden viele Cuts zur Optimierung Gesetz, um das Programm schnell zu machen.
Wieso funktioniert Resulution sowohl mit Konjunktiver als auch mit Disjunktiver Normalform?
Die Resulution beruht auf der Formel: (aÚF1)Ù(ØaÚF2)= (aÚF1)Ù(ØaÚF2)Ù(F1ÚF2)
Beweis:
|
a |
F1 |
F2 |
(aÚF1)Ù(ØaÚF2) |
(aÚF1)Ù(ØaÚF2)Ù(F1ÚF2) |
|
0 |
0 |
0 |
0 |
0 |
|
0 |
0 |
1 |
0 |
0 |
|
0 |
1 |
0 |
1 |
1 |
|
0 |
1 |
1 |
1 |
1 |
|
1 |
0 |
0 |
0 |
0 |
|
1 |
0 |
1 |
1 |
1 |
|
1 |
1 |
0 |
0 |
0 |
|
1 |
1 |
1 |
1 |
1 |
Wenn die leere Klausel entsteht war die Ursprungsresulution aÙØa, diese Formel ist unerfüllbar und damit wird die gesamte Konjunktive Normalform unerfüllbar.
Für die Disjunktive Formel gilt die Formel: (aF1)Ú(ØaF2)= (aF1)Ú(ØaF2)Ú(F1F2)
Beweis:
|
a |
F1 |
F2 |
(aF1)Ú(ØaF2) |
(aF1)Ú(ØaF2)Ú(F1F2) |
|
0 |
0 |
0 |
0 |
0 |
|
0 |
0 |
1 |
1 |
1 |
|
0 |
1 |
0 |
0 |
0 |
|
0 |
1 |
1 |
1 |
1 |
|
1 |
0 |
0 |
0 |
0 |
|
1 |
0 |
1 |
0 |
0 |
|
1 |
1 |
0 |
1 |
1 |
|
1 |
1 |
1 |
1 |
1 |
Wenn die leere Klausel entsteht war die Ursprungsresulution aÚØa, diese Formel ist allgemeingültig und damit wird die gesamte Disjunktive Normalform allgemeingültig.
Wenn das Resulutionsverfahren bei der Erzeugung der leeren Klausel false(bzw. fail) ausgibt, ist die Disjunktive Normalform allgemeingültig und die Konjunktive Normalform unerfüllbar. Dieses Ergebnis wird negiert und man erhält das richtige Ergebnis.
(Nicht von den ganzen Negationen stören lassen)
Also Eingabe: prove(P,F) bzw. prove1(P’,F’)
à PàF=(ØP)ÚF=(Ø(ØFÙP))
Bearbeitet wird die Formel: (ØFÙP) (ØF’ÙP’)
leere Klausel gefunden Ausgabe resulution(X) fail
(ØFÙP) unerfüllbar (ØF’ÙP’) allgemeingültig
(Ø(ØFÙP)) allgemeingültig (Ø(ØF’ÙP’)) unerfüllbar
Vorteile bei den zwei Beweisklauseln
Die Resulution ist mit der Klauselform(Konjunktive Normalform) zum schnellen Beweisen geeignet, da dann eine leere Klausel gefunden wird und nicht alle Terme, auf die Möglichkeit Resulutionen bilden zu können, überprüft werden müssen.
Andersrum bei der Disjunktiven Normalform. Die Resulution ist mit der dualen Klauselform zum schnellen Zeigen der Unerfüllbarkeit geeignet, da dann eine leere Klausel gefunden wird und nicht alle Terme, auf die Möglichkeit Resulutionen bilden zu können, überprüft werden müssen.
Leider konnte ich dies nicht Testen, da alle Formeln viel zu schnell abgearbeitet wurden um die Zeit zu messen(selbst auf meinen langsamen Linux Rechner).
Datenverlaufsgraphen
von prove:
Liste
mit Formeln(z.B.[neg(a or b),a and f]) fuegeListeZusammen(X,Z) entfernt die
Kommas und ersetzt sie durch „and“ Liste
der Konjunktive Normalform (z.B.
[(a or b or a), (a or neg a), (a or a or b)] ) Liste von Listen der Konjunktive Normalform (z.B.
[[a, b,a], [a, neg a], [a, a, b]] )
EleminateOrL1(A,B) ersetzt die
„oder“ durch Kommas „ ,“ in Unterlisten
Datenverlaufsgraph
von Klauselform:
Der Datenverlaufsgraph von duale Klauselform ist
ähnlich(wird hier deshalb nicht aufgeführt) nur das „and“ und „or“, Disjunktion
und Konjunktion vertauscht sind und die „1“ am Ende von den Namen fehlt.
Die Klauseln entfDoppelteVorkommen(+X,-Y) und entfKonstanten(+X,-Y)
dienen nur zur Optimierung(Verkürzung) der ausgangsformel für die Resulution.
Die Klauseln fuegeListeZusammen(X,Z), eleminateAnd1([B],C) und eleminateOrL1(C,D) dienen zur Veränderung der Form der Formel(z.B. von Formel in Liste).