1 %% This file consists of three parts
:
3 %% (2) ncDP
: A Non
-Clausal Form Decision Procedure
4 %% (3) A simple interface tp
/4 that uses leancop
and ncdp to compute
7 %% This file is provided
for your convenience
, but you may as well
8 %% use the original software
.
10 %% Leancop
and ncDP are copyright Jens Otten
(see www
.leancop
.de
).
12 %% For documentation of these tools
, we refer to the webpage above
.
15 :- op
(1130, xfy
, <=>). % equivalence
16 :- op
(1110, xfy
, =>). % implication
19 :- op
( 500, fy
, ~). % negation
20 :- op
( 500, fy
, all
). % universal quantifier
21 :- op
( 500, fy
, ex
). % existential quantifier
25 % ------------------------------------------------------------------
26 % make_matrix
(+Fml
,-Matrix
,+Settings
)
27 % - transform first
-order formula into set of clauses
(matrix
)
29 % Fml
, Matrix
: first
-order formula
and matrix
31 % Settings
: list of settings
, which can contain def
, nodef
and conj
;
32 % if it contains nodef
/def
, no definitional transformation
33 % or a complete definitional transformation is done
,
34 % otherwise a definitional transformation is done
for
35 % the conjecture
and the standard transformation is done
36 % for the axioms
; conjecture is marked
if conj is
given
38 % Syntax of Fml
: negation
'~', disjunction
';', conjunction
',',
39 % implication
'=>', equivalence
'<=>', universal
/existential
40 % quantifier
'all X:<Formula>'/'ex X:<Formula>' where
'X' is a
41 % Prolog variable
, and atomic formulae are Prolog atoms
.
43 % Example
: make_matrix
(ex Y
:(all X
:((p
(Y
) => p
(X
)))),Matrix
,[]).
44 % Matrix
= [[-(p
(X1
))], [p
(1 ^ [X1
])]]
46 make_matrix
(Fml
,Matrix
,Set
) :-
48 ( member
(conj
,Set
), F1
=(A
=>C
) -> F2
=((A
,#)=>(#,C)) ; F2=F1 ),
49 ( member
(nodef
,Set
) ->
50 def_nnf
(F2
,NNF
,1,_
,nnf
), dnf
(NNF
,DNF
)
52 \
+member
(def
,Set
), F2
=(B
=>D
) ->
53 def_nnf
(~(B
),NNF
,1,I
,nnf
), dnf
(NNF
,DNF1
),
54 def_nnf
(D
,DNF2
,I
,_
,def
), DNF
=(DNF2
;DNF1
)
56 def_nnf
(F2
,DNF
,1,_
,def
)
59 ( member
(reo
(I
),Set
) -> mreorder
(M
,Matrix
,I
) ; Matrix
=M
).
61 % ------------------------------------------------------------------
62 % def_nnf
(+Fml
,-DEF
) - transform formula into a definitional
63 % Skolemized negation normal form
(DEF
)
64 % Fml
, DEF
: first
-order formula
and formula
in DEF
66 % Example
: def_nnf
(ex Y
:(all X
:((p
(Y
) => p
(X
)))),DEF
,def
).
67 % DEF
= ~ p
(X1
) ; p
(1 ^ [X1
])
69 def_nnf
(Fml
,DEF
,I
,I1
,Set
) :-
70 def
(Fml
,[],NNF
,DEF1
,_
,I
,I1
,Set
), def
(DEF1
,NNF
,DEF
).
73 def
([(A
,(B
;C
))|DefL
],DEF
,Fml
) :- !, def
([(A
,B
),(A
,C
)|DefL
],DEF
,Fml
).
74 def
([A
|DefL
],DEF
,Fml
) :- def
(DefL
,(A
;DEF
),Fml
).
76 def
(Fml
,FreeV
,NNF
,DEF
,Paths
,I
,I1
,Set
) :-
77 ( Fml
= ~(~A
) -> Fml1
= A
;
78 Fml
= ~(all X
:F
) -> Fml1
= (ex X
: ~F
);
79 Fml
= ~(ex X
:F
) -> Fml1
= (all X
: ~F
);
80 Fml
= ~((A
; B
)) -> Fml1
= ((~A
, ~B
));
81 Fml
= ~((A
, B
)) -> Fml1
= (~A
; ~B
);
82 Fml
= (A
=> B
) -> Fml1
= (~A
; B
);
83 Fml
= ~((A
=> B
))-> Fml1
= ((A
, ~B
));
85 ( Set
=def
-> Fml1
= ((A
=> B
) , (B
=> A
));
86 Fml1
= ((A
, B
) ; (~A
, ~B
)) );
87 Fml
= ~((A
<=>B
)) -> Fml1
= ((A
, ~B
) ; (~A
, B
)) ), !,
88 def
(Fml1
,FreeV
,NNF
,DEF
,Paths
,I
,I1
,Set
).
90 def
((ex X
:F
),FreeV
,NNF
,DEF
,Paths
,I
,I1
,Set
) :- !,
91 def
(F
,[X
|FreeV
],NNF
,DEF
,Paths
,I
,I1
,Set
).
93 def
((all X
:Fml
),FreeV
,NNF
,DEF
,Paths
,I
,I1
,Set
) :- !,
94 copy_term
((X
,Fml
,FreeV
),((I
^FreeV
),Fml1
,FreeV
)), I2 is I
+1,
95 def
(Fml1
,FreeV
,NNF
,DEF
,Paths
,I2
,I1
,Set
).
97 def
((A
; B
),FreeV
,NNF
,DEF
,Paths
,I
,I1
,Set
) :- !,
98 def
(A
,FreeV
,NNF1
,DEF1
,Paths1
,I
,I2
,Set
),
99 def
(B
,FreeV
,NNF2
,DEF2
,Paths2
,I2
,I1
,Set
),
100 append
(DEF1
,DEF2
,DEF
), Paths is Paths1
* Paths2
,
101 (Paths1
> Paths2
-> NNF
= (NNF2
;NNF1
);
104 def
((A
, B
),FreeV
,NNF
,DEF
,Paths
,I
,I1
,Set
) :- !,
105 def
(A
,FreeV
,NNF3
,DEF3
,Paths1
,I
,I2
,Set
),
106 ( NNF3
=(_
;_
), Set
=def
-> append
([(~I2
^FreeV
,NNF3
)],DEF3
,DEF1
),
107 NNF1
=I2
^FreeV
, I3 is I2
+1 ;
108 DEF1
=DEF3
, NNF1
=NNF3
, I3 is I2
),
109 def
(B
,FreeV
,NNF4
,DEF4
,Paths2
,I3
,I4
,Set
),
110 ( NNF4
=(_
;_
), Set
=def
-> append
([(~I4
^FreeV
,NNF4
)],DEF4
,DEF2
),
111 NNF2
=I4
^FreeV
, I1 is I4
+1 ;
112 DEF2
=DEF4
, NNF2
=NNF4
, I1 is I4
),
113 append
(DEF1
,DEF2
,DEF
), Paths is Paths1
+ Paths2
,
114 (Paths1
> Paths2
-> NNF
= (NNF2
,NNF1
);
117 def
(Lit
,_
,Lit
,[],1,I
,I
,_
).
119 % ------------------------------------------------------------------
120 % dnf
(+NNF
,-DNF
) - transform formula
in NNF into formula
in DNF
121 % NNF
, DNF
: formulae
in NNF
and DNF
123 % Example
: dnf
(((p
;~p
),(q
;~q
)),DNF
).
124 % DNF
= (p
, q
; p
, ~ q
) ; ~ p
, q
; ~ p
, ~ q
126 dnf
(((A
;B
),C
),(F1
;F2
)) :- !, dnf
((A
,C
),F1
), dnf
((B
,C
),F2
).
127 dnf
((A
,(B
;C
)),(F1
;F2
)) :- !, dnf
((A
,B
),F1
), dnf
((A
,C
),F2
).
128 dnf
((A
,B
),F
) :- !, dnf
(A
,A1
), dnf
(B
,B1
),
129 ( (A1
=(C
;D
);B1
=(C
;D
)) -> dnf
((A1
,B1
),F
) ; F
=(A1
,B1
) ).
130 dnf
((A
;B
),(A1
;B1
)) :- !, dnf
(A
,A1
), dnf
(B
,B1
).
133 % ------------------------------------------------------------------
134 % mat
(+DNF
,-Matrix
) - transform formula
in DNF into matrix
135 % DNF
, Matrix
: formula
in DNF
, matrix
137 % Example
: mat
(((p
, q
; p
, ~ q
) ; ~ p
, q
; ~ p
, ~ q
),Matrix
).
138 % Matrix
= [[p
, q
], [p
, -(q
)], [-(p
), q
], [-(p
), -(q
)]]
140 mat
((A
;B
),M
) :- !, mat
(A
,MA
), mat
(B
,MB
), append
(MA
,MB
,M
).
141 mat
((A
,B
),M
) :- !, (mat
(A
,[CA
]),mat
(B
,[CB
]) -> union2
(CA
,CB
,M
);M
=[]).
142 mat
(~Lit
,[[-Lit
]]) :- !.
145 % ------------------------------------------------------------------
146 % univar
(+Fml
,[],-Fml1
) - rename variables
147 % Fml
, Fml1
: first
-order formulae
149 % Example
: univar
((all X
:(p
(X
) => (ex X
:p
(X
)))),[],F1
).
150 % F1
= all Y
: (p
(Y
) => ex Z
: p
(Z
))
152 univar
(X
,_
,X
) :- (atomic
(X
);var
(X
);X
==[[]]), !.
154 F
=..[A
,B
|T
], ( (A
=ex
;A
=all
) -> B
=(X
:C
), delete2
(Q
,X
,Q1
),
155 copy_term
((X
,C
,Q1
),(Y
,D
,Q1
)), univar
(D
,[Y
|Q
],D1
), F1
=..[A
,Y
:D1
] ;
156 univar
(B
,Q
,B1
), univar
(T
,Q
,T1
), F1
=..[A
,B1
|T1
] ).
158 % ------------------------------------------------------------------
159 % union2
/member2
- union
and member
for lists without unification
162 union2
([X
|L1
],L2
,M
) :- member2
(X
,L2
), !, union2
(L1
,L2
,M
).
163 union2
([X
|_
],L2
,M
) :- (-Xn
=X
;-X
=Xn
) -> member2
(Xn
,L2
), !, M
=[].
164 union2
([X
|L1
],L2
,M
) :- union2
(L1
,[X
|L2
],M
).
166 member2
(X
,[Y
|_
]) :- X
==Y
, !.
167 member2
(X
,[_
|T
]) :- member2
(X
,T
).
169 % ------------------------------------------------------------------
170 % delete2
- delete variable from list
173 delete2
([X
|T
],Y
,T1
) :- X
==Y
, !, delete2
(T
,Y
,T1
).
174 delete2
([X
|T
],Y
,[X
|T1
]) :- delete2
(T
,Y
,T1
).
176 % ------------------------------------------------------------------
177 % mreorder
- reorder clauses
179 mreorder
(M
,M
,0) :- !.
181 length(M
,L
), K is L
//3, append
(A
,D
,M
), length(A
,K
),
182 append
(B
,C
,D
), length(C
,K
), mreorder2
(C
,A
,B
,M2
), I1 is I
-1,
185 mreorder2
([],[],C
,C
).
186 mreorder2
([A
|A1
],[B
|B1
],[C
|C1
],[A
,B
,C
|M1
]) :- mreorder2
(A1
,B1
,C1
,M1
).
188 :- dynamic
(pathlim
/0), dynamic
(lit
/4).
191 %%% prove matrix M
/ formula F
193 prove
(F
,Proof
) :- prove2
(F
,[cut
,comp
(7)],Proof
).
195 prove2
(F
,Set
,Proof
) :-
196 (F
=[_
|_
] -> M
=F
; make_matrix
(F
,M
,Set
)),
197 retractall
(lit
(_
,_
,_
,_
)), (member
([-(#)],M) -> S=conj ; S=pos),
198 assert_clauses
(M
,S
), prove
(1,Set
,Proof
).
200 prove
(PathLim
,Set
,Proof
) :-
201 \
+member
(scut
,Set
) -> prove
([-(#)],[],PathLim,[],Set,[Proof]) ;
202 lit
(#,_,C,_) -> prove(C,[-(#)],PathLim,[],Set,Proof1),
204 prove
(PathLim
,Set
,Proof
) :-
205 member
(comp
(Limit
),Set
), PathLim
=Limit
-> prove
(1,[],Proof
) ;
206 (member
(comp
(_
),Set
);retract
(pathlim
)) ->
207 PathLim1 is PathLim
+1, prove
(PathLim1
,Set
,Proof
).
209 %%% leanCoP core prover
211 prove
([],_
,_
,_
,_
,[]).
213 prove
([Lit
|Cla
],Path
,PathLim
,Lem
,Set
,Proof
) :-
214 Proof
=[[[NegLit
|Cla1
]|Proof1
]|Proof2
],
215 \
+ (member
(LitC
,[Lit
|Cla
]), member
(LitP
,Path
), LitC
==LitP
),
216 (-NegLit
=Lit
;-Lit
=NegLit
) ->
217 ( member
(LitL
,Lem
), Lit
==LitL
, Cla1
=[], Proof1
=[]
219 member
(NegL
,Path
), unify_with_occurs_check
(NegL
,NegLit
),
222 lit
(NegLit
,NegL
,Cla1
,Grnd1
),
223 unify_with_occurs_check
(NegL
,NegLit
),
224 ( Grnd1
=g
-> true
; length(Path
,K
), K
<PathLim
-> true
;
225 \
+ pathlim
-> assert
(pathlim
), fail
),
226 prove
(Cla1
,[Lit
|Path
],PathLim
,Lem
,Set
,Proof1
)
228 ( member
(cut
,Set
) -> ! ; true
),
229 prove
(Cla
,Path
,PathLim
,[Lit
|Lem
],Set
,Proof2
).
231 %%% write clauses into Prolog
's database
233 assert_clauses([],_).
234 assert_clauses([C|M],Set) :-
235 (Set\=conj, \+member(-_,C) -> C1=[#|C] ; C1=C),
236 (ground(C) -> G=g ; G=n), assert_clauses2(C1,[],G),
237 assert_clauses(M,Set).
239 assert_clauses2([],_,_).
240 assert_clauses2([L|C],C1,G) :-
241 assert_renvar([L],[L2]), append(C1,C,C2), append(C1,[L],C3),
242 assert(lit(L2,L,C2,G)), assert_clauses2(C,C3,G).
244 assert_renvar([],[]).
245 assert_renvar([F|FunL],[F1|FunL1]) :-
246 ( var(F) -> true ; F=..[Fu|Arg], assert_renvar(Arg,Arg1),
247 F1=..[Fu|Arg1] ), assert_renvar(FunL,FunL1).
253 bmatrix((~X),Pol,M) :- !, Pol1 is (1-Pol), bmatrix(X,Pol1,M).
254 bmatrix((X1<=>X2),Pol,M) :- !, bmatrix(((X1=>X2),(X2=>X1)),Pol,M).
255 bmatrix(X,Pol,M3) :- X=..[F,X1,X2], alpha(F,Pol,Pol1,Pol2), !,
256 bmatrix(X1,Pol1,M1), bmatrix(X2,Pol2,M2),
258 bmatrix(X,Pol,[M3]) :- X=..[F,X1,X2], beta(F,Pol,Pol1,Pol2), !,
259 bmatrix(X1,Pol1,M1), bmatrix(X2,Pol2,M2),
260 sim(M1,M4), sim(M2,M5), union(M4,M5,M3).
264 sim([M],M) :- !. sim(M,[M]).
266 alpha(',',1,1,1):-!. alpha(';',0,0,0):-!. alpha((=>),0,1,0):-!.
267 beta(',',0,0,0):-!. beta(';',1,1,1):-!. beta((=>),1,0,1):-!.
271 prove(F) :- bmatrix(F,0,M), pure(M,M1), dp(M1).
273 %%% dp (non-clausal DP)
276 dp(M) :- member([],M), !.
279 dp(M) :- member([L],M), ( atom(L), N= -L ; -N=L ), !,
280 reduce(M,N,L,M1), dp(M1).
283 dp([[[C1|M],[C2|M2]|C]|M1]) :- !,
284 dp([[[C1|M]]|M1]), dp([[[C2|M2]]|M1]), dp([C|M1]).
287 dp(M) :- selectLit(M,P,N),
288 reduce(M,P,N,M1), dp(M1),
289 reduce(M,N,P,M2), dp(M2).
291 %%% reduce MReduce/CReduce
293 reduce(L,L,_,[[]]) :- !. %% true
294 reduce(N,_,N,[]) :- !. %% false
296 reduce([C|M],L,N,M1) :- !,
297 reduce(C,L,N,C1), %% evaluate clauses/matrices
298 (C1=[] -> M1=[[]] ; %% matrix/clause elimination
299 C1=[[]] -> reduce(M,L,N,M1) ; %% simplify
300 reduce(M,L,N,M2), %% evaluate remaining cl./mat.
301 (M2=[[]] -> M1=[[]] ; %% matrix/clause elimination
302 M2=[], C1=[M3] -> M1=M3 ; M1=[C1|M2] )).
307 selectLit([M|_],A,An) :- !, selectLit(M,A,An).
308 selectLit(-A,-A,A) :- !.
312 pure(M,M1) :- litM(M,LitM), pure(M,LitM,M1,LitM).
315 pure(M,[L|LitM],M1,LL) :-
317 (member(N,LL) -> M2=M ;
318 reduce(M,N,L,M2)), pure(M2,LitM,M1,LL).
321 litM([H|T],L) :- !, litM(H,L1), litM(T,L2), union(L1,L2,L).
324 % -----------------------------------------------------------------------------
325 % Code for computing conflict sets
327 conjunction([], true).
329 conjunction([X|L], (X,F)) :- conjunction(L, F).
333 instantiate((_,_), _, [], (,), true).
334 instantiate((_,_), _, [], (;), false).
335 instantiate((X,F), COMP, [C], O, FG) :-
336 copy_term((X,F), O, (C,I)),
338 instantiate((X,F), COMP, [C|Rest], O, AG) :-
339 copy_term((X,F),(C,I)),
341 instantiate((X,F), COMP, Rest, O, RG),
344 ground(~F, COMP, ~G) :- ground(F, COMP, G).
345 ground((F1 , F2), COMP, (G1 , G2)) :- ground(F1, COMP, G1), ground(F2, COMP, G2).
346 ground((F1 ; F2), COMP, (G1 ; G2)) :- ground(F1, COMP, G1), ground(F2, COMP, G2).
347 ground((F1 => F2), COMP, (G1 => G2)) :- ground(F1, COMP, G1), ground(F2, COMP, G2).
348 ground((F1 <=> F2), COMP, (G1 <=> G2)) :- ground(F1, COMP, G1), ground(F2, COMP, G2).
349 ground((all X:F), COMP, G) :- instantiate((X,F), COMP, COMP, (,), G).
350 ground((ex X:F), COMP, G) :- instantiate((X,F), COMP, COMP, (;), G).
354 % -----------------------------------------------------------------------------
355 % tp(+SD,+COMP, +OBS, +HS, -CS)
356 % - Determines a conflict set for the diagnostic problem
357 % (SD,COMP-HS,OBS). The term ~ab(c) is assumed for all
358 % elements of COMP-HS.
360 % SD: list of first-order formula, where variables are understood to quantify
361 % over elements in COMP
362 % COMP: set of all components
363 % OBS: set of (ground) facts
364 % HS: set of components assumed to be abnormal
366 % Example: tp([all X:(~ab(X) => p(X))], [c,d], [~p(c)], [], CS).
369 tp(SD, COMP, OBS, HS, CS) :-
370 subtract(COMP, HS, NormComp), % components assumed to be normal
371 maplist(normal, NormComp, S), % normal predicates
372 append3(SD, S, OBS, Theory), % construct theory
373 conjunction(Theory, F), % construct formula
374 ground(F, COMP, F2),!, % ground formula based on COMP
375 prove(~((F2))), % establish truth of negated formula
376 prove(~((F2)), Proof), % find proof (if true)
377 flatten(Proof,FlatProof), % extract elements of proof
378 include(copy_term(ab(_)),FlatProof,Abs),
379 maplist(arg(1), Abs, CompProof),% components in proof
380 list_to_set(CompProof, CompSorted), % remove repetitions
381 % if elements from HS occur in proof, ignore them
382 subtract(CompSorted, HS, CS),!.
384 % -----------------------------------------------------------------------------