title([
'%-----------------------------------------------------------',
'% simulating propositional logic in Prolog (logic01.pl)',
'% author: Kenryo Indo (Kanto Gakuen University)',
'%-----------------------------------------------------------'
]).
data([
'% logic01.pl',
'% created: 1 Jun 2003.(logic0.pl)',
'% modified: 5 Jun 2003.',
'% modified: 12-13 July 2003.'
]).

main_predicates([
%  formula0/3,
  formula1/3,
%  truth_value0/2,
%  truth_value1/2,
%  well_defined_formula/3,
%  well_defined_formula1/3,
%  interpretation0/3,
  interpretation1/3,
  'truth_table(A,B,TT,[OPT]):OPT=p/w/t/h/l',
  'reduced_normal_form(disjunctive,A,B,D,O):O=[w]/[]',
  'minimal_reduced_normal_form(disjunctive,A,B,D,O):O=[w]/[]',
  'all_minimal_reduced_normal_forms(disjunctive,A,B,S)',
  'minimal_reduced_MLD_normal_form(disjunctive,A,B,D,O):O=[w]/[]'
]). 

:- nl,title(H),main_predicates(P),
   forall((member(X,H)),(nl,write(X))),
   nl,write('%main predicates:'),
   forall((member(X,P)),(nl,write(X))).

proposition(p).
proposition(q).
proposition(r).
proposition(s).
proposition(t).


%---------- model 0 -----------------

/*
formula0(1,'�i�`‚o�È‚p�j�¨‚q',and(not(p),q)->r).
formula0(2,'‚o�¨�i�i‚p�È‚q�j�¨‚r�j', p->(and(q,r)->s)).
formula0(3,'�`�i‚o�É�`‚p�j�È�i‚r�¨‚s�j', and(not(or(p,not(q))),s->t)).
formula0(4,'�i‚o�¨‚p�j�¨‚q',((p->q)->r)).
formula0(5,'�`�i‚o�È‚p�j�È�i‚o�É‚p�j',and(not(and(p,q)),and(p,q))).
*/

formula0(1, (\+ p,q)->r, and(not(p),q)->r).
formula0(2, p->((q,r)->s), p->(and(q,r)->s)).
formula0(3, (\+ (p; \+ q),(s->t)), and(not(or(p,not(q))),s->t)).
formula0(4, (p->q)->r, ((p->q)->r)).
formula0(5, (\+ (p,q),(p;q)), and(not(and(p,q)),and(p,q))).
formula0(6, (\+ (p->((q,r)->s))), not(p->(and(q,r)->s))).  % negation of 2


truth_value0(P,true):-proposition(P).
truth_value0(P,false):-proposition(P).
truth_value0(not(true),false).
truth_value0(not(false),true).
truth_value0(and(true,true),true).
truth_value0(and(true,false),false).
truth_value0(and(false,true),false).
truth_value0(and(false,false),false).
truth_value0(or(true,true),true).
truth_value0(or(true,false),true).
truth_value0(or(false,true),true).
truth_value0(or(false,false),false).
truth_value0(true->true,true).
truth_value0(true->false,false).
truth_value0(false->true,true).
truth_value0(false->false,true).

well_defined_formula0(P,T,[P=T]):-
   proposition(P),
   truth_value0(P,T).
well_defined_formula0(Q,T,M):-
   Q = not(P),
   well_defined_formula0(P,T1,M),
   truth_value0(not(T1),T).
well_defined_formula0(Q,T,M):-
   Q = and(P1,P2),
   well_defined_formula0(P1,T1,M1),
   well_defined_formula0(P2,T2,M2),
   truth_value0(and(T1,T2),T),
   union(M1,M2,M12),
   sort(M12,M).
well_defined_formula0(Q,T,M):-
   Q = or(P1,P2),
   well_defined_formula0(P1,T1,M1),
   well_defined_formula0(P2,T2,M2),
   truth_value0(or(T1,T2),T),
   union(M1,M2,M12),
   sort(M12,M).
well_defined_formula0(Q,T,M):-
   Q = (P1->P2),
   well_defined_formula0(P1,T1,M1),
   well_defined_formula0(P2,T2,M2),
   truth_value0((T1->T2),T),
   union(M1,M2,M12),
   sort(M12,M).


