%% Copyright (C) 2001 towr

:-set_prolog_flag(unknown,fail).  


s5(P):-atom(P).

s5(not(P)):- \+var(P),s5(P).

s5(or(P,Q)):- \+var(P),s5(P), \+var(Q), s5(Q).
s5(and(P,Q)):- \+var(P),s5(P),\+var(Q), s5(Q).

s5('K'(P)):- \+var(P), s5(P).
s5('M'(P)):- \+var(P), s5(P).


:- include('tree.pl'). %% printing as tree + marking
:- include('prop.pl'). %% proposition logic


inv('K'(P), 'M'(P2)):-inv(P,P2).
inv('M'(P), 'K'(P2)):-inv(P,P2).

remand(and(P,Q),P,mark(Q, orange)).
remand(and(P,Q),Q,mark(P, orange)).
remand(and(P,Q),R,and(P2,Q)):-remand(P,R,P2).
remand(and(P,Q),R,and(P,Q2)):-remand(Q,R,Q2).

remand(or(P,Q),P,mark(Q, orange)).
remand(or(P,Q),Q,mark(P, orange)).
remor(or(P,Q),R,or(P2,Q)):-remor(P,R,P2).
remor(or(P,Q),R,or(P,Q2)):-remor(Q,R,Q2).

%%%%%%%%%%%% modal-logic  %%%%%%%%%%%%

%%%%%%%%%%%% and  %%%%%%%%%%%%

simplify(and('K'(P),'M'(P)), mark('K'(P), red), '<=> { K(p) & M(p) == K(p) }\n').
simplify(and('M'(P),'K'(P)), mark('K'(P), red), '<=> { M(p) & K(p) == K(p) }\n').

simplify(and(P,'M'(Q)), mark(P,red), '<=> { K(p) & M(p) == K(p) }\n'):- inand(P,'K'(Q)).
simplify(and(P, Q), mark(P,red), '<=> { K(p) & p == K(p) }\n'):- inand(P,'K'(Q)).

simplify(and(P, 'K'(Q)), mark(and(P2,'K'(Q)),red), '<=> { p & K(p) == K(p) }\n'):- remand(P,Q,P2).
simplify(and(P, 'K'(Q)), mark(and(P2,'K'(Q)),red), '<=> { M(p) & K(p) == K(p) }\n'):- remand(P,'M'(Q),P2).

simplify(and(P,'M'(Q)), mark(false,red), '<=> { K(~p) & M(p) == F }\n'):-inv(Q,Q2),inand(P,'K'(Q2)).
simplify(and(P,'K'(Q)), mark(false,red), '<=> { M(~p) & K(p) == F }\n'):-inv(Q,Q2),inand(P,'M'(Q2)).
simplify(and(P,'K'(Q)), mark(false,red), '<=> { K(~p) & K(p) == F }\n'):-inv(Q,Q2),inand(P,'K'(Q2)). % should be redundant %


simplify(and('K'(P),P),mark('K'(P),red), '<=> { K(p) & p == K(p) }\n').  %% Kp -> p         % redundant %
                                                                         %% Kp -> Kp 
simplify(and(P,'K'(P)),mark('K'(P),red), '<=> { p & K(p) == K(p) }\n').  %% p & Kp -> Kp    % redundant %
                                                                         %% Kp == p & Kp

simplify(and('K'(P),Q), mark(and(Q,'K'(P)),green), '<=> {  }\n'):-Q\='K'(_).
simplify(and(and(P,'K'(Q)),R), mark(and(and(P,R),'K'(Q)),green), '<=> {  }\n'):-R\='K'(_).
simplify(and('M'(P),Q), mark(and(Q,'M'(P)),green), '<=> {  }\n'):-Q\='K'(_),Q\='M'(_).
simplify(and(and(P,'M'(Q)),R), mark(and(and(P,R),'M'(Q)),green), '<=> {  }\n'):-R\='K'(_),R\='M'(_).

%%%%%%%%%%%% or  %%%%%%%%%%%%
% not(K(p)) == not(and(p,K(p)))
% M(p) == or(p, M(p))

simplify(or(P,'K'(Q)), mark(P,red), '<=> { M(p) | K(p) == M(p) }\n'):- inor(P,'M'(Q)).
simplify(or(P, Q), mark(P,red), '<=> { M(p) | p == M(p) }\n'):- inor(P,'M'(Q)).

