
% Näide: tõestada valem: c/\(a\/b) -> (~a)/\a.
% Päring Prologis: [u(a)/\(a\/b)]?c/\a.

% operaator: prioriteet (1, ..., 1500) – väiksem number annab kõrgema prioriteedi.
%
:- op(510, fx, [~]).		
:- op(520, xfy, [/\]).		
:- op(530, xfy, [\/]).		
:- op(540, xfx, [->]).					
:- op(550, xfx, [?]).

% [eelduste hulk]?(tõestatav valem)
Assumptions?Goal:- 								% Näide: [~(~a)]?a
	transform(Assumptions, Goal, Formula),      % Assumptions: [~(~a)] , Goal: a , Formula: ~(~a)/\ ~a
	setup(Formula, Valuation),
	(generate(Valuation),
	value(Formula,t,Valuation),					% kui tagastatav väärtus unifitseerub 't',siis kuulutatakse valem vääraks, kuna tegemist on vastuväitelise tõestusega
	write('not valid'));
	write('valid').

% valemite listi teisendamine KNK-le
transform([],G,~G).                    % Lisatakse eitusega tõestatav valem (vastuväiteline tõestus)
transform([H|T],G,H/\X):- transform(T,G,X).

% eraldab välja lausemuutujad, tekib list [[a, _], [b, _], ...], hiljem _ asendatakse T või V -ga
setup(A,[[A|_]]):- atomic(A).
setup(~F,V):-  setup(F,V).
setup(F,V):- 
	F=..[_,A,B], 
	setup(A,X), 	
	setup(B,Y),
	union(X,Y,V).

% ======= Lausemuutujate tõeväärtuste generereerimine ========
% esimesel läbimisel t, backtrack asendab f-ga
generate([]).				% sabarekursioon
generate([[A,V]|T]):-		% A – lausemuutuja, V – tema tõeväärtus
	(V=t; V=f),				% lausemuutujate väärtustamine algselt “true”-ga
	generate(T).			% tagasivõtu korral väärtustamine “false”-ga

% arvutab kogu valemile tõeväärtuse
value(A,Z,V):- atomic(A),!,member([A,Z],V).   			% kui tegemist automaarse valemiga - leia väärtus
value(~A,Z,V):- value(A,X,V), truth_table(~X,Z).        % kui tegemist eitusega - eituse all oleva valemi interpreteerimine
value(A/\B,Z,V):- value(A,X,V), value(B,Y,V), 	truth_table(X/\Y,Z).  % kui osavalem - pöördu tõeväärtustabeli poole
value(A\/B,Z,V):- value(A,X,V), value(B,Y,V), 	truth_table(X\/Y,Z).
value(A->B,Z,V):- value(A,X,V), value(B,Y,V), 	truth_table(X->Y,Z).

truth_table(t/\t,t):- !.
truth_table(_/\_,f).
truth_table(f\/f,f):- !.
truth_table(_\/_,t).
truth_table(t->f,f):- !.
truth_table(_->_,t).
truth_table(~t,f).
truth_table(~f,t).

union([],Y,Y).
union([[A,_]|T],Y,Z):- member([A,_],Y),!, union(T,Y,Z).
union([[A,V]|T],Y,[[A,V]|Z]):- union(T,Y,Z).
member(X,[H|T]):- X=H;member(X,T).

subterm(T,T).
subterm(S,T):- T =..[_|Args], sub(S, Args).
sub(S, [First|Rest]):- subterm(S, First); sub(S,Rest).

% predikaatloogika
%
% p(a)
% p(b)
% a(1)
% a(2)

% clause/2, term_to_atom/2,atomic/1