%---------- model 1 -----------------

% P->Q must be read as (Q;\+ P)
formula1(1, F= ((\+ P,Q)->R), [F,P,Q,R]).
formula1(2, F= (P->((Q,R)->S)), [F,P,Q,R,S]).
formula1(3, F= (\+ (P; \+ Q), (S->T)), [F,P,Q,S,T]).
formula1(4, F= ((P->Q)->R), [F,P,Q,R]).
formula1(5, F= (\+ (P,Q),(P;Q)), [F,P,Q]).
formula1(6, F= (\+ ((P->Q),(Q->P))), [F,P,Q]).
%note: the second argument of the below may not read as F=X. 
%formula1(1, F= (\+ P,Q)->R, [F,P,Q,R]).
%formula1(2, F= P->((Q,R)->S), [F,P,Q,R,S]).
%formula1(4, F= (P->Q)->R, [F,P,Q,R]).


truth_value1(P,true):-proposition(P).
truth_value1(P,false):-proposition(P).
truth_value1((\+ true),false).
truth_value1((\+ false),true).
truth_value1((true,true),true).
truth_value1((true,false),false).
truth_value1((false,true),false).
truth_value1((false,false),false).
truth_value1((true;true),true).
truth_value1((true;false),true).
truth_value1((false;true),true).
truth_value1((false;false),false).
truth_value1(true->true,true).
truth_value1(true->false,false).
truth_value1(false->true,true).
truth_value1(false->false,true).


well_defined_formula1(P,T,[P=T]):-
   proposition(P),
   truth_value1(P,T).
well_defined_formula1(Q,T,M):-
   Q = (\+ P),
   well_defined_formula1(P,T1,M),
   truth_value1((\+ T1),T).
well_defined_formula1(Q,T,M):-
   Q = (P1,P2),
   well_defined_formula1(P1,T1,M1),
   well_defined_formula1(P2,T2,M2),
   truth_value1((T1,T2),T),
   union(M1,M2,M12),
   sort(M12,M),
   uniquely_assigned(M).
well_defined_formula1(Q,T,M):-
   Q = (P1;P2),
   well_defined_formula1(P1,T1,M1),
   well_defined_formula1(P2,T2,M2),
   truth_value1((T1;T2),T),
   union(M1,M2,M12),
   sort(M12,M),
   uniquely_assigned(M).
well_defined_formula1(Q,T,M):-
   Q = (P1->P2),
   well_defined_formula1(P1,T1,M1),
   well_defined_formula1(P2,T2,M2),
   truth_value1((T1->T2),T),
   union(M1,M2,M12),
   sort(M12,M),
   uniquely_assigned(M).


%------ truth value assignment -----------------------

uniquely_assigned_tvector(M,Ps,Ts):-
   findall(P0,
     (
      member(P0=_T0,M),
      uniquely_assigned(M,P0=_T0)
     ),
   Ps),
   findall(T0,
     (
      member(_P0=T0,M),
      uniquely_assigned(M,_P0=T0)
     ),
   Ts).

uniquely_assigned(M):-
   \+ (
     member(P0=_,M),
     \+ uniquely_assigned(M,P0=_)
   ).

uniquely_assigned(M,P0=X0):-
   assigned_values(M,P0,[X0]).

assigned_values(M,P0,X0):-
   member(P0=_,M),
   bagof(T0,member(P0=T0,M),X0).

%---------------------------------------
%   building the truth table
%---------------------------------------

interpretation0(A,F=B,[F|C]):-
  formula1(A,F=B,[F|C]),
  tvector0(C),
  ((B,F=true);((\+ B),F=fail)).

tvector0([]).
tvector0([X|Y]):-
  tvector0(Y),
  member(X,[true,fail]).


interpretation1(A,F=B,M):-
  formula0(A,B,_),
  well_defined_formula1(B,F,M).


a_row_of_truth_table(A,B,RT):-
  interpretation1(A,F=B,M),
  RT=[B=F|M].
  

