5
$\begingroup$

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?

$\endgroup$
2
$\begingroup$

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.

Source: http://www.dbai.tuwien.ac.at/proj/arvis/#usage

% 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)
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.