% Autor: MB % Version JUL 2016 :- consult('DisjunktiveNormalform.pl'). % Aussagenlogische Formeln werden dargestellt wie: neg(a oder (b und c)) imp d % die Umformung in Disjunktive Normalform dient hier auch als Basis für ein % Tableau-Entscheidungsverfahren: zuerst wird die Disjunktive Normalform gebildet % und dann, ausgehend von der Negation der auf Gültigkeit zu prüfenden Formel, % überprüft, ob alle Disjunkte, die Untertableaus entsprechen, inkonsistent sind geschlossen([Teiltableau|Rest]) :- member(false,Teiltableau), geschlossen(Rest). geschlossen([Teiltableau|Rest]) :- member(X, Teiltableau), member(neg X, Teiltableau), geschlossen(Rest). geschlossen([]). % Umgang mit der leeren Liste als Rest % vor jedem weiteren Schritt der Tableau-Entwicklung wird überprüft, ob das % Tableau nicht schon geschlossen ist entwickleUndPruefe(Tableau) :- geschlossen(Tableau). % da Tableaus nichtdeterministisch sind, empfiehlt sich zur Effizienssteigerung % der Einsatz des Cut entwickleUndPruefe(Tableau) :- einSchritt(Tableau, NeuesTableau), !, entwickleUndPruefe(NeuesTableau). % damit Variante 1 läuft, muss Variante 2 auskommentiert werden % Variante 1 läuft ausdrücklich über die Disjunktive Normalform % entscheide(X) :- disjunktiveNormalform(neg X,DNF),!, geschlossen(DNF) -> ja; nein. % Variante 2 enthält die oben beschriebene Beschleunigung entscheide(X) :- entwickleUndPruefe([[neg X]]) -> ja; nein. ja :- write('Eine aussagenlogische Tautologie!'),nl. nein :- write('Keine aussagenlogische Tautologie!'), nl.