% Autor: MB % Version JUL 2016 /* Grundsätzlich beziehen sich die folgenden Regeln auf Tableaus und Belegungen von Variablen in einem Herbrand-Universum. Vgl. zum Vorgehen: Fitting, Melvin. First-Order Logic and Automated Theorem Proving. Verwendet werden die Systemprädikate: var/1, member/2, atomic/1, functor/3, arg/3, nonvar/1, append/3, retract/1, asert/1, dynamic/1, op/3 */ :- dynamic(funktionenzaehler/1). % 1. syntaktische Kategorien und Belegung von Variablen % sowie ein damit umgehendes Unifikationsverfahren, das benötigt wird, um an % den geeigneten Stellen in Tableaus dieselben Terme zu verwenden (etwa genau % den Term universell zu spezialisieren, der zuvor existentiell spezialisiert wurde) % Definition der Junktoren ?- op(100,fy,neg). % Negation ?- op(160,xfy,und). % Konkunktion ?- op(160,xfy,oder). % Disjunktion ?- op(160,xfy,imp). % Materiale Implikation ?- op(160,xfy,nand). % Sheffer-Strich ?- op(160,xfy,aequi). % Äquivalenz % Konkunktive Formeln konjunktiv( _ und _ ). konjunktiv(neg(_ oder _)). konjunktiv(neg(_ imp _)). konjunktiv(neg(_ nand _)). konjunktiv( _ aequi _). % Disjunktive Formeln disjunktiv(_ oder _). disjunktiv(neg(_ und _)). disjunktiv(_ imp _). disjunktiv(_ nand _). % Negationen bzw. einstellige Formeln einstellig(neg neg _). einstellig(neg true). einstellig(neg false). % Komponenten von Formeln komponenten(X und Y, X, Y). komponenten(neg(X und Y),neg X, neg Y). komponenten(X oder Y, X, Y). komponenten(neg(X oder Y), neg X, neg Y). komponenten(X imp Y, neg X, Y). komponenten(neg(X imp Y), X, neg Y). komponenten(X nand Y, neg X, neg Y). komponenten(X aequi Y, X imp Y, Y imp X). komponenten(neg neg X, X). komponenten(neg true, false). komponenten(neg false, true). % syntaktische Kategorien variable(var(_)). komplex(X) :- functor(X,_,N), N > 0. literal(X) :- not(konjunktiv(X)), not(disjunktiv(X)), not(einstellig(X)), not(universell(X)), not(existentiell(X)). atomareFormel(X) :- literal(X), X \= neg _. zweistelligerJunktor(X) :- member(X, [und, oder, imp, aequi, nand]). % Belegungen/Interpretationen im Herbrand-Universum partielleBelegung(Term, Umgebung, Wert) :- member([Term,NeuerTerm],Umgebung), partielleBelegung(NeuerTerm, Umgebung, Wert). partielleBelegung(Term,_,Term). /* Tableaus werden später als Listen modelliert, aus denen dann Formeln entfernt werden können bzw. zu denen Formeln hinzugefügt werden; Variablen werden evtl. aus Listen von Variablen oder aus Belegungslisten entfernt */ kommtVorIn(Term1, Term2, Umgebung) :- partielleBelegung(Term2, Umgebung, Wert), (Term1 == Wert; not(variable(Wert)),not(atomic(Wert)), inFunktor(Term1,Wert,Umgebung)). kommtNichtVorIn(X,Y) :- var(Y), X \== Y. kommtNichtVorIn(_,Y) :- nonvar(Y), atomic(Y). kommtNichtVorIn(X,Y) :- nonvar(Y), komplex(Y), functor(Y,_,Stelligkeit), kommtNichtVorIn(Stelligkeit,X,Y). kommtNichtVorIn(Stelligkeit,X,Y) :- Stelligkeit > 0, arg(Stelligkeit,Y,Argumente), kommtNichtVorIn(X,Argumente), Stelligkeit1 is Stelligkeit - 1, kommtNichtVorIn(Stelligkeit1,X,Y). kommtNichtVorIn(0,_,_). inFunktor(Variable, Belegung, Umgebung) :- Belegung =.. [_|Liste], inListe(Variable, Liste, Umgebung). inListe(X, [K|_], Umgebung) :- kommtVorIn(X, K, Umgebung). inListe(X, [_|R], Umgebung) :- inListe(X,R,Umgebung). entferneVorkommnis(_,[],[]). entferneVorkommnis(X, [Y|Rest], NeuerRest) :- X == Y, entferneVorkommnis(X,Rest,NeuerRest). entferneVorkommnis(X, [Y|Rest], [Y|NeuerRest]) :- X \== Y, entferneVorkommnis(X,Rest,NeuerRest). % Unifikation wird benötigt, um auf geeignete Variablen zu spezialisieren unifiziere(X,Y) :- var(X), var(Y), X = Y. unifiziere(X,Y) :- var(X), nonvar(Y), kommtNichtVorIn(X,Y), X = Y. unifiziere(X,Y) :- var(Y), nonvar(X), kommtNichtVorIn(Y,X), Y = X. unifiziere(X,Y) :- nonvar(X), nonvar(Y), atomic(X), atomic(Y), X = Y. unifiziere(X,Y) :- nonvar(X), nonvar(Y), komplex(X), komplex(Y), unifiziereTerme(X,Y). unifiziereTerme(X,Y) :- functor(X,Ausdruck,Stelligkeit), functor(Y,Ausdruck,Stelligkeit), unifiziereArgumente(Stelligkeit,X,Y). unifiziereArgumente(N,X,Y) :- N > 0, unifiziereArgument(N,X,Y), N1 is N - 1, unifiziereArgumente(N1,X,Y). unifiziereArgumente(0,_,_). unifiziereArgument(N,X,Y) :- arg(N,X,ArgumentX), arg(N,Y,ArgumentY), unifiziere(ArgumentX,ArgumentY). % 2. Quantorenlogische Regeln % sowie die Regeln zur Substitution von Variablen und Termen universell(alle(_,_)). universell(neg einige(_,_)). existentiell(einige(_,_)). existentiell(neg alle(_,_)). sub(Term, Variable, Formel, NeueFormel) :- subst(Term, Variable, Formel, NeueFormel), !. subst(Term,Variable,A,Term) :- Variable == A. subst(_,_,A,A) :- atomic(A). subst(_,_,A,A) :- var(A). subst(Term,Variable, neg X, neg Y) :- subst(Term,Variable,X,Y). subst(Term,Variable,Zweistellig1,Zweistellig2) :- zweistelligerJunktor(J), Zweistellig1 =.. [J,X,Y], Zweistellig2 =.. [J,U,V], subst(Term,Variable,X,U), subst(Term,Variable,Y,V). subst(_,Variable,alle(Variable,Y),alle(Variable,Y)). subst(Term,Variable,alle(X,Y),alle(X,Z)) :- subst(Term,Variable,Y,Z). subst(_,Variable,einige(Variable,Y),einige(Variable,Y)). subst(Term,Variable,einige(X,Y),einige(X,Z)) :- subst(Term,Variable,Y,Z). subst(Term,Variable,Funktor,NeuerFunktor) :- Funktor =.. [F|Argumente], subListe(Term,Variable,Argumente,ArgumenteNeu), NeuerFunktor =.. [F|ArgumenteNeu]. subListe(Term,Variable,[Kopf|Rest],[NeuerKopf|NeuerRest]):- subst(Term,Variable,Kopf,NeuerKopf), subListe(Term,Variable,Rest,NeuerRest). subListe(_,_,[],[]). instanz(alle(X,Y),Term,Z) :- sub(Term,X,Y,Z). instanz(neg einige(X,Y),Term,neg Z) :- sub(Term,X,Y,Z). instanz(einige(X,Y),Term,Z) :- sub(Term,X,Y,Z). instanz(neg alle(X,Y),Term,neg Z) :- sub(Term,X,Y,Z). /* da bei der existentiellen Spezialisierung auf einen neuen Term spezialisiert werden muss, werden solche Terme durch Skolem-Funktionen eingeführt; dafür muss auch mitgezählt werden, wieviele Skolem-Funktionen bisher eingeführt wurden. Die Skolem-Funktoren haben die Form: fun(4), fun(56) etc. */ funktionenzaehler(0). weitereSkolemFunktion(N) :- funktionenzaehler(N), retract(funktionenzaehler(N)), M is N + 1, assert(funktionenzaehler(M)). funktionenzaehlerZuruecksetzen :- retract(funktionenzaehler(_)), assert(funktionenzaehler(0)). skolem(VariablenListe, SkolemTerm) :- weitereSkolemFunktion(N), SkolemTerm =.. [fun|[N|VariablenListe]]. /* da in der existentiellen Spezialisierung auch die vorhandenen freien Variablen berücksichtigt werden müssen, werden in das Tableau nicht Formeln selbst eingetragen, sondern Formlen mit einer Liste ihrer freien Variablen (eine sogenannte "Notation"), in der Form: n([X,Z],gibt(X,buch,Z) imp einige(Y,buch(Y) und hat(Z,Y)) Die Hilfspädikate 'freieVariablen' und 'formel' greifen die beiden Teile dieser Notation heraus. */ freieVariablen(n(X,_),X). formel(n(_,X),X). % 3. Tableauregeln für den prädikaktenlogischen Fall /* da die Prädikatenlogik nicht entscheidbar ist, kann das Verfahren nur eine Antwort generieren, wenn man sich auf eine Obergrenze der vorzunehmenden universellen Instantiierungen festlegt; die gültigen Formeln sind bei einer bestimmten finiten Anzahl universeller Instantiierungen per geschlossener Tableaus (für deren Negationen) findbar, bezüglich der ungültigen Formeln wird man nie mehr sagen können, als dass sie für die getestete Anzahl von Instantiierungen nicht gültig sind; die Expansion des prädikatenlogischen Tableaus benutzt daher ein 'einSchritt'-Prädikat, das sich auf eine gewählte Obergrenze universeller Instantiierungen bezieht. */ einSchritt([AlterZweig|Rest],Grenze,[NeuerZweig|Rest],Grenze) :- member(Notation,AlterZweig), freieVariablen(Notation, Freie), formel(Notation,Formel), einstellig(Formel), komponenten(Formel,NeueFormel), freieVariablen(NeueNotation,Freie), formel(NeueNotation,NeueFormel), entferneVorkommnis(Notation,AlterZweig,Temp), NeuerZweig = [NeueNotation|Temp]. einSchritt([AlterZweig|Rest],Grenze,[NeuerZweig|Rest],Grenze) :- member(NotationKon,AlterZweig), freieVariablen(NotationKon,Freie), formel(NotationKon,Formel), konjunktiv(Formel), komponenten(Formel,Formel1,Formel2), freieVariablen(Notation1,Freie), formel(Notation1,Formel1), freieVariablen(Notation2,Freie), formel(Notation2,Formel2), entferneVorkommnis(NotationKon,AlterZweig,Temp), NeuerZweig = [Notation1,Notation2|Temp]. einSchritt([AlterZweig|Rest],Grenze,[NeuerZweig1,NeuerZweig2|Rest],Grenze) :- member(NotationDis,AlterZweig), freieVariablen(NotationDis,Freie), formel(NotationDis,Formel), disjunktiv(Formel), komponenten(Formel,Formel1,Formel2), freieVariablen(Notation1,Freie), formel(Notation1,Formel1), freieVariablen(Notation2,Freie), formel(Notation2,Formel2), entferneVorkommnis(NotationDis,AlterZweig,Temp), NeuerZweig1 = [Notation1|Temp], NeuerZweig2 = [Notation2|Temp]. einSchritt([AlterZweig|Rest],Grenze,[NeuerZweig|Rest],Grenze) :- member(NotationEx,AlterZweig), freieVariablen(NotationEx,Freie), formel(NotationEx,Formel), existentiell(Formel), skolem(Freie,Term), instanz(Formel,Term,Existenzinstanz), freieVariablen(NotationExistenzinstanz,Freie), formel(NotationExistenzinstanz,Existenzinstanz), entferneVorkommnis(NotationEx,AlterZweig,Temp), NeuerZweig = [NotationExistenzinstanz|Temp]. einSchritt([AlterZweig|Rest],Grenze,NeuerBaum,NeueGrenze) :- member(NotationUn,AlterZweig), freieVariablen(NotationUn,Freie), formel(NotationUn,FormelUn), universell(FormelUn), Grenze > 0, entferneVorkommnis(NotationUn,AlterZweig,Temp), NeueFreie = [V|Freie], instanz(FormelUn,V,FormelUnInstanz), freieVariablen(NotationUnInstanz,NeueFreie), formel(NotationUnInstanz,FormelUnInstanz), % die Allaussagen müssen für spätere Instantiierungen bewahrt werden append([NotationUnInstanz|Temp],[NotationUn],NeuerZweig), append(Rest,[NeuerZweig],NeuerBaum), NeueGrenze is Grenze - 1. einSchritt([Zweig|AlterRest],AlteGrenze,[Zweig|NeuerRest],NeueGrenze) :- einSchritt(AlterRest,AlteGrenze,NeuerRest,NeueGrenze). schrittfolge(Tableau,Grenze,NeuesTableau) :- einSchritt(Tableau,Grenze,Temp,TempGrenze), schrittfolge(Temp,TempGrenze,NeuesTableau). schrittfolge(Tableau,_,Tableau). geschlossen([Zweig|Rest]) :- member(Falsum,Zweig),formel(Falsum,false), geschlossen(Rest). geschlossen([Zweig|Rest]) :- member(Notation1,Zweig), formel(Notation1,Formel1), atomareFormel(Formel1), member(Notation2,Zweig), formel(Notation2, neg Formel2), unifiziere(Formel1,Formel2), geschlossen(Rest). geschlossen([]). entscheide(Formel,Grenze) :- funktionenzaehlerZuruecksetzen, freieVariablen(Notation,[]), formel(Notation,neg Formel), schrittfolge([[Notation]],Grenze,Tableau), geschlossen(Tableau) -> ja(Grenze); nein(Grenze). ja(Grenze) :- write('Ein prädikatenlogisches Theorem bei maximal '), write(Grenze), write(' universellen Instantiierungen.'), nl, write('Vorgenommene Existenzinstantiierungen: '), funktionenzaehler(N), writeln(N), !. nein(Grenze) :- write('Kein prädikatenlogisches Theorem bei maximal '), write(Grenze), write(' universellen Instantiierungen.'), nl, write('Vorgenommene Existenzinstantiierungen: '), funktionenzaehler(N), writeln(N), !. % test: entscheide(alle(X,praedikat(X)) imp einige(X,praedikat(X)),10). % test: entscheide(einige(X,praedikat(X))imp alle(X,praedikat(X)),10). % test: entscheide(alle(X,f(X) imp g(X)) imp (alle(X,f(X)) imp alle(X,g(X))),10). % test: entscheide(alle(X,f(X) imp g(X)) imp (alle(X,f(X)) imp alle(X,g(X))),1). % test: entscheide(alle(X,f(X)) imp f(a),29). % test: entscheide(einige(X,f(X)) imp f(a),29). % test: entscheide(einige(x,alle(y,relation(x,y))) imp alle(y,einige(x,relation(x,y))),10). % Problemfall: exponentielles Wachstum der Instantiierungen bei diesem Verfahren, z.B. % test: entscheide(alle(x,einige(y,relation(x,y))) imp einige(y,alle(x,relation(x,y))),3).