20
21:- op(1130, xfy, <=>). 22:- op(1110, xfy, =>). 25:- op( 500, fy, ~). 26:- op( 500, fy, all). 27:- op( 500, fy, ex). 28:- op( 500,xfy, :). 29
30
51
52make_matrix(Fml,Matrix,Set) :-
53 univar(Fml,[],F1),
54 ( member(conj,Set), F1=(A=>C) -> F2=((A,#)=>(#,C)) ; F2=F1 ),
55 ( member(nodef,Set) ->
56 def_nnf(F2,NNF,1,_,nnf), dnf(NNF,DNF)
57 ;
58 \+member(def,Set), F2=(B=>D) ->
59 def_nnf(~(B),NNF,1,I,nnf), dnf(NNF,DNF1),
60 def_nnf(D,DNF2,I,_,def), DNF=(DNF2;DNF1)
61 ;
62 def_nnf(F2,DNF,1,_,def)
63 ),
64 mat(DNF,M),
65 ( member(reo(I),Set) -> mreorder(M,Matrix,I) ; Matrix=M ).
66
74
75def_nnf(Fml,DEF,I,I1,Set) :-
76 def(Fml,[],NNF,DEF1,_,I,I1,Set), def(DEF1,NNF,DEF).
77
78def([],Fml,Fml).
79def([(A,(B;C))|DefL],DEF,Fml) :- !, def([(A,B),(A,C)|DefL],DEF,Fml).
80def([A|DefL],DEF,Fml) :- def(DefL,(A;DEF),Fml).
81
82def(Fml,FreeV,NNF,DEF,Paths,I,I1,Set) :-
83 ( Fml = ~(~A) -> Fml1 = A;
84 Fml = ~(all X:F) -> Fml1 = (ex X: ~F);
85 Fml = ~(ex X:F) -> Fml1 = (all X: ~F);
86 Fml = ~((A ; B)) -> Fml1 = ((~A , ~B));
87 Fml = ~((A , B)) -> Fml1 = (~A ; ~B);
88 Fml = (A => B) -> Fml1 = (~A ; B);
89 Fml = ~((A => B))-> Fml1 = ((A , ~B));
90 Fml = (A <=> B) ->
91 ( Set=def -> Fml1 = ((A => B) , (B => A));
92 Fml1 = ((A , B) ; (~A , ~B)) );
93 Fml = ~((A<=>B)) -> Fml1 = ((A , ~B) ; (~A , B)) ), !,
94 def(Fml1,FreeV,NNF,DEF,Paths,I,I1,Set).
95
96def((ex X:F),FreeV,NNF,DEF,Paths,I,I1,Set) :- !,
97 def(F,[X|FreeV],NNF,DEF,Paths,I,I1,Set).
98
99def((all X:Fml),FreeV,NNF,DEF,Paths,I,I1,Set) :- !,
100 copy_term((X,Fml,FreeV),((I^FreeV),Fml1,FreeV)), I2 is I+1,
101 def(Fml1,FreeV,NNF,DEF,Paths,I2,I1,Set).
102
103def((A ; B),FreeV,NNF,DEF,Paths,I,I1,Set) :- !,
104 def(A,FreeV,NNF1,DEF1,Paths1,I,I2,Set),
105 def(B,FreeV,NNF2,DEF2,Paths2,I2,I1,Set),
106 append(DEF1,DEF2,DEF), Paths is Paths1 * Paths2,
107 (Paths1 > Paths2 -> NNF = (NNF2;NNF1);
108 NNF = (NNF1;NNF2)).
109
110def((A , B),FreeV,NNF,DEF,Paths,I,I1,Set) :- !,
111 def(A,FreeV,NNF3,DEF3,Paths1,I,I2,Set),
112 ( NNF3=(_;_), Set=def -> append([(~I2^FreeV,NNF3)],DEF3,DEF1),
113 NNF1=I2^FreeV, I3 is I2+1 ;
114 DEF1=DEF3, NNF1=NNF3, I3 is I2 ),
115 def(B,FreeV,NNF4,DEF4,Paths2,I3,I4,Set),
116 ( NNF4=(_;_), Set=def -> append([(~I4^FreeV,NNF4)],DEF4,DEF2),
117 NNF2=I4^FreeV, I1 is I4+1 ;
118 DEF2=DEF4, NNF2=NNF4, I1 is I4 ),
119 append(DEF1,DEF2,DEF), Paths is Paths1 + Paths2,
120 (Paths1 > Paths2 -> NNF = (NNF2,NNF1);
121 NNF = (NNF1,NNF2)).
122
123def(Lit,_,Lit,[],1,I,I,_).
124
131
132dnf(((A;B),C),(F1;F2)) :- !, dnf((A,C),F1), dnf((B,C),F2).
133dnf((A,(B;C)),(F1;F2)) :- !, dnf((A,B),F1), dnf((A,C),F2).
134dnf((A,B),F) :- !, dnf(A,A1), dnf(B,B1),
135 ( (A1=(C;D);B1=(C;D)) -> dnf((A1,B1),F) ; F=(A1,B1) ).
136dnf((A;B),(A1;B1)) :- !, dnf(A,A1), dnf(B,B1).
137dnf(Lit,Lit).
138
145
146mat((A;B),M) :- !, mat(A,MA), mat(B,MB), append(MA,MB,M).
147mat((A,B),M) :- !, (mat(A,[CA]),mat(B,[CB]) -> union2(CA,CB,M);M=[]).
148mat(~Lit,[[-Lit]]) :- !.
149mat(Lit,[[Lit]]).
150
157
158univar(X,_,X) :- (atomic(X);var(X);X==[[]]), !.
159univar(F,Q,F1) :-
160 F=..[A,B|T], ( (A=ex;A=all) -> B=(X:C), delete2(Q,X,Q1),
161 copy_term((X,C,Q1),(Y,D,Q1)), univar(D,[Y|Q],D1), F1=..[A,Y:D1] ;
162 univar(B,Q,B1), univar(T,Q,T1), F1=..[A,B1|T1] ).
163
166
167union2([],L,[L]).
168union2([X|L1],L2,M) :- member2(X,L2), !, union2(L1,L2,M).
169union2([X|_],L2,M) :- (-Xn=X;-X=Xn) -> member2(Xn,L2), !, M=[].
170union2([X|L1],L2,M) :- union2(L1,[X|L2],M).
171
172member2(X,[Y|_]) :- X==Y, !.
173member2(X,[_|T]) :- member2(X,T).
174
177
178delete2([],_,[]).
179delete2([X|T],Y,T1) :- X==Y, !, delete2(T,Y,T1).
180delete2([X|T],Y,[X|T1]) :- delete2(T,Y,T1).
181
184
185mreorder(M,M,0) :- !.
186mreorder(M,M1,I) :-
187 length(M,L), K is L//3, append(A,D,M), length(A,K),
188 append(B,C,D), length(C,K), mreorder2(C,A,B,M2), I1 is I-1,
189 mreorder(M2,M1,I1).
190
191mreorder2([],[],C,C).
192mreorder2([A|A1],[B|B1],[C|C1],[A,B,C|M1]) :- mreorder2(A1,B1,C1,M1)