Enlèvement en ASP

Question

Eh bien, pardonnez mon ignorance à ce sujet que je joue avec ASP pour la dernière quelques jours.

Considérez cet exemple simple

p.
s :- p.

Et la sortie correspondante générée après l'exécution du programme en Clingo:

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

Models      : 1
...

Lorsque des modèles possibles sont générés ayant p true et la formule p -> s.

Mais si je veux poser une question qui nécessite abduction afin de générer des réponses; autrement dit, je dois connaître les solutions possibles à la s true de fait. Ainsi, l'exemple « supposé » devrait être comme suit:

s.
s :- p.

Mais, malheureusement, la réponse ne contient pas p comme prévu.

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

Models      : 1
...

pourrait-il être fait en aucune façon en ASP?

Answer 1

Je trouve que cela ne pouvait être fait nativement en ASP (ou au moins dans les solveurs que j'utilise). Ainsi, les besoins de la théorie de l'enlèvement à modéliser le problème afin d'obtenir des résultats escomptés.

Ceci est un exemple qui montre comment il peut être fait. Je ne l'ai pas eu le temps de bien tester son efficacité, mais il fonctionne pour quelques exemples de base.

Source: http://www.dbai.tuwien.ac.at / proj / Arvis / # utilisation

% 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.

Et l'exemple fourni dans la question de ce message:

% a_ex2.lp

% Variables V
variable("s";"p").

% Theory T over V
clause(1).
pos(1,"s").
neg(1,"p").

hypothesis("p").

manifestation("s").

Sortie:

$ ./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)