You selected logic01.pl
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È‚pj¨‚q',and(not(p),q)->r).
formula0(2,'‚o¨ii‚pÈ‚qj¨‚rj', p->(and(q,r)->s)).
formula0(3,'`i‚oÉ`‚pjÈi‚r¨‚sj', and(not(or(p,not(q))),s->t)).
formula0(4,'i‚o¨‚pj¨‚q',((p->q)->r)).
formula0(5,'`i‚oÈ‚pjÈi‚oÉ‚pj',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È‚pj¨‚q'
B = and(not p, q) -> r
T = true
M = [p = true,q = true,r = true] ;
A = 'i`‚oÈ‚pj¨‚q'
B = and(not p, q) -> r
T = true
M = [p = true,q = true,r = false] ;
A = 'i`‚oÈ‚pj¨‚q'
B = and(not p, q) -> r
T = true
M = [p = true,q = false,r = true] ;
A = 'i`‚oÈ‚pj¨‚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È‚pj¨‚q'
B = and(not p, q) -> r
T = true
M = [p = true,q = true,r = true] ;
A = 'i`‚oÈ‚pj¨‚q'
B = and(not p, q) -> r
T = true
M = [p = true,q = true,r = false] ;
A = 'i`‚oÈ‚pj¨‚q'
B = and(not p, q) -> r
T = true
M = [p = true,q = false,r = true] ;
A = 'i`‚oÈ‚pj¨‚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.
return to front page.