first initial commit
authorMart Lubbers <mart@martlubbers.net>
Tue, 7 Oct 2014 08:39:30 +0000 (10:39 +0200)
committerMart Lubbers <mart@martlubbers.net>
Tue, 7 Oct 2014 08:39:30 +0000 (10:39 +0200)
20142015-ker-practical1.pdf [new file with mode: 0644]
diagnosis.pl [new file with mode: 0644]
domain-template.pl [new file with mode: 0644]
instance-template.pl [new file with mode: 0644]
planner.pl [new file with mode: 0644]
sample-blocks-domain.pl [new file with mode: 0644]
sample-blocks.pl [new file with mode: 0644]
tp.pl [new file with mode: 0644]

diff --git a/20142015-ker-practical1.pdf b/20142015-ker-practical1.pdf
new file mode 100644 (file)
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 (file)
index 0000000..aa00d89
--- /dev/null
@@ -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 (file)
index 0000000..be21c73
--- /dev/null
@@ -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 (file)
index 0000000..1fe27b6
--- /dev/null
@@ -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 (file)
index 0000000..b162f7c
--- /dev/null
@@ -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( <action>(...), S ) :- <precond>
+%
+% - successor-state axioms             <fluent>( ..., result(A,S) ) :-
+%                                                                      <some events made it true>;     % or
+%                                                                      <it was true all along>,        % and
+%                                                                      not(<some events made it false>).
+%
+% - goal predicate                             goal(S) :- <goal conditions>
+%
+
+% --------------------------= 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 (file)
index 0000000..e58f174
--- /dev/null
@@ -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.            % <name>/<number of parameters>
+
+
+
+
+% -- 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 (file)
index 0000000..6942aee
--- /dev/null
@@ -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 (file)
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:<Formula>'/'ex X:<Formula>' 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<PathLim -> 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),!.
+
+% -----------------------------------------------------------------------------