From 075f1824931cf28f3a7173846a427343b54faabc Mon Sep 17 00:00:00 2001 From: Caspar Safarlou Date: Wed, 12 Nov 2014 10:12:14 +0100 Subject: [PATCH] add second assigment prolog source files --- report/src/diagnosis.pl | 57 ++++++ report/src/tp.pl | 384 ++++++++++++++++++++++++++++++++++++++++ 2 files changed, 441 insertions(+) create mode 100644 report/src/diagnosis.pl create mode 100644 report/src/tp.pl diff --git a/report/src/diagnosis.pl b/report/src/diagnosis.pl new file mode 100644 index 0000000..aa00d89 --- /dev/null +++ b/report/src/diagnosis.pl @@ -0,0 +1,57 @@ +:- [tp]. + +% Definition of logical gates, used in the examples below. +and_gate(all X:(and(X) , ~ab(X) => (in1(X), in2(X) <=> out(X)))). +or_gate( all X:(or(X) , ~ab(X) => (in1(X) ; in2(X) <=> out(X)))). +xor_gate(all X:(xor(X) , ~ab(X) => (out(X) <=> in1(X),~in2(X);~in1(X),in2(X)))). + +% Two unconnected AND gates with two inputs. It is observed that the +% inputs are true and the outputs are false. +problem1(SD, COMP, OBS) :- + and_gate(AND), + SD = [ AND, and(a1), and(a2) ], + COMP = [a1, a2], + OBS = [in1(a1), in2(a1), ~out(a1), in1(a2), in2(a2), ~out(a2)]. + +% Example of wwo AND gates where the output of the first gate (a1) is +% connected to the first input (in1) of the second gate (a2). It is +% easy to see that the observations are inconsistent with the +% specification. +problem2(SD, COMP, OBS) :- + and_gate(AND), + SD = [ AND, and(a1), and(a2), out(a1) <=> in1(a2) ], + COMP = [a1, a2], + OBS = [in1(a1), ~in2(a1), out(a2)]. + +% Another wiring example, now with two AND gates and an OR gate. +problem3(SD, COMP, OBS) :- + and_gate(AND), or_gate(OR), + SD = [ AND, OR, and(a1), and(a2), or(o1), + out(a1) <=> in1(o1), out(a2) <=> in2(o1)], + COMP = [a1, a2, o1], + OBS = [in1(a1), in2(a1), in1(a2), in2(a2), ~out(o1)]. + +% The following represents a (one-bit) full adder: a +% circuit that can be used for the addition of two bits with +% carry-in and carry-out bits. +% +% in1(fa), in2(fa): input bits +% carryin(fa): carry-in bit +% out(fa): output bit +% carryout(fa): carry-out bit +% +% returns the sum of in1(fa) + in2(fa) + carryin(fa) +% as 2 * carryout(fa) + out(fa) (i.e., as 2 bits) +fulladder(SD, COMP, OBS) :- + and_gate(AND), or_gate(OR), xor_gate(XOR), + SD = [AND, OR, XOR, + and(a1), and(a2), xor(x1), xor(x2), or(r1), + in1(fa) <=> in1(x1), in2(fa) <=> in1(a1), + carryin(fa) <=> in1(a2), carryin(fa) <=> in2(x2), + out(fa) <=> out(x2), carryout(fa) <=> out(r1), + in2(fa) <=> in2(x1), in2(fa) <=> in2(a1), + out(x1) <=> in2(a2), out(x1) <=> in1(x2), + out(a2) <=> in1(r1), out(a1) <=> in2(r1) ], + COMP = [a1, a2, x1, x2, r1], + OBS = [in1(fa), ~in2(fa), carryin(fa), out(fa), ~carryout(fa)]. %1+1=1? + diff --git a/report/src/tp.pl b/report/src/tp.pl new file mode 100644 index 0000000..34069df --- /dev/null +++ b/report/src/tp.pl @@ -0,0 +1,384 @@ +%% This file consists of three parts: +%% (1) Leancop 2.1 +%% (2) ncDP: A Non-Clausal Form Decision Procedure +%% (3) A simple interface tp/4 that uses leancop and ncdp to compute +%% conflict sets +%% +%% This file is provided for your convenience, but you may as well +%% use the original software. +%% +%% Leancop and ncDP are copyright Jens Otten (see www.leancop.de). +%% +%% For documentation of these tools, we refer to the webpage above. +%% + +:- op(1130, xfy, <=>). % equivalence +:- op(1110, xfy, =>). % implication +% % disjunction (;) +% % conjunction (,) +:- op( 500, fy, ~). % negation +:- op( 500, fy, all). % universal quantifier +:- op( 500, fy, ex). % existential quantifier +:- op( 500,xfy, :). + + +% ------------------------------------------------------------------ +% make_matrix(+Fml,-Matrix,+Settings) +% - transform first-order formula into set of clauses (matrix) +% +% Fml, Matrix: first-order formula and matrix +% +% Settings: list of settings, which can contain def, nodef and conj; +% if it contains nodef/def, no definitional transformation +% or a complete definitional transformation is done, +% otherwise a definitional transformation is done for +% the conjecture and the standard transformation is done +% for the axioms; conjecture is marked if conj is given +% +% Syntax of Fml: negation '~', disjunction ';', conjunction ',', +% implication '=>', equivalence '<=>', universal/existential +% quantifier 'all X:'/'ex X:' where 'X' is a +% Prolog variable, and atomic formulae are Prolog atoms. +% +% Example: make_matrix(ex Y:(all X:((p(Y) => p(X)))),Matrix,[]). +% Matrix = [[-(p(X1))], [p(1 ^ [X1])]] + +make_matrix(Fml,Matrix,Set) :- + univar(Fml,[],F1), + ( member(conj,Set), F1=(A=>C) -> F2=((A,#)=>(#,C)) ; F2=F1 ), + ( member(nodef,Set) -> + def_nnf(F2,NNF,1,_,nnf), dnf(NNF,DNF) + ; + \+member(def,Set), F2=(B=>D) -> + def_nnf(~(B),NNF,1,I,nnf), dnf(NNF,DNF1), + def_nnf(D,DNF2,I,_,def), DNF=(DNF2;DNF1) + ; + def_nnf(F2,DNF,1,_,def) + ), + mat(DNF,M), + ( member(reo(I),Set) -> mreorder(M,Matrix,I) ; Matrix=M ). + +% ------------------------------------------------------------------ +% def_nnf(+Fml,-DEF) - transform formula into a definitional +% Skolemized negation normal form (DEF) +% Fml, DEF: first-order formula and formula in DEF +% +% Example: def_nnf(ex Y:(all X:((p(Y) => p(X)))),DEF,def). +% DEF = ~ p(X1) ; p(1 ^ [X1]) + +def_nnf(Fml,DEF,I,I1,Set) :- + def(Fml,[],NNF,DEF1,_,I,I1,Set), def(DEF1,NNF,DEF). + +def([],Fml,Fml). +def([(A,(B;C))|DefL],DEF,Fml) :- !, def([(A,B),(A,C)|DefL],DEF,Fml). +def([A|DefL],DEF,Fml) :- def(DefL,(A;DEF),Fml). + +def(Fml,FreeV,NNF,DEF,Paths,I,I1,Set) :- + ( Fml = ~(~A) -> Fml1 = A; + Fml = ~(all X:F) -> Fml1 = (ex X: ~F); + Fml = ~(ex X:F) -> Fml1 = (all X: ~F); + Fml = ~((A ; B)) -> Fml1 = ((~A , ~B)); + Fml = ~((A , B)) -> Fml1 = (~A ; ~B); + Fml = (A => B) -> Fml1 = (~A ; B); + Fml = ~((A => B))-> Fml1 = ((A , ~B)); + Fml = (A <=> B) -> + ( Set=def -> Fml1 = ((A => B) , (B => A)); + Fml1 = ((A , B) ; (~A , ~B)) ); + Fml = ~((A<=>B)) -> Fml1 = ((A , ~B) ; (~A , B)) ), !, + def(Fml1,FreeV,NNF,DEF,Paths,I,I1,Set). + +def((ex X:F),FreeV,NNF,DEF,Paths,I,I1,Set) :- !, + def(F,[X|FreeV],NNF,DEF,Paths,I,I1,Set). + +def((all X:Fml),FreeV,NNF,DEF,Paths,I,I1,Set) :- !, + copy_term((X,Fml,FreeV),((I^FreeV),Fml1,FreeV)), I2 is I+1, + def(Fml1,FreeV,NNF,DEF,Paths,I2,I1,Set). + +def((A ; B),FreeV,NNF,DEF,Paths,I,I1,Set) :- !, + def(A,FreeV,NNF1,DEF1,Paths1,I,I2,Set), + def(B,FreeV,NNF2,DEF2,Paths2,I2,I1,Set), + append(DEF1,DEF2,DEF), Paths is Paths1 * Paths2, + (Paths1 > Paths2 -> NNF = (NNF2;NNF1); + NNF = (NNF1;NNF2)). + +def((A , B),FreeV,NNF,DEF,Paths,I,I1,Set) :- !, + def(A,FreeV,NNF3,DEF3,Paths1,I,I2,Set), + ( NNF3=(_;_), Set=def -> append([(~I2^FreeV,NNF3)],DEF3,DEF1), + NNF1=I2^FreeV, I3 is I2+1 ; + DEF1=DEF3, NNF1=NNF3, I3 is I2 ), + def(B,FreeV,NNF4,DEF4,Paths2,I3,I4,Set), + ( NNF4=(_;_), Set=def -> append([(~I4^FreeV,NNF4)],DEF4,DEF2), + NNF2=I4^FreeV, I1 is I4+1 ; + DEF2=DEF4, NNF2=NNF4, I1 is I4 ), + append(DEF1,DEF2,DEF), Paths is Paths1 + Paths2, + (Paths1 > Paths2 -> NNF = (NNF2,NNF1); + NNF = (NNF1,NNF2)). + +def(Lit,_,Lit,[],1,I,I,_). + +% ------------------------------------------------------------------ +% dnf(+NNF,-DNF) - transform formula in NNF into formula in DNF +% NNF, DNF: formulae in NNF and DNF +% +% Example: dnf(((p;~p),(q;~q)),DNF). +% DNF = (p, q ; p, ~ q) ; ~ p, q ; ~ p, ~ q + +dnf(((A;B),C),(F1;F2)) :- !, dnf((A,C),F1), dnf((B,C),F2). +dnf((A,(B;C)),(F1;F2)) :- !, dnf((A,B),F1), dnf((A,C),F2). +dnf((A,B),F) :- !, dnf(A,A1), dnf(B,B1), + ( (A1=(C;D);B1=(C;D)) -> dnf((A1,B1),F) ; F=(A1,B1) ). +dnf((A;B),(A1;B1)) :- !, dnf(A,A1), dnf(B,B1). +dnf(Lit,Lit). + +% ------------------------------------------------------------------ +% mat(+DNF,-Matrix) - transform formula in DNF into matrix +% DNF, Matrix: formula in DNF, matrix +% +% Example: mat(((p, q ; p, ~ q) ; ~ p, q ; ~ p, ~ q),Matrix). +% Matrix = [[p, q], [p, -(q)], [-(p), q], [-(p), -(q)]] + +mat((A;B),M) :- !, mat(A,MA), mat(B,MB), append(MA,MB,M). +mat((A,B),M) :- !, (mat(A,[CA]),mat(B,[CB]) -> union2(CA,CB,M);M=[]). +mat(~Lit,[[-Lit]]) :- !. +mat(Lit,[[Lit]]). + +% ------------------------------------------------------------------ +% univar(+Fml,[],-Fml1) - rename variables +% Fml, Fml1: first-order formulae +% +% Example: univar((all X:(p(X) => (ex X:p(X)))),[],F1). +% F1 = all Y : (p(Y) => ex Z : p(Z)) + +univar(X,_,X) :- (atomic(X);var(X);X==[[]]), !. +univar(F,Q,F1) :- + F=..[A,B|T], ( (A=ex;A=all) -> B=(X:C), delete2(Q,X,Q1), + copy_term((X,C,Q1),(Y,D,Q1)), univar(D,[Y|Q],D1), F1=..[A,Y:D1] ; + univar(B,Q,B1), univar(T,Q,T1), F1=..[A,B1|T1] ). + +% ------------------------------------------------------------------ +% union2/member2 - union and member for lists without unification + +union2([],L,[L]). +union2([X|L1],L2,M) :- member2(X,L2), !, union2(L1,L2,M). +union2([X|_],L2,M) :- (-Xn=X;-X=Xn) -> member2(Xn,L2), !, M=[]. +union2([X|L1],L2,M) :- union2(L1,[X|L2],M). + +member2(X,[Y|_]) :- X==Y, !. +member2(X,[_|T]) :- member2(X,T). + +% ------------------------------------------------------------------ +% delete2 - delete variable from list + +delete2([],_,[]). +delete2([X|T],Y,T1) :- X==Y, !, delete2(T,Y,T1). +delete2([X|T],Y,[X|T1]) :- delete2(T,Y,T1). + +% ------------------------------------------------------------------ +% mreorder - reorder clauses + +mreorder(M,M,0) :- !. +mreorder(M,M1,I) :- + length(M,L), K is L//3, append(A,D,M), length(A,K), + append(B,C,D), length(C,K), mreorder2(C,A,B,M2), I1 is I-1, + mreorder(M2,M1,I1). + +mreorder2([],[],C,C). +mreorder2([A|A1],[B|B1],[C|C1],[A,B,C|M1]) :- mreorder2(A1,B1,C1,M1). + +:- dynamic(pathlim/0), dynamic(lit/4). + + +%%% prove matrix M / formula F + +prove(F,Proof) :- prove2(F,[cut,comp(7)],Proof). + +prove2(F,Set,Proof) :- + (F=[_|_] -> M=F ; make_matrix(F,M,Set)), + retractall(lit(_,_,_,_)), (member([-(#)],M) -> S=conj ; S=pos), + assert_clauses(M,S), prove(1,Set,Proof). + +prove(PathLim,Set,Proof) :- + \+member(scut,Set) -> prove([-(#)],[],PathLim,[],Set,[Proof]) ; + lit(#,_,C,_) -> prove(C,[-(#)],PathLim,[],Set,Proof1), + Proof=[C|Proof1]. +prove(PathLim,Set,Proof) :- + member(comp(Limit),Set), PathLim=Limit -> prove(1,[],Proof) ; + (member(comp(_),Set);retract(pathlim)) -> + PathLim1 is PathLim+1, prove(PathLim1,Set,Proof). + +%%% leanCoP core prover + +prove([],_,_,_,_,[]). + +prove([Lit|Cla],Path,PathLim,Lem,Set,Proof) :- + Proof=[[[NegLit|Cla1]|Proof1]|Proof2], + \+ (member(LitC,[Lit|Cla]), member(LitP,Path), LitC==LitP), + (-NegLit=Lit;-Lit=NegLit) -> + ( member(LitL,Lem), Lit==LitL, Cla1=[], Proof1=[] + ; + member(NegL,Path), unify_with_occurs_check(NegL,NegLit), + Cla1=[], Proof1=[] + ; + lit(NegLit,NegL,Cla1,Grnd1), + unify_with_occurs_check(NegL,NegLit), + ( Grnd1=g -> true ; length(Path,K), K true ; + \+ pathlim -> assert(pathlim), fail ), + prove(Cla1,[Lit|Path],PathLim,Lem,Set,Proof1) + ), + ( member(cut,Set) -> ! ; true ), + prove(Cla,Path,PathLim,[Lit|Lem],Set,Proof2). + +%%% write clauses into Prolog's database + +assert_clauses([],_). +assert_clauses([C|M],Set) :- + (Set\=conj, \+member(-_,C) -> C1=[#|C] ; C1=C), + (ground(C) -> G=g ; G=n), assert_clauses2(C1,[],G), + assert_clauses(M,Set). + +assert_clauses2([],_,_). +assert_clauses2([L|C],C1,G) :- + assert_renvar([L],[L2]), append(C1,C,C2), append(C1,[L],C3), + assert(lit(L2,L,C2,G)), assert_clauses2(C,C3,G). + +assert_renvar([],[]). +assert_renvar([F|FunL],[F1|FunL1]) :- + ( var(F) -> true ; F=..[Fu|Arg], assert_renvar(Arg,Arg1), + F1=..[Fu|Arg1] ), assert_renvar(FunL,FunL1). + +append3(X,Y,Z,V) :- + append(X,Y,L), + append(L,Z,V). + +bmatrix((~X),Pol,M) :- !, Pol1 is (1-Pol), bmatrix(X,Pol1,M). +bmatrix((X1<=>X2),Pol,M) :- !, bmatrix(((X1=>X2),(X2=>X1)),Pol,M). +bmatrix(X,Pol,M3) :- X=..[F,X1,X2], alpha(F,Pol,Pol1,Pol2), !, + bmatrix(X1,Pol1,M1), bmatrix(X2,Pol2,M2), + union(M1,M2,M3). +bmatrix(X,Pol,[M3]) :- X=..[F,X1,X2], beta(F,Pol,Pol1,Pol2), !, + bmatrix(X1,Pol1,M1), bmatrix(X2,Pol2,M2), + sim(M1,M4), sim(M2,M5), union(M4,M5,M3). +bmatrix(X,0,[[X]]). +bmatrix(X,1,[[-X]]). + +sim([M],M) :- !. sim(M,[M]). + +alpha(',',1,1,1):-!. alpha(';',0,0,0):-!. alpha((=>),0,1,0):-!. +beta(',',0,0,0):-!. beta(';',1,1,1):-!. beta((=>),1,0,1):-!. + +%%% prove + +prove(F) :- bmatrix(F,0,M), pure(M,M1), dp(M1). + +%%% dp (non-clausal DP) + +dp([]) :- !, fail. +dp(M) :- member([],M), !. + +% UNIT +dp(M) :- member([L],M), ( atom(L), N= -L ; -N=L ), !, + reduce(M,N,L,M1), dp(M1). + +% Beta-Splitting +dp([[[C1|M],[C2|M2]|C]|M1]) :- !, + dp([[[C1|M]]|M1]), dp([[[C2|M2]]|M1]), dp([C|M1]). + +% Splitting +dp(M) :- selectLit(M,P,N), + reduce(M,P,N,M1), dp(M1), + reduce(M,N,P,M2), dp(M2). + +%%% reduce MReduce/CReduce + +reduce(L,L,_,[[]]) :- !. %% true +reduce(N,_,N,[]) :- !. %% false + +reduce([C|M],L,N,M1) :- !, + reduce(C,L,N,C1), %% evaluate clauses/matrices + (C1=[] -> M1=[[]] ; %% matrix/clause elimination + C1=[[]] -> reduce(M,L,N,M1) ; %% simplify + reduce(M,L,N,M2), %% evaluate remaining cl./mat. + (M2=[[]] -> M1=[[]] ; %% matrix/clause elimination + M2=[], C1=[M3] -> M1=M3 ; M1=[C1|M2] )). + +reduce(A,_,_,A). + +%% select literal +selectLit([M|_],A,An) :- !, selectLit(M,A,An). +selectLit(-A,-A,A) :- !. +selectLit(A,A,-A). + +%%% PURE +pure(M,M1) :- litM(M,LitM), pure(M,LitM,M1,LitM). + +pure(M,[],M,_). +pure(M,[L|LitM],M1,LL) :- + (L= -N ; -L=N), !, + (member(N,LL) -> M2=M ; + reduce(M,N,L,M2)), pure(M2,LitM,M1,LL). + +litM([],[]) :- !. +litM([H|T],L) :- !, litM(H,L1), litM(T,L2), union(L1,L2,L). +litM(A,[A]). + +% ----------------------------------------------------------------------------- +% Code for computing conflict sets + +conjunction([], true). +conjunction([X], X). +conjunction([X|L], (X,F)) :- conjunction(L, F). + +normal(X, ~ab(X)). + +instantiate((_,_), _, [], (,), true). +instantiate((_,_), _, [], (;), false). +instantiate((X,F), COMP, [C], O, FG) :- + copy_term((X,F), O, (C,I)), + ground(I, COMP, FG). +instantiate((X,F), COMP, [C|Rest], O, AG) :- + copy_term((X,F),(C,I)), + ground(I, COMP, FG), + instantiate((X,F), COMP, Rest, O, RG), + AG =.. [O, FG, RG]. + +ground(~F, COMP, ~G) :- ground(F, COMP, G). +ground((F1 , F2), COMP, (G1 , G2)) :- ground(F1, COMP, G1), ground(F2, COMP, G2). +ground((F1 ; F2), COMP, (G1 ; G2)) :- ground(F1, COMP, G1), ground(F2, COMP, G2). +ground((F1 => F2), COMP, (G1 => G2)) :- ground(F1, COMP, G1), ground(F2, COMP, G2). +ground((F1 <=> F2), COMP, (G1 <=> G2)) :- ground(F1, COMP, G1), ground(F2, COMP, G2). +ground((all X:F), COMP, G) :- instantiate((X,F), COMP, COMP, (,), G). +ground((ex X:F), COMP, G) :- instantiate((X,F), COMP, COMP, (;), G). +ground(Lit, _, Lit). + + +% ----------------------------------------------------------------------------- +% tp(+SD,+COMP, +OBS, +HS, -CS) +% - Determines a conflict set for the diagnostic problem +% (SD,COMP-HS,OBS). The term ~ab(c) is assumed for all +% elements of COMP-HS. +% +% SD: list of first-order formula, where variables are understood to quantify +% over elements in COMP +% COMP: set of all components +% OBS: set of (ground) facts +% HS: set of components assumed to be abnormal +% +% Example: tp([all X:(~ab(X) => p(X))], [c,d], [~p(c)], [], CS). +% CS = [c] + +tp(SD, COMP, OBS, HS, CS) :- + subtract(COMP, HS, NormComp), % components assumed to be normal + maplist(normal, NormComp, S), % normal predicates + append3(SD, S, OBS, Theory), % construct theory + conjunction(Theory, F), % construct formula + ground(F, COMP, F2),!, % ground formula based on COMP + prove(~((F2))), % establish truth of negated formula + prove(~((F2)), Proof), % find proof (if true) + flatten(Proof,FlatProof), % extract elements of proof + include(copy_term(ab(_)),FlatProof,Abs), + maplist(arg(1), Abs, CompProof),% components in proof + list_to_set(CompProof, CompSorted), % remove repetitions + % if elements from HS occur in proof, ignore them + subtract(CompSorted, HS, CS),!. + +% ----------------------------------------------------------------------------- -- 2.20.1