% Autor: MB % Version JUL 2016 % Aussagenlogische Formeln werden dargestellt wie: neg(a oder (b und c)) imp d % benötigt die PROLOG-Prädikate: member/2, true/0, false/0 % sowie entferne(_,[],[]). entferne(X,[X|Rest], Neu) :- entferne(X,Rest,Neu). entferne(X, [Kopf|Rest], [Kopf|Neu]) :- entferne(X,Rest,Neu). % 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 % Konkunktive Formeln - zur Generierung der Disjunktiven Normalform konjunktiv( _ und _ ). konjunktiv(neg(_ oder _)). konjunktiv(neg(_ imp _)). konjunktiv(neg(_ nand _)). % 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 in einer Zerlegung zur Disjunktiven Normalform 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(neg neg X, X). komponenten(neg true, false). komponenten(neg false, true). % Aufbau der disjunktiven Normalform je nachdem ob die Formel einstellig % disjunktiv oder konjunktiv ist einSchritt([Konjunktion|Rest], Neu) :- member(Formel, Konjunktion), einstellig(Formel), komponenten(Formel, NeueFormel), entferne(Formel, Konjunktion, Zwischen), NeueKonjunktion = [NeueFormel|Zwischen], Neu = [NeueKonjunktion|Rest]. einSchritt([Konjunktion|Rest], Neu) :- member(Formel, Konjunktion), konjunktiv(Formel), komponenten(Formel, FormelLinks, FormelRechts), entferne(Formel, Konjunktion, Zwischen), NeueKonjunktion = [FormelLinks, FormelRechts | Zwischen], Neu = [NeueKonjunktion|Rest]. einSchritt([Konjunktion|Rest],Neu) :- member(Formel, Konjunktion), disjunktiv(Formel), komponenten(Formel, FormelLinks, FormelRechts), entferne(Formel, Konjunktion, Zwischen), NeueKonjunktionLinks = [FormelLinks | Zwischen], NeueKonjunktionRechts = [FormelRechts | Zwischen], Neu = [NeueKonjunktionLinks, NeueKonjunktionRechts | Rest]. einSchritt([Konjunktion|Rest],[Konjunktion|NeuerRest]):- einSchritt(Rest, NeuerRest). schrittfolge(Disjunktion, NeueDisjunktion) :- einSchritt(Disjunktion, Zwischen), schrittfolge(Zwischen, NeueDisjunktion). schrittfolge(Disjunktion, Disjunktion). disjunktiveNormalform(Formel, DNF) :- schrittfolge([[Formel]], DNF), !. % test: disjunktiveNormalform(neg(a oder (b und c)) imp d,DNF).