simplify(or(P, 'M'(Q)), mark(or(P2,'K'(Q)),red), '<=> { p | M(p) == M(p) }\n'):- remand(P,Q,P2).
simplify(or(P, 'M'(Q)), mark(or(P2,'K'(Q)),red), '<=> { K(p) | M(p) == M(p) }\n'):- remand(P,'K'(Q),P2).



simplify(or('K'(P),'M'(Q)), mark(true,red), '<=> {  K(~p) | M(p) == T }\n'):-inv(P,Q).
simplify(or('M'(P),'K'(Q)), mark(true,red), '<=> {  M(~p) | K(p) == T }\n'):-inv(P,Q).

simplify(or(and(P, 'K'(Q)),R), mark(or(R,and(P,'K'(Q))),green), '<=> {  }\n'):-R\=and(_,'K'(_)).
simplify(or(or(P,and(Q,'K'(R))),S), mark(or(or(P,S),and(Q,'K'(R))),green), '<=> {  }\n'):-S\=and(_,'K'(_)).
simplify(or(and(P, 'M'(Q)),R), mark(or(R,and(P,'M'(Q))),green), '<=> {  }\n'):-R\=and(_,'K'(_)),R\=and(_,'M'(_)).
simplify(or(or(P,and(Q,'M'(R))),S), mark(or(or(P,S),and(Q,'M'(R))),green), '<=> {  }\n'):-S\=and(_,'K'(_)),S\=and(_,'M'(_)).

simplify(or('K'(P),Q), mark(or(Q,'K'(P)),green), '<=> {  }\n'):-Q\='K'(_),Q\=and(_,'K'(_)),Q\=and(_,'M'(_)).
simplify(or(or(P,'K'(Q)),R), mark(or(or(P,R),'K'(Q)),green), '<=> {  }\n'):-R\='K'(_),R\=and(_,'K'(_)),R\=and(_,'M'(_)).
simplify(or('M'(P),Q), mark(or(Q,'M'(P)),green), '<=> {  }\n'):-Q\='K'(_),Q\='M'(_),Q\=and(_,'K'(_)),Q\=and(_,'M'(_)).
simplify(or(or(P,'M'(Q)),R), mark(or(or(P,R),'M'(Q)),green), '<=> {  }\n'):-R\='K'(_),R\='M'(_),R\=and(_,'K'(_)),R\=and(_,'M'(_)).

simplify(or(and(P,P2),Q), mark(or(Q,and(P,P2)),green), '<=> {  }\n'):-Q\='K'(_),Q\='M'(_),Q\=and(_,_).
simplify(or(or(P,and(Q,Q2)),R), mark(or(or(P,R),and(Q,Q2)),green), '<=> {  }\n'):-R\='K'(_),R\='M'(_),R\=and(_,_).


%%%%%%%%%%%% not  %%%%%%%%%%%%

simplify(not('K'(P)), mark('M'(not(P)),green), '<=> { not(K(p)) == M(not(p)) }\n').
simplify(not('M'(P)), mark('K'(not(P)),green), '<=> { not(M(p)) == K(not(p)) }\n').

%%%%%%%%%%%% K/M  %%%%%%%%%%%%

simplify('K'(true),mark(true,red), '<=> { K(T) == T }\n').     %%%%%
simplify('K'(false),mark(false,red), '<=> { K(F) == F }\n').   %%%%%
simplify('K'(P),'K'(Q), MSG):-simplify(P,Q, MSG).
simplify('M'(true),mark(true,red), '<=> { M(T) == T }\n').     %%%%%
simplify('M'(false),mark(false,red), '<=> { M(F) == F }\n').   %%%%%
simplify('M'(P),'M'(Q), MSG):-simplify(P,Q, MSG).


simplify('K'(or(Pi,and(Lambda,'K'(Beta)))),
         mark(or(and('K'(or(mark(Pi,yellow),mark(Lambda, purple))),mark('K'(Beta),blue)),and('K'(mark(Pi,yellow)), not(mark('K'(Beta),blue)))),green), '<=> {  }\n').
simplify('K'(or(Pi,and(Lambda,'M'(Beta)))), 
         mark(or(and('K'(or(mark(Pi,yellow),mark(Lambda, purple))),mark('M'(Beta),blue)),and('K'(mark(Pi,yellow)), not(mark('M'(Beta),blue)))),green), '<=> {  }\n').

