From: Mart Lubbers Date: Tue, 7 Oct 2014 08:39:30 +0000 (+0200) Subject: first initial commit X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=913bd0d328f5cd89ac355bf9b993ceeb528e16ce;p=ker1415-1.git first initial commit --- 913bd0d328f5cd89ac355bf9b993ceeb528e16ce diff --git a/20142015-ker-practical1.pdf b/20142015-ker-practical1.pdf new file mode 100644 index 0000000..c5fcf21 Binary files /dev/null and b/20142015-ker-practical1.pdf differ diff --git a/diagnosis.pl b/diagnosis.pl new file mode 100644 index 0000000..aa00d89 --- /dev/null +++ b/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/domain-template.pl b/domain-template.pl new file mode 100644 index 0000000..be21c73 --- /dev/null +++ b/domain-template.pl @@ -0,0 +1,48 @@ +% ------------------------- Domain Definition ------------------------- +% This file describes a planning domain: a set of predicates and +% fluents that describe the state of the system, a set of actions and +% the axioms related to them. More than one problem can use the same +% domain definition, and therefore include this file + + +% --- Cross-file definitions ------------------------------------------ +% marks the predicates whose definition is spread across two or more +% files +% +% :- multifile name/#, name/#, name/#, ... + + + + + +% --- Primitive control actions --------------------------------------- +% this section defines the name and the number of parameters of the +% actions available to the planner +% +% primitive_action( dosomething(_,_) ). % underscore means `anything' + + + + + +% --- Precondition for primitive actions ------------------------------ +% describe when an action can be carried out, in a generic situation S +% +% poss( doSomething(...), S ) :- preconditions(..., S). + + + + + +% --- Successor state axioms ------------------------------------------ +% describe the value of fluent based on the previous situation and the +% action chosen for the plan. +% +% fluent(..., result(A,S)) :- positive; previous-state, not(negative) + + + + + +% --------------------------------------------------------------------- +% --------------------------------------------------------------------- diff --git a/instance-template.pl b/instance-template.pl new file mode 100644 index 0000000..1fe27b6 --- /dev/null +++ b/instance-template.pl @@ -0,0 +1,31 @@ +% ------------------------- Problem Instance -------------------------- +% This file is a template for a problem instance: the definition of an +% initial state and of a goal. + +% debug(on). % need additional debug information at runtime? + + + +% --- Load domain definitions from an external file ------------------- + +:- [domain-template]. % Replace with the domain for this problem + + + + +% --- Definition of the initial state --------------------------------- + + + + + + +% --- Goal condition that the planner will try to reach --------------- + +goal(S) :- % fill in the goal definition + + + + +% --------------------------------------------------------------------- +% --------------------------------------------------------------------- diff --git a/planner.pl b/planner.pl new file mode 100644 index 0000000..b162f7c --- /dev/null +++ b/planner.pl @@ -0,0 +1,103 @@ +% -------------= Simple planner for situation calculus =--------------- +% +% Executes an iterative deepening search, by default limited to a depth +% of 15 levels +% +% plan. will search for a plan of maximum length +% plan(M). will search for a plan of maximum length up to M +% plan(N,M). will search for a plan of mimimum length N and maximum +% length M +% +% +% Checklist for the definition of a domain and problem: +% +% - initial state initialize fluents in s0 +% +% - possibility axioms poss( (...), S ) :- +% +% - successor-state axioms ( ..., result(A,S) ) :- +% ; % or +% , % and +% not(). +% +% - goal predicate goal(S) :- +% + +% --------------------------= High Level =----------------------------- + +% default number of iterations (15) +plan :- plan(0, 15). + +% given max number of iterations +plan(MaxDepth) :- plan(0, MaxDepth). + +% given min and max number of iterations +plan(MinDepth, MaxDepth) :- + M is MaxDepth+1, write('Trying plans of length: '), + plan(Plan, MinDepth, M), nl, nl, writePlan(Plan). + + + +% same as above, to be called from shell; include additional output +% messages and halt to quit pl +planner :- planner(0, 15). +planner(MaxDepth) :- planner(0, MaxDepth). +planner(MinDepth, MaxDepth) :- + nl, plan(MinDepth, MaxDepth), nl, halt; + write('\n\nNo plan has been found!'), nl, nl, halt. + + + +% ---------------------------= Low Level =----------------------------- + +% start from depth N, up to M + +plan(P, N, M) :- + N < M, + debugoutput(write('\n\nPlans of length ')), + writef('%w %f',[N]), + seqplan(P, N, s0), !. + +plan(P, N, M) :- N < M, O is N+1, plan(P, O, M). + +seqplan( [], N, S ) :- N = 0, debugoutput(writeSituation(S)), goal(S). +seqplan( [A|L], N, S) :- N > 0, M is N-1, result(A,S,S1), seqplan(L, M, S1). + +result(E,S,result(E,S)) :- primitive_action(E), poss(E,S). + +% -----------------------= Support Function =-------------------------- + +% debugoutput will be printed only if debug(on) is defined in the KB +:- dynamic debug/1. +:- multifile debug/1. + +debug(off). +debugoutput(A) :- debug(on), A, !; true. + + +% prints a situation as a sequence of actions, starting from s0 +writeSituation(s0) :- write('\n s0'). +writeSituation(result(A,S)) :- writeSituation(S), writef(" > %w", [A]). + +% prints a plan as a list of actions, numbered + +writePlan(List) :- + debugoutput(write('\nA plan has been found:\n\n')), + writePlan(List,1). + +writePlan([],_) :- + nl. + +writePlan([Action|List], Counter) :- + writef('%3R %w\n',[Counter,Action]), + Next is Counter+1, + writePlan(List,Next). + + +% hides some (unimportant) warnings from the pl interpreter +:- style_check([-discontiguous, -singleton]). + + + +% --------------------------------------------------------------------- +% --------------------------------------------------------------------- diff --git a/sample-blocks-domain.pl b/sample-blocks-domain.pl new file mode 100644 index 0000000..e58f174 --- /dev/null +++ b/sample-blocks-domain.pl @@ -0,0 +1,61 @@ +% -------------------- Sample of a planning domain -------------------- + + +% the following line specifies which predicates or fluents are defined +% across two or more files. These predicates appear here, and in the +% initial state and goal definitions, in sample-blocks.pl + +:- multifile on/3, clear/2. % / + + + + +% -- Primitive control actions: this section defines the name and +% the number of parameters of the actions available to the planner + +primitive_action( move(_,_) ). % underscore means `anything' + + + + +% -- Preconditions for primitive actions: describe when an action +% can be carried out, in a generic situation S + +poss( move(What, Where), S ) :- % implication poss() <= precond + clear(What, S), + clear(Where, S), + not(heavy(What)), % can't move the table (or other heavy obj) + not(What = Where), % can't move a block on top of itself + not(on(What, Where, S)). % can't move around the same support + % (applies for the table) + + + +% -- Successor State Axioms for primitive fluents: describe the value +% of fluent based on the previous situation and the action chosen for +% the plan. + +% The general form of a successor state axiom is: +% +% a fluent is true in the situation resulting from applying action A +% in situation S, if +% - action A makes the fluent true; OR +% - the fluent was already true in the previous situation S, +% AND action A will not change this fact, by making it false. + + +on(Block, Support, result(A, S)) :- + A = move(Block, Support); + on(Block, Support, S), not(A = move(Block, _)). + + +clear(table, _). % special case, the table is clear any situation + % (i.e. there is always space on the table) + +clear(Block, result(A, S)) :- + A = move(Something, _), on(Something, Block, S); + not(A = move(_, Block)), clear(Block, S). + + +% --------------------------------------------------------------------- +% --------------------------------------------------------------------- diff --git a/sample-blocks.pl b/sample-blocks.pl new file mode 100644 index 0000000..6942aee --- /dev/null +++ b/sample-blocks.pl @@ -0,0 +1,40 @@ +% ------------------- Sample of a planning problem -------------------- + + +% define the following predicate to print out extended information +% about the planning process at runtime. Will produce A LOT of text +% after the first 4-5 iterations, since it shows all the plans +% considered by the program! + +debug(on). + + + +% -- Include domain definitions from sample-blocks-domain.pl + +:- ['sample-blocks-domain']. + + + + +% -- Define the initial state: the necessary set of eternal predicates +% and fluents that describe the situation at the beginning of the run + +heavy(table). % cannot be moved + +clear(blockA, s0). % the only block with nothing on top + +on(blockC, table, s0). +on(blockB, blockC, s0). +on(blockA, blockB, s0). + + + + +% -- Last, the goal condition that the planner will try to reach + +goal(S) :- on(blockB, table, S). + + +% --------------------------------------------------------------------- +% --------------------------------------------------------------------- diff --git a/tp.pl b/tp.pl new file mode 100644 index 0000000..34069df --- /dev/null +++ b/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),!. + +% -----------------------------------------------------------------------------