Entführung in ASP

Question

Verzeihen Sie meine Unwissenheit über die Angelegenheit, wie ich damit gespielt habe ASP In den letzten Tagen.

Betrachten Sie dieses einfache Beispiel

p.
s :- p.

Und die entsprechende Ausgabe erzeugt nach dem Ausführen des Programms in Clingo:

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

Models      : 1
...

Wo möglich Modelle erzeugt werden p true und die Formel p -> s.

Aber wenn ich eine Abfrage fragen möchte, die abduktives Denken erfordert, um einige Antworten zu generieren; Mit anderen Worten, ich muss die möglichen Lösungen für die Tatsache kennen s true. Das "angebliche" Beispiel sollte also wie folgt sein:

s.
s :- p.

Aber leider enthält die Antwort nicht p wie erwartet.

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

Models      : 1
...

Könnte das in ASP in irgendeiner Weise getan werden?

Answer 1

Ich fand heraus, dass dies nicht in ASP (oder zumindest in den von mir verwendeten Löser) nativ erfolgen konnte. Daher muss die Entduktionstheorie mit dem Problem modelliert werden, um die erwarteten Ergebnisse abzuleiten.

Dies ist ein Beispiel, das zeigt, wie es getan werden kann. Ich hatte nicht die Zeit, seine Effizienz gründlich zu testen, aber es funktioniert für einige grundlegende Beispiele.

Quelle: 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.

Und das Beispiel in der Frage dieses Beitrags:

% a_ex2.lp

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

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

hypothesis("p").

manifestation("s").

Ausgabe:

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