truth_table(A,B,TT,OPT):-
  formula0(A,B,_),
  findall(RT,a_row_of_truth_table(A,B,RT),TT),
  optional_execution(TT,OPT).


optional_execution(_TT,[]).
optional_execution(TT,OPT):-
  member(p,OPT),
  forall(member([FC|RT],TT),
    (
     nl,
     write(RT),
     write(FC)
    )
  ).

optional_execution(TT,OPT):-
  member(w,OPT),
  forall(member([P0=T0|RT],TT),
    (
     nl,
     forall(member(P=T,RT),
       (
        align(right,4,P),
        write(' = '),
        align(left,5,T)
       )
     ),
     tab(5),write(P0),
     write(' = '),
     align(left,5,T0)
    )
  ).

optional_execution([[P0=_|RT0]|_],OPT):-
  member(h,OPT),
  nl,
  forall(member(P=_T,RT0),
    (
     tab(5),align(left,5,P)
    )
  ),
  tab(5),
  write(P0).

optional_execution(TT,OPT):-
  member(t,OPT),
  optional_execution(TT,[h]),
  optional_execution(TT,[l]),
  forall(member([_P0=T0|RT],TT),
    (
     nl,
     tab(5),
     forall(member(_P=T,RT),
       (
        align(left,10,T)
       )
     ),
     tab(5),
     write(T0)
    )
  ),
  optional_execution(TT,[l]).

optional_execution([RT0|_],OPT):-
  member(l,OPT),
  nl,
  tab(5),
  write('-----'),
  forall(member(_,RT0),
    (
     write('----------')
    )
  ).

%---------------------------------------
%   making normal forms
%---------------------------------------


a_basis(A,B=TF,(K,RT),Z):-
  truth_table(A,B,TT,[]),
  nth1(K,TT,[_=TF|RT]),
  findall(X,
    (
     member(Q=T,RT),
     (
      T=false -> X = (\+Q)
      ; X=Q
     )
    ),
  Z).   

normal_form(disjunctive,A,B,D):-
  formula0(A,B,_),
  findall(Z,
    (
     a_basis(A,B=true,_,Z)
    ),
  D).




% reduction by complementary pair
%---------------------------------------
reduced_normal_form(disjunctive,A,B,D,[]):-
  normal_form(disjunctive,A,B,C),
  reduce_normal_form(C,D,[]).

reduced_normal_form(disjunctive,A,B,D,[w]):-
  normal_form(disjunctive,A,B,C),
  forall(member(X,C),(nl,write(X))),
  reduce_normal_form(C,D,[w]).

reduce_normal_form(C,D,O):-
  reduce_normal_form0(C,C1,O),
  reduce_normal_form(C1,D,O).
reduce_normal_form(C,C,O):-
  \+ reduce_normal_form0(C,_,O).

% reduce a NF by complementary pair : merge of nodes set  
reduce_normal_form0(C,D,O):-
  member(X,C),
  member(Y,X),
  member(X1,C),X1 \= X,
  member((\+ Y),X1),
  subtract(X,[Y],X0),
  subtract(X1,[(\+ Y)],X0),
  subtract(C,[X,X1],C1),
  append(C1,[X0],D),
  write_option_reduced(X-X1-X0,O).

write_option_reduced(_-_-_,[]).
write_option_reduced(X-X1-X0,O):-
  member(w,O),
  nl,
  write(reduced(X-X1-X0)).



minimal_reduced_normal_form(disjunctive,A,B,D,O):-
  caution_on_complexity(A,B),
  reduced_normal_form(disjunctive,A,B,D0,O),
  length(D0,N),
  \+ (
    reduced_normal_form(disjunctive,A,B,D1,[]),
    length(D1,N1),
    N1 < N
  ),
  sort(D0,D).

all_minimal_reduced_normal_forms(disjunctive,A,B,S):-
  formula0(A,B,_),
  caution_on_complexity(A,B),
  findall(D,
    (
     minimal_reduced_normal_form(disjunctive,A,B,D,[])
    ),
  Z),
  sort(Z,S),
  forall(member(X,S),(nl,write(X))).



%minimal_length_description_reduced_normal_form
%------------------------------------------------

