% Manuel Mausz, 0728348
% unit tests befinden sich in gol.plt
 
% operator wertigkeit definieren
:- op(425, fy,  -).
:- op(450, yfx, &).
:- op(500, yfx, v).
 
% --------------------------------------------------------------------------
 
% wenn A atom ist, retourniere A
nnf(A, A) :-
	atomic(A).
 
% wenn A negiert ist und A atom ist, reourniere A negiert
nnf(-A, -A) :-
	atomic(A).
 
% wenn A doppelt negiert ist, entferne die doppelte negation
nnf(-(-A), X) :-
	nnf(A, X).
 
% de morgansche gesetze
nnf(-(A & B), X) :-
	nnf(-A v -B, X).
nnf(-(A v B), X) :-
	nnf(-A & -B, X).
 
% akzeptiere kon-/disjunktionen, wenn die subterme in NNF sind
nnf(A & B, X & Y) :-
	nnf(A, X), nnf(B, Y).
nnf(A v B, X v Y) :-
	nnf(A, X), nnf(B, Y).
 
% --------------------------------------------------------------------------
 
% literal check
literalp(A) :-
	atomic(A).
literalp(-A) :-
	atomic(A).
 
% --------------------------------------------------------------------------
 
% anzahl der "oder" (v) zaehlen
no_or(A, X) :-
	literalp(A), X is 0.
no_or(A v B, X) :-
	no_or(A, Y1), no_or(B, Y2), X is Y1 + Y2 + 1.
no_or(A & B, X) :-
	no_or(A, Y1), no_or(B, Y2), X is Y1 + Y2.
 
% --------------------------------------------------------------------------
 
% prove2/3 wrapper fuer prove3/4
prove2(F1, F2, NOW) :-
	prove2(F1, F2, NOW, _DATA).
 
% axioms
prove2(A, -A, _NOW, axiom([A, -A])).
prove2(-A, A, _NOW, axiom([A, -A])).
 
% (&, literal)
prove2((F1 & F2), A, NOW, undRegel([F1 & F2, A], [Praem1, Praem2])) :-
	literalp(A), prove2(F1, A, NOW, Praem1), prove2(F2, A, NOW, Praem2).
 
% (literal, &)
prove2(A, (F1 & F2), NOW, undRegel([A, F1 & F2], [Praem1, Praem2])) :-
	literalp(A), prove2(A, F1, NOW, Praem1), prove2(A, F2, NOW, Praem2).
 
% (v, literal)
prove2((F1 v F2), A, NOW, oderRegel([F1 v F2, A], Praem)) :-
	literalp(A), prove2(F1, A, NOW, Praem).
prove2((F1 v F2), A, NOW, oderRegel([F1 v F2, A], Praem)) :-
	literalp(A), prove2(F2, A, NOW, Praem).
 
% (literal, v)
prove2(A, (F1 v F2), NOW, oderRegel([A, F1 v F2], Praem)) :-
	literalp(A), prove2(A, F1, NOW, Praem).
prove2(A, (F1 v F2), NOW, oderRegel([A, F1 v F2], Praem)) :-
	literalp(A), prove2(A, F2, NOW, Praem).
 
% (&, &)
prove2((F1 & F2), (F3 & F4), NOW, undRegel([F1 & F2, F3 & F4], [Praem1, Praem2])) :-
	prove2(F1, (F3 & F4), NOW, Praem1), prove2(F2, (F3 & F4), NOW, Praem2).
prove2((F1 & F2), (F3 & F4), NOW, undRegel([F1 & F2, F3 & F4], [Praem1, Praem2])) :-
	prove2((F1 & F2), F3, NOW, Praem1), prove2((F1 & F2), F4, NOW, Praem2).
 
% (&, v)
prove2((F1 & F2), (F3 v F4), NOW, undRegel([F1 & F2, F3 v F4], [Praem1, Praem2])) :-
	prove2(F1, (F3 v F4), NOW, Praem1), prove2(F2, (F3 v F4), NOW, Praem2).
prove2((F1 & F2), (F3 v F4), NOW, oderRegel([F1 & F2, F3 v F4], Praem)) :-
	prove2((F1 & F2), F3, NOW, Praem).
prove2((F1 & F2), (F3 v F4), NOW, oderRegel([F1 & F2, F3 v F4], Praem)) :-
	prove2((F1 & F2), F4, NOW, Praem).
 
% (v, &)
prove2((F1 v F2), (F3 & F4), NOW, oderRegel([F1 v F2, F3 & F4], Praem)) :-
	prove2(F1, (F3 & F4), NOW, Praem).
prove2((F1 v F2), (F3 & F4), NOW, oderRegel([F1 v F2, F3 & F4], Praem)) :-
	prove2(F2, (F3 & F4), NOW, Praem).
prove2((F1 v F2), (F3 & F4), NOW, undRegel([F1 & F2, F3 v F4], [Praem1, Praem2])) :-
	prove2((F1 v F2), F3, NOW, Praem1), prove2((F1 v F2), F4, NOW, Praem2).
 
% (v, W)
prove2((F1 v F2), Z, NOW, weakening([F1 v F2, Z], Praem)) :-
	NOW > 0, Z \== (F1 v F2), Z \== (F2 v F1),
	prove2((F1 v F2), (F1 v F2), NOW - 1, Praem).
 
% (W, v)
prove2(Z, (F1 v F2), NOW, weakening([Z, F1 v F2], Praem)) :-
	NOW > 0, Z \== (F1 v F2), Z \== (F2 v F1),
	prove2((F1 v F2), (F1 v F2), NOW - 1, Praem).
 
% (v, v)
prove2((F1 v F2), (F3 v F4), NOW, oderRegel([F1 v F2, F3 v F4], Praem)) :-
	prove2(F1, (F3 v F4), NOW, Praem).
prove2((F1 v F2), (F3 v F4), NOW, oderRegel([F1 v F2, F3 v F4], Praem)) :-
	prove2(F2, (F3 v F4), NOW, Praem).
prove2((F1 v F2), (F3 v F4), NOW, oderRegel([F1 v F2, F3 v F4], Praem)) :-
	prove2((F1 v F2), F3, NOW, Praem).
prove2((F1 v F2), (F3 v F4), NOW, oderRegel([F1 v F2, F3 v F4], Praem)) :-
	prove2((F1 v F2), F4, NOW, Praem).
 
% --------------------------------------------------------------------------
 
% zusatzaufgabe 1
writelist([]) :- !.
writelist([X]) :- write(X), !.
writelist([H | T] ) :- write(H), write(', '), writelist(T).
 
writeKonk(Konk) :-
	write('|- '), writelist(Konk), nl.
writeRegel(Str, Konk, Praem) :-
	call(Praem),
	write('-------------------------------------------------- '), write(Str), nl,
	writeKonk(Konk).
oderRegel(Konk, Praem) :-
	writeRegel('or', Konk, Praem).
undRegel(Konk, [P1, P2]) :-
	writeRegel('and', Konk, P1),
	write('================================================== '), nl,
	writeRegel('and', Konk, P2).
weakening(Konk, Praem) :-
	writeRegel('W', Konk, Praem).
axiom(Konk) :-
	writeKonk(Konk).
 
% --------------------------------------------------------------------------
 
% prover
:- dynamic(prove_print/0).
prove(IN) :-
	nnf(IN, NNF), no_or(NNF, NOR), prove2(NNF, NNF, NOR, DATA), (prove_print, call(DATA); true).
 
% vim: set noet sw=4 ts=4: