%% Copyright (C) 2005 Igor Stéphan
%% 
%% This program is free software; you can redistribute it and/or
%% modify it under the terms of the GNU General Public License
%% as published by the Free Software Foundation; either version 2
%% of the License, or (at your option) any later version.
%% 
%% This program is distributed in the hope that it will be useful,
%% but WITHOUT ANY WARRANTY; without even the implied warranty of
%% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
%% GNU General Public License for more details.
%% 
%% You should have received a copy of the GNU General Public License
%% along with this program; if not, write to the Free Software
%% Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA  02110-1301, USA.
%% http:%%www.gnu.org/copyleft/gpl.html
%%
%% igor.stephan@univ-angers.fr
%% 
:- use_module(library(clpb),[sat/1,taut/2,'*'/2,'+'/2,'>'/2,'<'/2,'~'/1]).

'|='(M,F) :-
	\+(\+((sat(M),taut(F,1)))).

'|='(F) :-
	\+(\+(taut(F,1))).

contingent(F) :-
	\+(taut(F,1)),
	\+(taut(~F,1)).
contingent(M,F) :-
	\+((sat(M),taut(F,1))),
	\+((sat(M),taut(~F,1))).

'==='(M,X,Y) :-
	\+(\+((sat(M),taut((X >= Y) * (X =< Y),1)))).
'==='(X,Y) :-
	\+(\+(taut((X >= Y) * (X =< Y),1))).

simplification(X,X) :-
	(var(X);atomic(X)),
	!.

simplification(~X,Z) :-
	simplification(X,X_),
	((compound(X_), X_ = ~Z) ->
	    true; Z = ~X_).
simplification(X*Y,Z) :-
	simplification(X,X_),
	simplification(Y,Y_),
	(
	    atomic(X_),
	    X_ = 0,
	    !,
	    Z = 0;

	    atomic(Y_),
	    Y_ = 0,
	    !,
	    Z = 0;

	    atomic(X_),
	    X_ = 1,
	    !,
	    Z = Y_;
	    
	    atomic(Y_),
	    Y_ = 1,
	    !,
	    Z = X_;

	    compound(X_),
	    X_ = ~U,
	    U == Y_,
	    !,
	    Z = 0;

	    compound(Y_),
	    Y_ = ~U,
	    U == X_,
	    !,
	    Z = 0;

	    X_ == Y_,
	    !,
	    Z = X_;

	    Z = X_ * Y_
	).
simplification(X+Y,Z) :-
	simplification(X,X_),
	simplification(Y,Y_),
	(
	    atomic(X_),
	    X_ = 1,
	    !,
	    Z = 1,

	    atomic(Y_),
	    Y_ = 1,
	    !,
	    Z = 1;

	    atomic(X_),
	    X_ = 0,
	    !,
	    Z = Y_;
	    
	    atomic(Y_),
	    Y_ = 0,
	    !,
	    Z = X_;

	    compound(X_),
	    X_ = ~U,
	    U == Y_,
	    !,
	    Z = 1;

	    compound(Y_),
	    Y_ = ~U,
	    U == X_,
	    !,
	    Z = 1;

	    X_ == Y_,
	    !,
	    Z = X_;

	    Z = X_ + Y_
	).