reduced_MLD_normal_form(disjunctive,A,B,D,[]):-
  reduced_normal_form(disjunctive,A,B,C,[]),
  reduce_MLD_normal_form(C,D,[]).

reduced_MLD_normal_form(disjunctive,A,B,D,[w]):-
  reduced_normal_form(disjunctive,A,B,C,[]),
  forall(member(X,C),(nl,write(X))),
  reduce_MLD_normal_form(C,D,[w]).

reduce_MLD_normal_form(C,D,O):-
  reduce_MLD_normal_form0(C,C1,O),
  reduce_MLD_normal_form(C1,D,O).
reduce_MLD_normal_form(C,C,O):-
  \+ reduce_MLD_normal_form0(C,_C1,O).

reduce_MLD_normal_form0(C,D,O):-
  member([X],C),
  member(Y,C),Y \= [X],
  member((\+ X),Y),
  subtract(Y,[(\+ X)],Y0),
  subtract(C,[Y],C1),
  append(C1,[Y0],D),
  write_option_reduced(Y-[\+ X]-Y0,O).
reduce_MLD_normal_form0(C,D,O):-
  member([\+ X],C),
  member(Y,C),Y \= [\+ X],
  member(X,Y),
  subtract(Y,[X],Y0),
  subtract(C,[Y],C1),
  append(C1,[Y0],D),
  write_option_reduced(Y-[X]-Y0,O).


minimal_reduced_MLD_normal_form(disjunctive,A,B,D,O):-
  caution_on_complexity(A,B),
  reduced_MLD_normal_form(disjunctive,A,B,D0,O),
  length(D0,N),
  \+ (
    reduced_MLD_normal_form(disjunctive,A,B,D1,[]),
    length(D1,N1),
    N1 < N
  ),
  sort(D0,D).

all_minimal_reduced_MLD_normal_forms(disjunctive,A,B,S):-
  formula0(A,B,_),
  caution_on_complexity(A,B),
  findall(D,
    (
     minimal_reduced_MLD_normal_form(disjunctive,A,B,D,[])
    ),
  Z),
  sort(Z,S),
  forall(member(X,S),(nl,write(X))).



caution_on_complexity(A,B):-
  normal_form(disjunctive,A,B,D),
  length(D,N),
  (
   N =< 10 ->true
   ;
   (
    length(D,N),
    N > 10,
    nl,
    write('Target:'),
    nl,
    write(D),
    nl,
    write('Warning:'),
    nl,
    write(' This formula may cause the complexity problem. Are you ok?'),
    nl,
    read(Y),
    (Y=y->true;(!,fail))
   )
  ).



/* %---- sample execution

?- reduced_normal_form(disjunctive,B,C,D).

[p, q, r]
[p, q, \+r]
[p, \+q, r]
[p, \+q, \+r]
[\+p, q, r]
[\+p, \+q, r]
[\+p, \+q, \+r]
reduced([p, q, r]-[\+p, q, r]-[q, r])
reduced([p, q, \+r]-[p, \+q, \+r]-[p, \+r])
reduced([p, \+q, r]-[\+p, \+q, r]-[\+q, r])
reduced([q, r]-[\+q, r]-[r])

B = 1
C = \+p, q->r
D = [[\+p, \+q, \+r], [p, \+r], [r]] 

Yes
?- 
*/

/* %---- sample execution

14 ?- formula0(1,A,B),well_defined_formula0(B,T,M).

A = '�i�`‚o�È‚p�j�¨‚q'
B = and(not p, q) -> r
T = true
M = [p = true,q = true,r = true] ;

A = '�i�`‚o�È‚p�j�¨‚q'
B = and(not p, q) -> r
T = true
M = [p = true,q = true,r = false] ;

A = '�i�`‚o�È‚p�j�¨‚q'
B = and(not p, q) -> r
T = true
M = [p = true,q = false,r = true] ;

A = '�i�`‚o�È‚p�j�¨‚q'
B = and(not p, q) -> r
T = true
M = [p = true,q = false,r = false] 

%---omit
14 ?- formula0(1,A,B),well_defined_formula0(B,T,M).

A = '�i�`‚o�È‚p�j�¨‚q'
B = and(not p, q) -> r
T = true
M = [p = true,q = true,r = true] ;

A = '�i�`‚o�È‚p�j�¨‚q'
B = and(not p, q) -> r
T = true
M = [p = true,q = true,r = false] ;

A = '�i�`‚o�È‚p�j�¨‚q'
B = and(not p, q) -> r
T = true
M = [p = true,q = false,r = true] ;

A = '�i�`‚o�È‚p�j�¨‚q'
B = and(not p, q) -> r
T = true
M = [p = true,q = false,r = false] 

%---omit
*/







