tp.pl

   1 %% This file consists of three parts:
   2 %%      (1) Leancop 2.1
   3 %%      (2) ncDP: A Non-Clausal Form Decision Procedure
   4 %%      (3) A simple interface tp/4 that uses leancop and ncdp to compute
   5 %%          conflict sets
   6 %%
   7 %% This file is provided for your convenience, but you may as well
   8 %% use the original software.
   9 %%
  10 %% Leancop and ncDP are copyright Jens Otten (see www.leancop.de).
  11 %%
  12 %% For documentation of these tools, we refer to the webpage above.
  13 %%
  14
  15 :- op(1130, xfy, <=>). % equivalence
  16 :- op(1110, xfy, =>).  % implication
  17 %                      % disjunction (;)
  18 %                      % conjunction (,)
  19 :- op( 500, fy, ~).    % negation
  20 :- op( 500, fy, all).  % universal quantifier
  21 :- op( 500, fy, ex).   % existential quantifier
  22 :- op( 500,xfy, :).
  23
  24
  25 % ------------------------------------------------------------------
  26 %  make_matrix(+Fml,-Matrix,+Settings)
  27 %    -  transform first-order formula into set of clauses (matrix)
  28 %
  29 %  Fml, Matrix: first-order formula and matrix
  30 %
  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
  37 %
  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.
  42 %
  43 %  Example: make_matrix(ex Y:(all X:((p(Y) => p(X)))),Matrix,[]).
  44 %           Matrix = [[-(p(X1))], [p(1 ^ [X1])]]
  45
  46 make_matrix(Fml,Matrix,Set) :-
  47     univar(Fml,[],F1),
  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)
  51        ;
  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)
  55         ;
  56         def_nnf(F2,DNF,1,_,def)
  57     ),
  58     mat(DNF,M),
  59     ( member(reo(I),Set) -> mreorder(M,Matrix,I) ; Matrix=M ).
  60
  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
  65 %
  66 %  Example: def_nnf(ex Y:(all X:((p(Y) => p(X)))),DEF,def).
  67 %           DEF = ~ p(X1) ; p(1 ^ [X1])
  68
  69 def_nnf(Fml,DEF,I,I1,Set) :-
  70     def(Fml,[],NNF,DEF1,_,I,I1,Set), def(DEF1,NNF,DEF).
  71
  72 def([],Fml,Fml).
  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).
  75
  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));
  84       Fml = (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).
  89
  90 def((ex X:F),FreeV,NNF,DEF,Paths,I,I1,Set) :- !,
  91     def(F,[X|FreeV],NNF,DEF,Paths,I,I1,Set).
  92
  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).
  96
  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);
 102                         NNF = (NNF1;NNF2)).
 103
 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);
 115                         NNF = (NNF1,NNF2)).
 116
 117 def(Lit,_,Lit,[],1,I,I,_).
 118
 119 % ------------------------------------------------------------------
 120 %  dnf(+NNF,-DNF)  -  transform formula in NNF into formula in DNF
 121 %  NNF, DNF: formulae in NNF and DNF
 122 %
 123 %  Example: dnf(((p;~p),(q;~q)),DNF).
 124 %           DNF = (p, q ; p, ~ q) ; ~ p, q ; ~ p, ~ q
 125
 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).
 131 dnf(Lit,Lit).
 132
 133 % ------------------------------------------------------------------
 134 %  mat(+DNF,-Matrix)  -  transform formula in DNF into matrix
 135 %  DNF, Matrix: formula in DNF, matrix
 136 %
 137 %  Example: mat(((p, q ; p, ~ q) ; ~ p, q ; ~ p, ~ q),Matrix).
 138 %           Matrix = [[p, q], [p, -(q)], [-(p), q], [-(p), -(q)]]
 139
 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]]) :- !.
 143 mat(Lit,[[Lit]]).
 144
 145 % ------------------------------------------------------------------
 146 %  univar(+Fml,[],-Fml1)  -  rename variables
 147 %  Fml, Fml1: first-order formulae
 148 %
 149 %  Example: univar((all X:(p(X) => (ex X:p(X)))),[],F1).
 150 %           F1 = all Y : (p(Y) => ex Z : p(Z))
 151
 152 univar(X,_,X)  :- (atomic(X);var(X);X==[[]]), !.
 153 univar(F,Q,F1) :-
 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] ).
 157
 158 % ------------------------------------------------------------------
 159 %  union2/member2 - union and member for lists without unification
 160
 161 union2([],L,[L]).
 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).
 165
 166 member2(X,[Y|_]) :- X==Y, !.
 167 member2(X,[_|T]) :- member2(X,T).
 168
 169 % ------------------------------------------------------------------
 170 %  delete2 - delete variable from list
 171
 172 delete2([],_,[]).
 173 delete2([X|T],Y,T1) :- X==Y, !, delete2(T,Y,T1).
 174 delete2([X|T],Y,[X|T1]) :- delete2(T,Y,T1).
 175
 176 % ------------------------------------------------------------------
 177 %  mreorder - reorder clauses
 178
 179 mreorder(M,M,0) :- !.
 180 mreorder(M,M1,I) :-
 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,
 183     mreorder(M2,M1,I1).
 184
 185 mreorder2([],[],C,C).
 186 mreorder2([A|A1],[B|B1],[C|C1],[A,B,C|M1]) :- mreorder2(A1,B1,C1,M1).
 187
 188 :- dynamic(pathlim/0), dynamic(lit/4).
 189
 190
 191 %%% prove matrix M / formula F
 192
 193 prove(F,Proof) :- prove2(F,[cut,comp(7)],Proof).
 194
 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).
 199
 200 prove(PathLim,Set,Proof) :-
 201     \+member(scut,Set) -> prove([-(#)],[],PathLim,[],Set,[Proof]) ;
 202     lit(#,_,C,_) -> prove(C,[-(#)],PathLim,[],Set,Proof1),
 203     Proof=[C|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).
 208
 209 %%% leanCoP core prover
 210
 211 prove([],_,_,_,_,[]).
 212
 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=[]
 218          ;
 219          member(NegL,Path), unify_with_occurs_check(NegL,NegLit),
 220          Cla1=[], Proof1=[]
 221          ;
 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)
 227        ),
 228        ( member(cut,Set) -> ! ; true ),
 229        prove(Cla,Path,PathLim,[Lit|Lem],Set,Proof2).
 230
 231 %%% write clauses into Prolog's database
 232
 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).
 238
 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).
 243
 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).
 248
 249 append3(X,Y,Z,V) :-
 250         append(X,Y,L),
 251         append(L,Z,V).
 252
 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),
 257                             union(M1,M2,M3).
 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).
 261 bmatrix(X,0,[[X]]).
 262 bmatrix(X,1,[[-X]]).
 263
 264 sim([M],M) :- !. sim(M,[M]).
 265
 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):-!.
 268
 269 %%% prove
 270
 271 prove(F) :- bmatrix(F,0,M), pure(M,M1), dp(M1).
 272
 273 %%% dp (non-clausal DP)
 274
 275 dp([]) :- !, fail.
 276 dp(M)  :- member([],M), !.
 277
 278 % UNIT
 279 dp(M)  :- member([L],M), ( atom(L), N= -L ; -N=L ), !,
 280           reduce(M,N,L,M1), dp(M1).
 281
 282 % Beta-Splitting
 283 dp([[[C1|M],[C2|M2]|C]|M1])  :- !,
 284    dp([[[C1|M]]|M1]), dp([[[C2|M2]]|M1]), dp([C|M1]).
 285
 286 % Splitting
 287 dp(M)  :- selectLit(M,P,N),
 288           reduce(M,P,N,M1), dp(M1),
 289           reduce(M,N,P,M2), dp(M2).
 290
 291 %%% reduce MReduce/CReduce
 292
 293 reduce(L,L,_,[[]])   :- !.  %% true
 294 reduce(N,_,N,[])     :- !.  %% false
 295
 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] )).
 303
 304 reduce(A,_,_,A).
 305
 306 %% select literal
 307 selectLit([M|_],A,An) :- !, selectLit(M,A,An).
 308 selectLit(-A,-A,A)    :- !.
 309 selectLit(A,A,-A).
 310
 311 %%% PURE
 312 pure(M,M1) :- litM(M,LitM), pure(M,LitM,M1,LitM).
 313
 314 pure(M,[],M,_).
 315 pure(M,[L|LitM],M1,LL) :-
 316    (L= -N ; -L=N), !,
 317    (member(N,LL) -> M2=M ;
 318     reduce(M,N,L,M2)), pure(M2,LitM,M1,LL).
 319
 320 litM([],[])   :- !.
 321 litM([H|T],L) :- !, litM(H,L1), litM(T,L2), union(L1,L2,L).
 322 litM(A,[A]).
 323
 324 % -----------------------------------------------------------------------------
 325 % Code for computing conflict sets
 326
 327 conjunction([], true).
 328 conjunction([X], X).
 329 conjunction([X|L], (X,F)) :- conjunction(L, F).
 330
 331 normal(X, ~ab(X)).
 332
 333 instantiate((_,_), _, [], (,), true).
 334 instantiate((_,_), _, [], (;), false).
 335 instantiate((X,F), COMP, [C], O, FG) :-
 336         copy_term((X,F), O, (C,I)),
 337         ground(I, COMP, FG).
 338 instantiate((X,F), COMP, [C|Rest], O, AG) :-
 339         copy_term((X,F),(C,I)),
 340         ground(I, COMP, FG),
 341         instantiate((X,F), COMP, Rest, O, RG),
 342         AG =.. [O, FG, RG].
 343
 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).
 351 ground(Lit, _, Lit).
 352
 353
 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.
 359 %
 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
 365 %
 366 %  Example: tp([all X:(~ab(X) => p(X))], [c,d], [~p(c)], [], CS).
 367 %           CS = [c]
 368
 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),!.
 383
 384 % -----------------------------------------------------------------------------