% Autors: Guntis Barzdins, Oktobris 2006
% Propositional calculus satisfyability solver (tableau algorithm)
% Tested on SWI-Prolog (http://www.swi-prolog.org/)

:- op(1130, xfy, <=>). % equivalence
:- op(1110, xfy, =>).  % implication
:- op(1100, xfy, v).   % disjunction
:- op(1100, xfy, &).   % conjunction
:- op( 500, fy, ~).    % negation

% -----------------------------------------------------------------
%  prove(+Fml)
%
% Fml is a Propositional calculus formula with free variables.
% p(+Fml) succeeds, if the free variables in Fml can be bound 
% to true/false values resulting in the Fml itself becoming true
% 
% Example:  prove((A => ~ B) & B).
%           A = false
%           B = true ;

prove(Fml) :- nnf(Fml,NNF), p(NNF).

p(true) :- !.
p((~ false)) :- !.
p((A & B)) :- !, p(A), p(B).
p((A v B)) :- p(A); p(B).


% -----------------------------------------------------------------
%  nnf(+Fml,?NNF)
%
% Fml is a Propositional calculus formula and NNF its negation normal form 
% 
% Example:  nnf((Y => X),NNF).
%           NNF = (~(Y) v X)

nnf(Lit,Lit) :- not(not(Lit=anything)), !.
nnf(~ Lit, ~ Lit) :- not(not(Lit=anything)), !.
nnf(Fml,NNF) :- 
	(Fml = ~(~ A)     -> Fml1 = A;
	 Fml = ~((A v B)) -> Fml1 = ((~ A & ~ B));
	 Fml = ~((A & B)) -> Fml1 = (~ A v ~B);
	 Fml = (A => B)   -> Fml1 = (~ A v B);
	 Fml = ~((A => B))-> Fml1 = ((A & ~ B));
	 Fml = (A <=> B)  -> Fml1 = ((A & B) v (~ A & ~ B));
	 Fml = ~((A<=>B)) -> Fml1 = ((A & ~ B) v (~ A & B))),!,
	nnf(Fml1,NNF).
nnf((A v B),(NNF1 v NNF2)) :- !, nnf(A,NNF1), nnf(B,NNF2).
nnf((A & B),(NNF1 & NNF2)) :- !, nnf(A,NNF1), nnf(B,NNF2).