World's most popular travel blog for travel bloggers.

# [Solved]: Abduction in ASP

, ,
Problem Detail:

Well, forgive my ignorance about the matter as I have been playing with ASP for the last couple of days.

Consider this simple example

``p. s :- p. ``

And the corresponding output generated after running the program in clingo:

``\$ ./clingo.exe  ex.lp --number=0 Answer: 1 p s SATISFIABLE  Models      : 1 ... ``

Where possible models are generated having `p true` and the formula `p -> s`.

But if I want to ask some query that requires abductive reasoning in order to generate some answers; in other words, I need to know the possible solutions to the fact `s true`. So the "supposed" example should be like the following:

``s. s :- p. ``

But unfortunately the answer does not contain `p` as expected.

``\$ ./clingo.exe  ex.lp --number=0 % warning: p/0 is never defined Answer: 1 s SATISFIABLE  Models      : 1 ... ``

Could that be done in any way in ASP?

I found out that this could not be done natively in ASP (or at least in the solvers that I am using). So the abduction theory needs to be modeled with the problem in order to derive expected results.

This is an example that demonstrates how it can be done. I haven't had the time to thoroughly test its efficiency but it works for some basic examples.

``% abduction.lp  %%%%%%%%%%%%% Preprocessing %%%%%%%%%%  % Remove tautological clauses  taut(C) :- pos(C,X), neg(C,X). preprocessed_clause(C) :- clause(C), not taut(C).  % which variable is in which clause  var_in_clause(C,X) :- preprocessed_clause(C), pos(C,X). var_in_clause(C,X) :- preprocessed_clause(C), neg(C,X).  %%%%%%%%%%%%% Guess a Candidate Solution %%%%%%%%%%  % S, a subset of hypotheses  is a solution iff (1) and (2) hold solution(S) :- hypothesis(S), not nosolution(S). nosolution(S) :- hypothesis(S), not solution(S).  %%%%%%%%%%%%% (1) background theory is consistent with S %%%%%%%%%%  % guess an assignment for all variables true_consistency(X) :- variable(X), not false_consistency(X). false_consistency(X) :- variable(X), not true_consistency(X).  %% Solution must be true true_consistency(S) :- solution(S).  %% Check for each clause in T whether it is satisfied sat(C) :- preprocessed_clause(C), pos(C,V), true_consistency(V). sat(C) :- preprocessed_clause(C), neg(C,V), false_consistency(V).  %% In case a clause is not satisfied, remove AS  notsat :- preprocessed_clause(C), not sat(C). :- notsat.   %%%%%%%%%%%%%% (2) background theory and solution entail the manifestation%%%%%%%%%%  %% Find assignment, which is a counter-example to entailment true_entail(X) | false_entail(X) :- variable(X).  % ordering over variables in preprocessed clauses lowerThan(C,X,Y) :- var_in_clause(C,X), var_in_clause(C,Y), X<Y. not_successor(C,X,Z) :- lowerThan(C,X,Y), lowerThan(C,Y,Z). successor(C,X,Y) :- lowerThan(C,X,Y), not not_successor(C,X,Y). not_infimum(C,X) :- lowerThan(C,Y,X). not_supremum(C,X) :- lowerThan(C,X,Y). infimum(C,X) :- not not_infimum(C,X), var_in_clause(C,X). supremum(C,X) :- not not_supremum(C,X), var_in_clause(C,X).  % check if unsat unsatupto(C,V) :- infimum(C,V), pos(C,V), false_entail(V). unsatupto(C,V) :- infimum(C,V), neg(C,V), true_entail(V). unsatupto(C,V) :- unsatupto(C,PreV), successor(C,PreV,V), pos(C,V), false_entail(V). unsatupto(C,V) :- unsatupto(C,PreV), successor(C,PreV,V), neg(C,V), true_entail(V).  unsat(C) :- unsatupto(C,V), supremum(C,V). unsat :- unsat(C).  % make sure that variables in manifestations and solution get the right truth value false_entail(X) :- manifestation(X). true_entail(X) :- solution(X).  % saturation true_entail(X) :- variable(X), unsat. false_entail(X) :- variable(X), unsat.  :- not unsat.  #show solution/1. %#show manifestation/1. %#show hypothesis/1. %#show variable/1. ``

And the example provided in this post's question:

``% a_ex2.lp  % Variables V variable("s";"p").  % Theory T over V clause(1). pos(1,"s"). neg(1,"p").  hypothesis("p").  manifestation("s"). ``

Output:

``\$ ./gringo.exe abduction.lp a_ex2.lp | ./claspD.exe --number 0 claspD version 1.1. Reading...done Answer: 1 solution("p")  Models      : 1 Time        : 0.002  (Parsing: 0.001) ``

Question Source : http://cs.stackexchange.com/questions/14592

3.2K people like this