subformula0(and(A,_B),A).
subformula0(and(_A,B),B).
subformula0(or(A,_B),A).
subformula0(or(_A,B),B).
subformula0(A->_B,A).
subformula0(_A->B,B).
subformula0(not(A),A).


%--------------- rewriting rules -----------------------
%“™‰¿�‘‚«Š·‚¦ƒ‹�[ƒ‹

rule(1,equivalent,(F,'<-->', G) = and((F->G),(G->F))).
rule(2,implication,(F->G)=or(not(F),G)).
rule(3,associative,or(F,G)=or(G,F)).
rule(4,commutative,and(F,G)=and(G,F)).
rule(5,commutative,or(or(F,G),H)=or(F,or(G,H))).
rule(6,associative,and(and(F,G),H)=and(F,and(G,H))).
rule(7,distributive,or(F,and(G,H))=and(or(F,G),or(F,H))).
rule(8,distributive,and(F,or(G,H))=or(and(F,G),and(F,H))).
rule(9,inconsistent,or(F,[])=F).
rule(10,inconsistent,and(_F,[])=[]).
rule(11,valid,or(_F,[@])=[@]).
rule(12,valid,and(F,[@])=F).
rule(13,complement,or(F,not(F))=[@]).
rule(14,complement,and(F,not(F))=� ).
rule(15,double_negation,not(not(F))=F).
rule(16,demorgan,not(or(F,G))=and(not(F),not(G))).
rule(17,demorgan,not(and(F,G))=or(not(F),not(G))).
/*
F<-->G=(F->G)�È(F->G)
F�¨G=�`F�ÉG
F�ÉG=G�ÉF
F�ÈG=G�ÈF
(F�ÉG)�ÉH=F�É(G�ÉH)
(F�ÈG)�ÈH=F�È(G�ÈH)
F�É(G�ÈH)=(F�ÉG)�È(F�ÉH)
F�È(G�ÉH)=(F�ÈG)�É(F�ÈH)
F�É� =F
F�È� =� 
F�É�¡=�¡
F�È�¡=F
F�É�`F=�¡
F�È�`F=� 
�`(�`F)=F
�`(F�ÉG)=�`F�È�`G
�`(F�ÈG)=�`F�É�`G
*/


rule1(1,equivalent, [(F,'<-->', G),((F->G),(G->F))]).
rule1(2,implication, [(F->G), (G;\+ F)]).
rule1(3,associative, [(F;G), (G;F)]).
rule1(4,commutative, [(F,G), (G,F)]).
rule1(5,commutative, [((F;G);H), (F;(G;H))]).
rule1(6,associative, [((F,G),H), (F,(G,H))]).
rule1(7,distributive, [(F;(G,H)), ((F;G),(F;H))]).
rule1(8,distributive, [(F,(G;H)), ((F,G);(F,H))]).
rule1(9,inconsistent, [(F;false), F]).
rule1(10,inconsistent, [(_F,false), false]).
rule1(11,valid, [(_F;true), true]).
rule1(12,valid, [(F,true), F]).
rule1(13,complement, [(F;\+F), true]).
rule1(14,complement, [(F,\+F), false]).
rule1(15,double_negation, [\+ (\+ F), F]).
rule1(16,demorgan, [\+ (F;G), (\+F,\+G)]).
rule1(17,demorgan, [\+ (F,G), (\+F;\+G)]).

rephrase(formula0(A),from(B),to(E),by_rule(N,M)):-
 formula0(A,B,_C),rule1(N,M,D),member(B,D),member(E,D),E\=B.


/*  
%---------------------------------------
?- rephrase(A,B,C,D).

A = formula0(1)
B = from((\+p, q->r))
C = to((r;\+ (\+p, q)))
D = by_rule(2, implication) ;

A = formula0(1)
B = from((\+p, q->r))
C = to((\+p, q->r;false))
D = by_rule(9, inconsistent) ;

A = formula0(1)
B = from((\+p, q->r))
C = to(((\+p, q->r), true))
D = by_rule(12, valid) 

Yes
%---------------------------------------
*/

%-------------------------------------
% utilities
%-------------------------------------


% prity print.
%-------------------------------------

align(left,N,M):- pp2(N,M).
align(right,N,M):- pp(N,M).

% left align
pp2(0,_,_).
%pp2(0,[],[]).
%pp2(0,Y,_Z):-   Y \= [],   pp2(0,[],[]).
pp2(N,[X|Y],[X|Z]):-
   N > 0,
   N1 is N -1,%(N1=0->trace;true),
   pp2(N1,Y,Z).
pp2(N,[],[' '|Z]):-
   N > 0,
   N1 is N -1,
   pp2(N1,[],Z).
pp2(N,X):-
   list_name(X,_Y,X1),
   pp2(N,X1,Z),
   list_name(Q,_W,Z),
   write(Q).

pp1(0,[],[]).
pp1(N,[X|Y],[X|Z]):-
   length([X|Y],L),
   N = L,
   N1 is N -1,
   pp1(N1,Y,Z).
pp1(N,Y,[' '|Z]):-
   length(Y,L),
   N > L,
   N1 is N -1,
   pp1(N1,Y,Z).
pp1(N,[X|Y],Z):-
   length([X|Y],L),
   N < L,
   N1 is N -1,
   pp1(N1,Y,Z).
pp1(N,X):-
   list_name(X,_Y,X1),
   pp1(N,X1,Z),
   list_name(Q,_W,Z),
   write(Q).

pp0(0,[]).
pp0(N,[X|Y]):-
   length([X|Y],L),
   N = L,
   write(X),
   N1 is N -1,
   pp0(N1,Y).
pp0(N,Y):-
   length(Y,L),
   N > L,
   write(' '),
   N1 is N -1,
   pp0(N1,Y).
pp0(N,[X|Y]):-
   length([X|Y],L),
   N < L,
   N1 is N -1,
   pp0(N1,Y).

% right align
pp(N,X):-
   list_name(X,_Y,X1),
   pp0(N,X1).

list_name0([],[]).
list_name0([X|Y],[Z|W]):-
   name(Z,[X]),
   list_name0(Y,W).

list_name(X,W,Y):-
   \+ var(X),
   name(X,W),
   list_name0(W,Y).
list_name(X,W,Y):-
   var(X),
   (\+ var(Y); \+ var(W)),
   list_name0(W,Y),
   name(X,W).


% tell a successful goal
%--------------------------------

tell_goal(File,G):-
   (current_stream(File,write,S0)->close(S0);true),
   open(File,write,S),
   tell(File),
   nl,
   tstamp('% file output start time ',_),
   nl,
   write('%----------  start from here ------------%'),
   nl,
   G,
   nl,
   write('%----------  end of data ------------%'),
   nl,
   tstamp('% file output end time ',_),
   tell(user),
   close(S),
   % The following is to cope with the duplicated stream problem.
   (current_stream(File,write,S1)->close(S1);true).


% tell all successful goal
%--------------------------------

tell_goal(File,forall,G):-
   G0 = (nl,write(G),write('.')),
   G1 = forall(G,G0),
   tell_goal(File,G1).


% time stamp
%--------------------------------

tstamp(no,T):-
   get_time(U),
   convert_time(U,A,B,C,D,E,F,_G),
   T = [date(A/B/C), time(D:E:F)],
   nl.

tstamp(Word,T):-
   \+ var(Word),
   Word \= no,
   get_time(U),
   convert_time(U,A,B,C,D,E,F,_G),
   T = [date(A/B/C), time(D:E:F)],
%   format('~`.t~t~a~30|~`.t~t~70|~n',[Word]),
   write((Word,T)),
   nl.