Похищение в Asp

Question

Ну, прости мое невежество по этому поводу, так как я играл Аспирант За последние пару дней.

Рассмотрим этот простой пример

p.
s :- p.

И соответствующий вывод, сгенерированный после запуска программы в Clingo:

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

Models      : 1
...

Где генерируются модели p true и формула p -> s.

Но если я хочу спросить какой -то запрос, который требует абсуктивных рассуждений, чтобы генерировать некоторые ответы; Другими словами, мне нужно знать возможные решения о факте s true. Анкет Таким образом, «предполагаемый» пример должен быть похож на следующее:

s.
s :- p.

Но, к сожалению, ответ не содержит p как и ожидалось.

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

Models      : 1
...

Можно ли это сделать в любом случае в ASP?

Answer 1

Я узнал, что это нельзя было сделать изначально в ASP (или, по крайней мере, в решателях, которые я использую). Таким образом, теория похищения должна быть смоделирована с проблемой, чтобы получить ожидаемые результаты.

Это пример, который демонстрирует, как это можно сделать. У меня не было времени, чтобы тщательно проверить его эффективность, но она работает для некоторых основных примеров.

Источник: 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.

И пример, приведенный в вопросе этого поста:

% a_ex2.lp

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

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

hypothesis("p").

manifestation("s").

Выход:

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