% Aufagbe (1)

knf(X,X) :- inknf(X,aussen).
knf(X,Y) :- trans(X,Z), knf(Z,Y).

% inknf soll testen, ob eine quantorfreie Formel in KNF vorliegt.


% trans soll einzelne Transformationsschritte (z.B.
% Regel von de Morgan, Distributivgesetze, ...), die
% die Formel weiter in Richtung KNF ueberfuehren.
% Die wiederholte Anwendung wird durch knf selber erledigt.



% Aufgabe (2)

% unsat soll testen, ob eine Klauselmenge unerfuellbar ist.


% Es folgen ein paar Praedikate, die bei der Implementierung
% von unsat hilfreich sein koennen.

% Sie koennen das Praedikat delete verwenden, um nicht-deterministisch
% Elemente aus einer Liste auszuwaehlen. 
delete(X, [X|YS], YS).
delete(X, [Y|YS], [Y|ZS]) :- delete(X, YS, ZS).

% Sie koennen das Praedikat append verwenden, um Listen
% aneinanderzuhaengen.
append([], YS, YS).
append([X|XS], YS, [X|ZS]) :- append(XS, YS, ZS).

% Sie koennen das Praedikat uniq verwenden, um doppelte Elemente
% aus Listen zu entfernen.
uniq(XS, YS) :- uniq(XS, [], YS).
uniq([], _, []).
uniq([X|XS], YS, ZS) :- member(X, YS), !, uniq(XS, YS, ZS).
uniq([X|XS], YS, [X|ZS]) :- uniq(XS, [X|YS], ZS).