LeanCop, ein einfacher Beweiser für PL1

LeanCop,
ein einfacher Beweiser für PL1
Michael Merk
Überblick
Vorteile von LeanCop
●
Beispiele
●
Konnektionsmethode
●
Vorstellung und Erklärung des Prolog-Codes
●
Performance
●
Vorteile von LeanCop
Theorembeweiser für klassische PL1.
●
Basiert auf der Konnektionsmethode
●
Minimalversion hat nur 333 bytes.
●
für die wichtgsten Prolog-Systeme verfügbar
●
Verhältnismässig starke Leistung.
●
Einfach zur Erforschung neuer Suchtechniken zu
ändern und in Anwendungen zu integrieren.
●
Einfaches Klausel-Eingabeformat
●
ist kostenlos und frei erhältlich
●
Überblick
Vorteile von LeanCop
●
Beispiele
●
Konnektionsmethode
●
Vorstellung und Erklärung des Prolog-Codes
●
Performance
●
Beispiel - Äquivalenz
(ƎX (p=>f(X)) Λ ƎX (f(X)=>p)) => ƎX(p<=>f(X))
(p Λ ¬f(a)) V (f(b)Λ¬p) V (pΛf(X)) V (¬pΛ¬f(X))
{{p,¬f(a)},
{f(b),¬p},
{p,f(X)},
[[p,-f(a)],[f(b),-p],[p,f(X)],[-p,-f(X)]]
{¬p,¬f(X)}}
Überblick
Vorteile von LeanCop
●
Beispiele
●
Konnektionsmethode
●
Vorstellung und Erklärung des Prolog-Codes
●
Performance
●
Konnektionsmethode
●
●
Bilde Matrix aus Klauseln
Überprüfe (Top-Down-)
Pfade:
– Wenn es einen Pfad
gibt, der kein Paar von
komplementären
Literalen enthält, dann
ist die Klauselmenge
erfüllbar.
Beispiele zum
Erweiterungsschritt
?- g.
?- g(x).
g:- a,b,c.
g(x):-a,b,c(f(x)).
a.
c.
a.
b.
b:- d,e.
c(x):- g(h(x).
d.
e.
g(h(f(x)):- a,b,c(f(g(f(x)))
c(f(x)):- g(h(f(x))
Überblick
Vorteile von LeanCop
●
Beispiele
●
Konnektionsmethode
●
Vorstellung und Erklärung des Prolog-Codes
●
Performance
●
Code(1)
prove([C|M]) :- !, Time1 is cputime,
prove([C|M],1),
Time2 is cputime,
Time is Time2-Time1, print(Time).
prove(F) :-Time1 is cputime, make_matrix(F,M),
prove(M,1), Time2 is cputime,
Time is Time2-Time1, print(Time).
//Grosse Schleifen zwecks Laufzeitmessung
Code(2)
prove(Mat,PathLim) ://Startwert
append(MatA,[Cla|MatB],Mat),
\+member(-_,Cla),
append(MatA,MatB,Mat1),
prove([!],[[-!|Cla]|Mat1],[ ],PathLim).
prove(Mat,PathLim) ://setzt Iterative deepening um
\+ground(Mat), PathLim1 is PathLim+1,
prove(Mat,PathLim1).
prove([],_,_,_).
// Abbruchbedingung
Append
●
append([a], [b,c], L) führt zu L = [a, b, c ].
●
Falls erste beiden Argumente nicht angegeben,
haben sie beim Backtracking alle Möglichkeiten
append(A,[X|B], [a,b,c]) und append(A,B,C) führt zu
X=a, C=[b,c]
X=b, C=[a,c]
X=c, C=[a,b]
so wählt man jedes Element aus und gibt den Rest
der Liste zurück
Code(3)
prove([Lit|Cla],Mat,Path,PathLim) :(-NegLit=Lit;-Lit=NegLit) ->
//Negation vom Literal
( member(NegL,Path),
unify_with_occurs_check(NegL,NegLit);
append(MatA,[Cla1|MatB],Mat), copy_term(Cla1,Cla2),
append(ClaA,[NegL|ClaB],Cla2),
unify_with_occurs_check(NegL,NegLit),
append(ClaA,ClaB,Cla3),
( Cla1==Cla2 ->
append(MatB,MatA,Mat1);
length(Path,K), K<PathLim,
append(MatB,[Cla1|MatA],Mat1)
),
prove(Cla3,Mat1,[Lit|Path],PathLim)
),
prove(Cla,Mat,Path,PathLim).
Überblick
Vorteile von LeanCop
●
Beispiele
●
Konnektionsmethode
●
Vorstellung und Erklärung des Prolog-Codes
●
Performance
●
Performance
●
●
●
leanCoP wurde auf der TPTP Bibliothek (Sutcliﬀe and Suttner, 1998) auf
allen 2200 als wahr bekannten Problemen in Klauselform.
Alle Tests wurden auf einer SUN Ultra10, 128 Mbytes mit eclipse Prolog
version 3.5.2.
Das Zeitlimit wurde auf 300 Sekunden gesetzt.
Performance - Vergleich
Quellen
www.leancop.de - die Internetseite zum Prover von Jens Otten
and Wolfgang Bibel mit ausführlichen Beschreibungen und
SourceCode
„Matrixverfahren (Konnektionsmethode)“ - Kurt Eberle
www.cl.uni-heidelberg.de/kurs/ss04/deduktion/MATRIX.DOC
Noch Fragen ?
Vielen Dank !
[email protected]

Download Report