simplify('M'(or(Pi,and(Lambda,'K'(Beta)))),mark(not(T),green), MSG):-simplify('K'(or(and(not(Pi),not(Lambda)),and(not(Pi),not('K'(Beta))))),T, MSG).
simplify('M'(or(Pi,and(Lambda,'M'(Beta)))),mark(not(T),green), MSG):-simplify('K'(or(and(not(Pi),not(Lambda)),and(not(Pi),not('M'(Beta))))),T, MSG).

simplify('K'(or(Pi,'K'(Beta))), or('K'(mark(Pi,yellow)), mark('K'(Beta),blue)), '<=> { K(p | K(q)) == K(p) | K(q) }\n'). %%% lambda = T
simplify('K'(or(Pi,'M'(Beta))), or('K'(mark(Pi,yellow)), mark('M'(Beta),blue)), '<=> { K(p | M(q)) == K(p) | M(q) }\n'). %%% lambda = T

simplify('M'(and(Lambda,'K'(Beta))),mark(and('M'(mark(Lambda,purple)),mark('K'(Beta),blue)),green), '<=> { M(p & K(q)) == K(q) & (M(p) | ~K(q)) }\n').        %%% pi =F
simplify('M'(and(Lambda,'M'(Beta))),mark(and('M'(mark(Lambda,purple)),mark('M'(Beta),blue)),green), '<=> { M(p & M(q)) == M(q) & (M(p) | ~M(q)) }\n').        %%% pi =F

simplify('K'(and(P,'K'(Q))),mark('K'(and(P,Q)),green), '<=> { K(p & K(q)) == K(p & q) }\n').      %%% pi =F
simplify('K'(and(P,'M'(Q))),mark(and('K'(P),'M'(Q)),green), '<=> { K(p & M(q)) == K(p) & M(q) }\n'). %%% pi =F

simplify('M'(or(P,'M'(Q))),mark(or('M'(P),'M'(Q)),green), '<=> { M(p | M(q)) == M(p) | K(q) }\n').   %%% lambda = T
simplify('M'(or(P,'K'(Q))),mark('K'(or(P,Q)),green), '<=> { M(p | K(q)) == M(p | q) }\n').        %%% lambda = T

simplify(and('K'(P),'K'(Q)),mark('K'(and(P,Q)),green), '<=> { K(p) & K(q) == K(p & q) }\n').
simplify(or('M'(P),'M'(Q)),mark('M'(or(P,Q)),green), '<=> { M(p) | M(q) == M(p | q) }\n').


simplify('K'('K'(P)),mark('K'(P),red), '<=> { K(K(p)) == K(p) }\n').        %%% A3,A4
simplify('K'('M'(P)),mark('M'(P),red), '<=> { K(M(p)) == M(p) }\n').        %%% A3,A5 

simplify('M'('K'(P)),mark('K'(P),red), '<=> { M(K(p)) == K(p) }\n').      
simplify('M'('M'(P)),mark('M'(P),red), '<=> { M(M(p)) == M(p) }\n').      


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


simplify(Q):-printexp(Q), write('\n'), write('\n'), clean(Q,Q2),
             (simplify(Q2,R, MSG)
            -> write(MSG), write('\n'), simplify(R)
	     ; write('\n done \n')
	     ).

start(Q):- s5(Q), simplify(Q).
start(_):- write('I\'m sorry to inform you that your expression could not be parsed due to syntax errors therein.
The syntax rules are provided above.
Please try again with a different expression').


simplify2(Q):-buildtree(Q), write('\n'), clean(Q,Q2),
             (simplify(Q2,R, MSG)
            -> write(MSG), write('\n'), simplify2(R)
	     ; write('\n done \n')
	     ).

start2(Q):- s5(Q), simplify2(Q).
start2(_):- start(0).


%% simplify('K'(or(false, and(true, 'K'(beta))))).
%% simplify(or(and('K'(or(false,true)), 'K'(beta)), and('K'(false), not('K'(beta))))).





%%%%%%%%%%%%%
simplify(P, mark(or(U,Q),red), '<=> { p | (~p & q) == p | q }'):-inor(P,U),inor(P,V),inv(U,W),remand(V,W,Q). %%(10-9-01)




