=Paper=
{{Paper
|id=Vol-1433/tc_84
|storemode=property
|title=Unifying Justifications and Debugging for
Answer-Set Programs
|pdfUrl=https://ceur-ws.org/Vol-1433/tc_84.pdf
|volume=Vol-1433
|dblpUrl=https://dblp.org/rec/conf/iclp/DamasioMA15
}}
==Unifying Justifications and Debugging for
Answer-Set Programs==
https://ceur-ws.org/Vol-1433/tc_84.pdf
Technical Communications of ICLP 2015. Copyright with the Authors. 1
Unifying Justifications and Debugging for
Answer-Set Programs
Carlos Viegas Damásio (e-mail: cd@fct.unl.pt)
NOVA LINCS, Universidade Nova de Lisboa, Portugal
João Moura∗ (e-mail: joaomoura@yahoo.com)
NOVA LINCS, Universidade Nova de Lisboa, Portugal
Anastasia Analyti (analyti@ics.forth.gr)
Institute of Computer Science, FORTH-ICS, Crete, Greece
submitted 29 April 2015; accepted 5 June 2015
Abstract
Recently, (Viegas Damásio et al. 2013) introduced a way to construct propositional formu-
lae encoding provenance information for logic programs. From these formulae, justifications
for a given interpretation are extracted but it does not explain why such interpretation
is not an answer-set (debugging). Resorting to a meta-programming transformation for
debugging logic programs, (Gebser et al. 2008) does the converse.
Here we unify these complementary approaches using meta-programming transforma-
tions. First, an answer-set program is constructed in order to generate every provenance
propositional models for a program, both for well-founded and answer-set semantics, sug-
gesting alternative repairs to bring about (or not) a given interpretation. In particular, we
identify what changes must be made to a program in order for an interpretation to be an
answer-set, thus providing the basis to relate provenance with debugging.
With this meta-programming method, one does not have the need to generate the
provenance propositional formulas and thus obtain debugging and justification models
directly from the transformed program. This enables computing provenance answer-sets
in an easy way by using AS solvers. We show that the provenance approach generalizes
the debugging one, since any error has a counterpart provenance but not the other way
around. Because the method we propose is based on meta-programming, we extended an
existing tool and developed a proof-of-concept built to help computing our models.
1 Introduction and Background
Theoretical results leading to tools for debugging answer-set programs have in the
last few years been identified as a crucial prerequisite for a wider acceptance of
answer-set programming (ASP). Tracing approaches (Bsusoniu et al. 2013) expose
the user to the intricacies of reasoners (Brain et al. 2007) and declarative debugging
approaches based in meta-programming techniques have instead been developed.
But, one needs to understand why some interpretation is an answer-set (AS) –
∗ Under grant SFRH/BD/69006/2010 from Fundação para a Ciência e Tecnologia / Ministério
do Ensino e da Ciência.
2 C. V. Damásio and J. Moura and A. Analyti
justifications – while understanding why some other interpretation is not an AS
– debugging.
Example 1
Consider Π = {r1 : a ← b. r2 : a ← not b.}. Besides knowing a is true in the single
AS of Π, it is also be important to know that a is true because rules r1 and r2 are
in Π, independently of what we can conclude about b. Another possible justification
(among others) for a being true is that r2 is in Π and b has no support. Of course,
if one intends a to be false then there is a bug in Π, with one justification being
that rule r2 is unsatisfied.
In (Viegas Damásio et al. 2013), each literal can be associated with its why not
provenance (WnP), i.e. a logical propositional formula explaining why a literal is
true or false in an AS. In Example 1, formula W hy(a) = r1 ∧ ¬not(b) ∨ r2 ∧ not(b) ∨
¬not(a) is obtained for literal a and its negation for not a. Clearly, r1 ∧ r2 |=
W hy(a) is an intuitive justification for a. This provenance approach is capable
of providing the corrections (adding or removing facts, and removing rules, e.g.
not(a) ∧ not(b) ∧ ¬r2 |= ¬W hy(a) in Ex. 1) that are necessary in order to bring
about certain intended models.
Debugging ASP programs has been addressed in the literature by several au-
thors, and the most effective approaches resort to meta-transformations to detect
the diverse forms of anomalies in programs (Brain et al. 2007; Gebser et al. 2008;
Oetsch et al. 2010; Polleres et al. 2013). Being fine grained, these are designed to
pinpoint errors in LPs. Provenance formulas are inspired by a program transforma-
tion previously defined for declarative debugging of LPs (Pereira et al. 1993) and
have been conjectured to be related (Viegas Damásio et al. 2013) with debugging.
The most important contributions we make are (1) bridging the gap between
provenance models and LPs using meta-programming for ASP (2) unifying these
two complementary approaches by mapping provenance models with debugging
models (Gebser et al. 2008) (3) obtain justifications under the well-founded (WF)
and AS semantics without calculating WnP formulae for a LP.
Structure Overview – Next we review relevant LP formalisms followed by debugging
and provenance literature. In Section 2 we introduce a novel meta-programming
transformation both for WF and AS semantics that is used to obtain models for
WnP formulas of a given LP. We clarify which models are justifications, define
them in terms of AS existence for the meta-program and discuss computational
complexity. Section 3 provides a new mapping between our and the debugging
transformations, showing that provenance captures debugging models but not the
other way around. We end with a discussion, a comparison of these approaches with
others in the literature and possible future work.
1.1 Logic Programming Formalisms
Normal logic programs (NLP) are sets of rules r of the following form:
r : A1 ← A2 , . . . , Am , not Am+1 , . . . , not An .s.t., (n ≥ m ≥ 0)
Unifying Justifications and Debugging for Answer-Set Programs 3
where each Ai is a logical atom without function symbols. Let Head(r) = {A1 },
Body + (r) = {A2 , . . . , Am }, Body − (r) = {Am+1 , . . . , An }, and Body(r) = Body + (r)∪
not Body − (r). An (explicit) integrity constraint (IC) is a rule with the following
form: r : Head(r) ← Body(r), not Head(r). while its implicit form is r: ← Body(r).
A program is definite (or positive) if it has no negated atoms. A disjunctive logic
program (DLP) allows disjunction in the heads of rules. Without loss of generality,
we assume that programs are grounded, and Gr(Π) denotes the program obtained
from Π by instantiating variables with constants occurring in Π. The Herbrand
Base HΠ of a program Π is formed by the set of atoms occurring in it.
Given a set of literals J, let not J = {a | not a ∈ J} ∪ {not a | a ∈ J s.t., for
each b, a 6= not b}. A two-valued interpretation is a subset of HΠ specifying the
true atoms, and a partial interpretation is a subset of HΠ ∪ not HΠ (absent literals
are undefined).
A two-valued interpretation I corresponds to the partial interpretation I∪not (HΠ \
I). The least model least(Π) of a definite program Π is the least fixpoint of operator
TΠ (I) = {Head(r) | r ∈ Π ∧ Body(r) ⊆ I}, where I is a two-valued interpretation.
The answer-sets of NLP Π are fixpoints of Γ(I) = least(ΠI ), where ΠI =
{Head(r) ← Body + (r) | r ∈ Π, Body − (r) ∩ I = ∅}.
The well-founded model (WFM) of Π is T ∪ not F where T and F are inter-
pretations s.t., T ∩ F = ∅, T is the least fixpoint T = Γ(Γ(T )) = Γ2 (T ) and
F = HΠ \ Γ(T ).
1.2 Debugging
Debugging of LPs and in particular ASP has received important contributions over
the last years. e.g., (Eiter et al. 2010) provided two approaches for explaining
inconsistency, both of which characterize inconsistency in terms of bridge rules: by
pointing out rules which need to be altered for restoring consistency, and by finding
combinations of rules which cause inconsistency.
We are mostly interested in (Gebser et al. 2008) though, where a meta-programming
technique for debugging ASPs is presented. Debugging queries are expressed by
means of ASP programs, which allows restricting debugging information to rele-
vant parts. The main question addressed is: ”Why are interpretations expected to
be answer-sets, not answer-sets of a given ASP program?” Thus it finds seman-
tic errors in programs. The provided explanations are based on a scheme of errors
relying in a characterization of AS semantics by (Lee 2005; Ferraris et al. 2007).
However, these approaches do not answer the question of why a given (possibly
unintended) interpretation is indeed an AS. In Theorem 2 of (Gebser et al. 2008),
the four possible causes of errors dealt with by their debugging framework are:
Unsatisfied rules: If rule r ∈ Gr(Π), with nonempty Head(r), is unsatisfied by I, the
logical implication expressed by r is false under I, i.e. I |= Body(r) and Head(r) 6∈ I,
and thus I is not a classical model of Π.
Violated integrity constraints: If an IC c ∈ Gr(Π) is applicable under I, the fact that
Head(c) 6= ∅ implies I 6|= Body(c), and thus I cannot be an answer-set of Π.
Unsupported atoms: If {a} ⊆ I is unsupported with respect to I, no rule in Gr(Π)
allows for deriving a, and thus I is not a minimal model of ΠI .
4 C. V. Damásio and J. Moura and A. Analyti
Unfounded loops: If a loop Γ ⊆ I of Π is unfounded with respect to I, there is no
acyclic derivation for the atoms in Π, and thus I is not a minimal model of ΠI .
They construct a meta-program (Fig. 1.2) from a given program Π and interpre-
tation I that is capable of detecting the above errors via occurrences of the following
error-indicating meta-atoms in its answer-sets: unsatisf ied(lr ) indicates that a rule
r ∈ Gr(Π) is unsatisfied by I; violated(lc ) indicates that an IC c ∈ Gr(Π) is vio-
lated under I; unsupported(la ) indicates that an atom a ∈ I is unsupported; and
uf Loop(la ) indicates that an atom a belongs to some unfounded loop Γ ⊆ I of Π
with respect to I.
πint ={int(A)← atom(A), not int(A).
int(A)← atom(A), not int(A).}
πsat = {hasHead(R)← head(R, ).
someHInI(R)← head(R, A), int(A).
violated(C)← ap(C), not hasHead(C).hasHead(R),
unsatisf ied(R)← ap(R), not someHInI(R).}
πsupp ={unsupported(A)← int(A), not supported(A).
supported(A)← head(R, A), ap(R), not otherHInI(R, A).
otherHInI(R, A1)← head(R, A2), int(A2), head(R, A1), A1 6= A2.}
πnoas ={noAnswerSet← unsatisf ied( ). noAnswerSet ← violated( ).
noAnswerSet← unsupported( ). noAnswerSet ← uf Loop( ).
← not noAnswerSet.}
πap ={bl(R)← Body + (R, A), int((A). %blocked rules
bl(R)← Body − (R, A), int(A).}
ap(R)← rule(R), not bl(R). %applicable rules
πuf loop ={uf Loop(A)← int(A), supported(A), not uf loop(A).
uf loop(A)← int(A), not uf Loop(A).
someBInLoop(R)← Body + (R, A), uf Loop(A).
someHOutLoop(R)← head(R, A), uf loop((A).
dpcy(A1, A2)← dpcy(A1, A3), dpcy(A3, A2).
dpcy(A1, A2)← head(R, A1), Body + (R, A2), ap(R), uf Loop(A1), uf Loop(A2),
not someHOutLoop(R).
← head(R, A), uf Loop(A), ap(R), not someHOutLoop(R),
not someBInLoop(R).
← uf Loop(A1), uf Loop(A2), not dpcy(A1, A2).}
Fig. 1. Static Modules of Meta-Program D(Π).
In (Gebser et al. 2008), the authors define the input meta-program πin (Π) from
a ground DLP Π (note that we restrict our discussion to NLPs) as the follow-
ing set of facts: πin (Π) = {atom(la ) ← |a ∈ At(Π)}∪ {rule(lr ) ← | r ∈ Π}∪
{Head(lr , la ) ← | r ∈ Π, a ∈ Head(r)}∪ {Body + (lr , la ) ← | r ∈ Π, a ∈ Body + (r)}∪
{Body − (lr , la ) ← | r ∈ Π, a ∈ Body − (r)}. Program πin (Π) consists of facts stat-
ing which rules and atoms occur in Π and, for each rule r ∈ Π, which atoms are
contained in Head(r), Body + (r), and Body − (r), respectively. Given πin (Π), the
non-disjunctive meta-program D(Π) is defined as follows:
Let Π be a ground DLP. Then, the meta-program D(Π) for Π consists of πin (Π)
Unifying Justifications and Debugging for Answer-Set Programs 5
together with the modules of Fig. 1, i.e., D(Π) = πin (Π) ∪ πint ∪ πap ∪ πsat ∪ πsupp ∪
πuf loop ∪ πnoas .
Example 2
Consider program {r1 : a ← b, c. r2 : b ← d. r3 : b ← not e. f1 : c. f2 : d.}, for
which an intended AS is I = {b, c, d, e, f }. An explanation for I not being an AS
is that r1 is unsatisfied and e is unsupported. On the onther hand, (Gebser et al.
2008) cannot say why {a, b, c, d} is an AS because a is true due to d being true due
to e being false.
1.3 Provenance
In turn, (Viegas Damásio et al. 2013) presents a declarative logical approach to
extract WnP information for logic programs. Using values of a freely generated
Boolean algebra as annotation tags for atoms, they specify WnP for positive and
NLPs under WF semantics, and relate it to abduction and calculation of prime
implicants. The approach generalizes to ASP. These WnP formulae are used to
determine provenance of literals true in a given model, and are shown in (Vie-
gas Damásio et al. 2013) to extend the approaches of evidence graphs (Pemmasani
et al. 2004) and off-line justifications (Pontelli et al. 2009). In the remaining of this
section, assume that an LP Π over HΠ is given. Why not provenance is defined
in (Viegas Damásio et al. 2013) and summarized bellow:
Let BΠ be the free Boolean algebra generated by propositional variables HΠ ∪
not(HΠ ) ∪ {ri |1 ≤ i ≤ |Π|}, where for each rule of Π there is a unique and distinct
rule identifier ri . Elements of BΠ are the equivalence classes of propositional formu-
las under logical equivalence, and the partial ordering of BΠ is entailment: [φ] [ψ]
iff φ |= ψ. Thus BΠ is a lattice, with join and meet defined by [φ] ⊕ [ψ] = [φ ∨ ψ],
[φ] ⊗ [ψ] = [φ ∧ ψ], and let [φ] − [ψ] = [φ ∧ ¬ψ]. WnP is extracted with monotonic
multivalued programs and a WnP program P over HΠ is defined as:
Let a WnP program P be formed by rules of the form A ⇐ [J] ⊗ B1 ⊗ . . . ⊗ Bm
with m ≥ 0, and where [J] ∈ BΠ and A, B1 , . . . , Bm ∈ HΠ . An interpretation I
for P is a mapping I : HΠ → BΠ . The set of all interpretations is a lattice with
point-wise ordering. An interpretation I satisfies a rule A ⇐ [J] ⊗ B1 ⊗ . . . ⊗ Bm of
program P iff I(A) [J] ⊗ I(B1 ) ⊗ . . . ⊗ I(Bm ) iff J ∧ I(B1 ) ∧ . . . ∧ I(Bm ) |= I(A).
Interpretation I is a model of P iff I satisfies all the rules of P.
The monotonicity of P guarantees the existence of a least model MP for it, and by
mimicking the construction of a Gelfond-Lifschitz like operator, WnP for LPs under
WF semantics is defined. The rationale for P is: If a program P has some fact A
(resp. no fact for A), WnP formula for A is [(ri ∧ W hyi ) ∨ . . . ∨ (rj ∧ W hyj ) ∨ A]
(resp. [(ri ∧ W hyi ) ∨ . . . ∨ (rj ∧ W hyj ) ∨ ¬not(A)]). A justification for A is [A]
meaning there is a fact for A. Other justifications are obtained using a rule rk
and justifying why its body is true. The later case (denoted before by ’resp.’)
is better understood taking the justification for not A which has WnP formula
[¬(ri ∧ W hyi ) ∧ . . . ∧ ¬(rj ∧ W hyj ) ∧ not(A)], expressing that all bodies must be
falsified and [not(A)] holds.
6 C. V. Damásio and J. Moura and A. Analyti
Provenance program PI is constructed from Π and WnP interpretation I as
follows:
• For the ith rule A ← B1 , . . . , Bm , not C1 , . . . , not Cn (m + n ≥ 1) in Π add
provenance rule A ⇐ [ri ∧ ¬I(C1 ) ∧ . . . ¬I(Cn )] ⊗ B1 ⊗ . . . ⊗ Bm to PI ;
• ∀A ∈ HΠ , if A ∈ Π (resp. A ∈ / Π) add A ⇐ [A] (resp. A ⇐ [¬not(A)]) to PI .
Operator GΠ (I) = M P returns the least model of PI .
I
Operator GΠ is anti-monotonic, and therefore G2Π is monotonic having a least
model TΠ , corresponding to provenance information for what is true in the WFM,
while TUΠ = GΠ (TΠ ) contains the WnP of what is true or undefined in the WFM
of Π. The following definitions capturing Why-not provenance information
under the well-founded semantics are then provided:
Let TΠ be the least model of G2Π , TUΠ = GΠ (TΠ ), and A be an atom. Let
W hyΠ (A) = [TΠ (A)], W hyΠ (not A) = [¬TUΠ (A)], and W hyΠ (undef A) = [¬TΠ (A)∧
TUΠ (A)].
Theorem 1 (Provenance Models for WF Semantics (Viegas Damásio et al. 2013))
Let G ∈/ Π and F ∈ Π (resp. R ∈ Π) be sets of facts (resp. rules). Literal
L ∈ W F M ((Π\(F ∪R))∪G) iff there is a conjunction of literals C |= W hyΠ (L) s.t.,
RemoveF acts(C) ⊆ F, KeepF acts(C)∩F = ∅, RemoveRules(C) ⊆ R, KeepRules(C)∩
R = ∅, M issingF acts(C) ⊆ G, and N oF acts(C) ∩ G = ∅ where N oF acts(C) (resp.
M issingF acts(C) ) are facts that cannot (resp. must) be added:
KeepFacts(C) = {A. | A ∈ F } RemoveFacts(C) = {A. | ¬A ∈ F }
KeepRules(C) = {ri : A ← Body | ri ∈ R and ri ∈ Π}
RemoveRules(C) = {ri : A ← Body | ¬ri ∈ R and ri ∈ Π}
NoFacts(C) = {A. | not(A) ∈ G} MissingFacts(C) = {A. | ¬not(A) ∈ G}
Example 3 (From (Viegas Damásio et al. 2013))
Consider again program Π in Ex. 2. Its WnP information is:
W hy(a) = [r1 ∧ c ∧ ((r2 ∧ d) ∨ (r3 ∧ not(e)) ∨ ¬not(b)) ∨ ¬not(a)]
W hy(not a)= [not(a) ∧ (¬r1 ∨ ¬c ∨ (not(b) ∧ (¬r2 ∨ ¬d) ∧ (¬r3 ∨ ¬not(e)))]
W hy(b) = [(r2 ∧ d) ∨ (r3 ∧ not(e)) ∨ ¬not(b)]
W hy(not b)= [not(b) ∧ (¬r2 ∨ ¬d) ∧ (¬r3 ∨ ¬not(e))]
W hy(c) = [c] W hy(not c) = [¬c] W hy(d) = [d]
W hy(not d)= [¬d] W hy(e) = [¬not(e)] W hy(not e) = [not(e)]
The provenance for a being false, and all other atoms true is derived from the
models of W hy(not a) ∧ W hy(b) ∧ W hy(c) ∧ W hy(d) ∧ W hy(e) = not(a) ∧ ¬r1 ∧
(r2 ∨ ¬not(b)) ∧ c ∧ d ∧ ¬not(e), thus a fact for a must be absent, we have to remove
rule r1 , keep rule r2 or add fact b, keep facts c and d, and add fact e. (Gebser
et al. 2008) detects that rule r1 is unsatisfied and e is unsupported but it does not
determine provenance for a. One way to make a true is to simply add a fact for
it; alternatively r1 must be kept in Π as well as facts c and b. This is achieved by:
keeping r2 and d; keeping r3 and not adding e; adding b.
Unifying Justifications and Debugging for Answer-Set Programs 7
One obtains AS provenance from the WFM provence basically by forcing all atoms
to be either positive or negative, i.e., non-undefined, and using the provenance
determined for the WF semantics (see examples in Section 2).
Justifications are defined as: Given a logic program Π and a literal l, a justifi-
cation J for l in Π as an implicant of the why provenance formula W hyΠ (l) , i.e.
a conjunction of literals s.t., J |= W hyΠ (l). The implicant is prime if there is no
other implicant J 0 of W hyΠ (l) with less literals.
Note that it has been proved in (Viegas Damásio et al. 2013) that evidence
graphs (Pemmasani et al. 2004) and off-line justifications (Pontelli et al. 2009)
models can all be captured by WnP implicants, but some of our justifications cannot
be mapped by them. Also related to provenance are causal chains (Cabalar and
Fandiño 2013) where a multi-valued semantics for NLPs whose truth values form a
lattice of causal chains is provided. A causal chain is a concatenation of rule labels
reflecting some sequence of rule applications.
2 Contributions: Meta-Transformation for Provenance Formulae
We define here a novel program transformation, capable of obtaining all models
of WnP formulae, composed of two parts: (1) a set of common modules in Fig. 2,
shared by specific transformations for WF and AS semantics; (2) WF specific mod-
ules in Fig. 3. Its vocabulary is based in (Gebser et al. 2008) to ease their subsequent
combining. We only deal with the non-disjunctive case and ICs must be in their
explicit form.
πf act = {f act(X)← rule(R), head(R, X), not hasBody(R).
hasBody(R)← rule(R), bodyP (R, A).
hasBody(R)← rule(R), bodyN (R, A).}
πRules = {keepRule(X)← rule(X), not removeRule(X).
removeRule(X)← rule(X), not keepRule(X).}
πF acts = {missingF act(X)← atom(X), not f act(X), not noF act(X).
noF act(X)← atom(X), not f act(X), not missingF act(X).}
Fig. 2. Common Provenance Modules πcommon
Module πf act ∈ πcommon defines facts as rules in the program having empty
bodies. Module πf act assumes that module πin ∈ D(Π) (Fig. 1.2) will also be
applied, since it depends on all facts defined in πin . Modules πRules and πF acts
are the generators for propositional variables used in the provenance formulae in
the vocabulary of Theorem 1. Note that in πRules the provenance propositional
variables for facts HΠ are captured by keepRule/1 since, for generality purposes,
rule/1 represents both rule and fact identifiers.
8 C. V. Damásio and J. Moura and A. Analyti
πttu = { ←atom(A), t(A), not tu(A).
←head(R, H), not ap(R, t), not ap(R, tu), not undef (H), removeRule(R).
t(H) ←head(R, H), keepRule(R), ap(R, t), not undef (H).
t(H) ←atom(H), missingF act(H), not f act(H), not undef (H).
tu(H) ←head(R, H), keepRule(R), ap(R, tu).
tu(H) ←atom(H), missingF act(H), not f act(H).
tu(H) ←atom(H), undef (H).}
πapttu (Π) = {ap(ri , t)← t(B1 ), . . . t(Bm ), not tu(C1 ), . . . , not tu(Cn ).,
ap(ri , tu)← tu(B1 ), . . . tu(Bm ), not t(C1 ), . . . , not t(Cn ).
| A← B1 , . . . Bm , not C1 , . . . , not Cn ∈ Π and identified by ri .}
Fig. 3. Meta transformation πwf s modules
2.1 Provenance for the WF Semantics
A provenance program under the WF semantics is captured by πwf s combined
with debugging modules πcommon and πin . Module πttu encodes the Γ2 operator
for the program subject to changes defined by pairs keepRule/removeRule and
missingF act/noF act, where predicate t/1 represents what is true (the outer Γ),
and tu/1 what is true or undefined (the inner Γ). The constraint discards models
where assignments are contradictory, ensuring that t(A) ⇒ tu(A) for every atom
A. The module also uses an extra meta-predicate undef /1 that allows to make
an atom undefined, a new kind of change not captured by the original provenance
model for WF semantics that is included for the sake of completeness. Module
πapttu determines when a rule is applicable in the outer (ap(R, t)), and inner steps
(ap(R, tu)), and generalizes module πap of (Gebser et al. 2008).
Lemma 1
Given a logic program Π and a propositional model M of formula W hyΠ (L) for a
literal L, then there is an AS M 0 of W (Π) = πin (Π) ∪ πcommon ∪ πwf s (Π) s.t.:
• If A ∈ HΠ s.t., fact A ∈ Π and A ∈ M then keepRule(rA← ) ∈ M 0 and
removeRule(rA← ) 6∈ M 0
• If A ∈ HΠ s.t., fact A ∈ Π and A 6∈ M then keepRule(rA← ) 6∈ M 0 and
removeRule(rA← ) ∈ M 0
• If not(A) ∈ HΠ s.t., no fact A in Π and not(A) 6∈ M then missingF act(A) ∈
M 0 and noF act(A) 6∈ M 0
• If not(A) ∈ HΠ s.t., no fact A in Π and not(A) ∈ M then missingF act(A) 6∈
M 0 and noF act(A) ∈ M 0
• If ri ∈ M then keepRule(ri ) ∈ M 0 and removeRule(ri ) 6∈ M 0
• If ri 6∈ M then keepRule(ri ) 6∈ M 0 and removeRule(ri ) ∈ M 0
For the converse direction extra answer-sets of W (Π) may be generated. When
we fix the changes to Π all partial stable models (PSM) of the changed program
are obtained, i.e. all fixpoints of Γ2 , instead of solely the least fixpoint of Γ2 . These
models can be filtered out by guaranteeing minimality of the model. This is captured
in the following Lemmata:
Unifying Justifications and Debugging for Answer-Set Programs 9
Lemma 2
Let M 0 ∈ AS(W (Π) = πin (Π) ∪ πcommon ∪ πwf s (Π)) and M odel(M 0 ) = {A | t(A) ∈
M 0 } ∪ {not A | tu(A) 6∈ M 0 }. Construct program Π0 by deleting from Π every rule
identified by ri s.t., removeRule(ri ) ∈ M 0 , and adding a fact A in Π0 for every
missingF act(rA← ) ∈ M 0 . Then, M odel(M 0 ) is a PSM of Π0 . Conversely, if Π0 is
a program obtained deleting rules or adding facts, then every PSM of Π0 has a
corresponding AS in W (Π).
Lemma 3
Let M 0 be an AS of W (Π) = πin (Π) ∪ πcommon ∪ πwf s (Π), s.t., there is no AS M 00
of W (Π) with M odel(M 00 ) ( M odel(M 0 ). Let M be the model obtained from M 0
by reverting transformation in Lemma 1. Then, M is a model of W hyΠ (L) for each
L ∈ M 0.
Example 4
Recall now Ex. 2, to which we apply transformation W (Π) where πin (Π) = {head(r1 , a).
bodyP (r1 , b). bodyP (r1 , c). head(r2 , b). bodyP (r2 , d). head(r3 , b). bodyN (r3 , e). head(f1 , c).
head(f2 , d).}. W (Π) has 256 answer-sets corresponding to all possible changes to
Π by removing or keeping rules, and adding or not facts. Of these answer-sets,
6 correspond to a being false and all other atoms true, and are in exact corre-
spondence with the propositional models of formula not(a)∧ ¬r1 ∧ (r2 ∨ ¬not(b))∧
c ∧ d ∧ ¬not(e) obtained in Ex. 3. All answer-sets below contain1 {noF act(a),
removeRule(r1 ), keepRule(f1 ; f2 ), missingF act(e)}, corresponding to conjuncts
not(a), ¬r1 , c, d, ¬not(e) of the previous formula and are filtered for readability:
{keepRule(r2 ; r3 ), missingF act(b)}
{keepRule(r2 ; r3 ), noF act(b)}
{keepRule(r2 ), removeRule(r3 ), missingF act(b)}
{keepRule(r2 ), removeRule(r3 ), noF act(b)}
{removeRule(r2 ), keepRule(r3 ), missingF act(b)}
{removeRule(r2 ; r3 ), missingF act(b)}
There are 151 possible AS explaining why a is true, corresponding to the 151 models
of W hyΠ (a).
2.2 Provenance for the Answer-Set Semantics
Forbidding undefined atoms in the model and disallowing models where t/1 does not
occur when tu/1 occurs (Fig. 4), adapts the WF transformation presented before
to the AS semantics.
Theorem 2 follows from the above Lemmata 1, 2 and 3 for the WF semantics,
but first we need an auxiliary notion defining what is the WnP of an intended AS:
1 we denote a set of predicates {a(X), ..., a(Y )} as a(X; ...; Y )
10 C. V. Damásio and J. Moura and A. Analyti
πas (Π) = πcommon ∪ πwf s (Π) ∪ {← atom(A), tu(A), not t(A). ← atom(A), undef (A).}
Fig. 4. Meta-transformation πas
Definition 1 (Why not provenance for an interpretation)
Let Π be a logic program and I an interpretation. The AS WnP for I is:
^ ^ ^
I
AnsW hyΠ = AnsW hyΠ (A) AnsW hyΠ (not A) {¬r|A ∈ Head(r)}
∀A∈I ∀A6∈I ∀A6∈I
Intuitively, the WnP for an interpretation I is the intersection of the WnP for
its positive (and negative) atoms. We then select WnP formulae containing ¬r for
every r ∈ Π s.t., an atom A ∈ / I belongs to Head(r) which effectively avoids con-
sidering rules giving support to unintended atoms, and thus providing unnecessary
justifications. This forms a restricted class, containing interesting WnP formulas,
for which the following applies:
Theorem 2 (WnP models for the AS semantics)
Given a logic program Π, and an interpretation I, then the answer-sets of trans-
formed program S(Π) = πin (Π) ∪ πas (Π) s.t., M odel(M ) = I are in 1:1 correspon-
I
dence with the models of AnsW hyΠ .
These models are complete in the sense they provide all possible justifications for
an AS or all explanations for why an interpretation is not a model. These can then
be minimized according to whatever criteria one might have, e.g., subset minimality,
minimal changes to the program, disallowing or preferring certain repair operations
over others etc., which can be captured by optimization constraints supported by
the major ASP solvers.
Consider now again the program in Example 2: {a ← c, not b. b ← not a. d ←
not c, not d. c ← not e. e ← f. f ← e.}. This program has answer-sets A1 : {a, c}
and A2 : {b, c}. Below are some of the 144 WnP models for A1 from which we
select the ones presenting intuitive explanations (model selection is clarified next)
from all of which the following literals are omitted: F = {keepRule(r2; r3; r5; r6),
noF act(b; d; e; f ), t(a; c)}: (1) {removeRule(r1), keepRule(r4), missingF act(a; c)}
(2) {removeRule(r1; r4), missingF act(a; c)} (3) {removeRule(r1), keepRule(r4),
missingF act(a), noF act(c)} (4) {keepRule(r1), removeRule(r4), noF act(a), missingF act(c)}
(5) {keepRule(r1; r4), missingF act(a; c)} (6) {keepRule(r1; r4), noF act(a), missingF act(c)}
(7) {keepRule(r1; r4), missingF act(a), noF act(c)} (8) {keepRule(r1), removeRule(r4),
missingF act(a; c)} (9) {keepRule(r1; r4), noF act(a; c)}
3 Contributions: Mapping Provenance with Debugging
As shown before, our meta-transformation produces a model for each WnP model
and some can be aligned with debugging models calculated by (Gebser et al. 2008).
These approaches complement each other: we produce provenance models for exist-
ing answer-sets, while the debugging approach is capable of obtaining more specific
Unifying Justifications and Debugging for Answer-Set Programs 11
results regarding the non-existence of answer-sets, namely in the presence of un-
founded loops. So, we need to impose equivalence between predicates int/1 and t/1
(see Fig. 5) and thus introduce of module πmap . The resulting models consist of
two parts, one stating what is the problem with the interpretation at hand (corre-
sponding to the debugging part) and the other offering a justification for why this
interpretation is a model of the program (corresponding to the provenance part).
πt−int = { ← atom(A), int(A), not t(A).
← atom(A), int(A), t(A).}
πics = { ← rule(R), violated(R), keepRule(R).}
πprune = { ← rule(R), removeRule(R), not ap(R).
← atom(A), missingF act(A), supported(A), not uf Loop(A).
← atom(A), noF act(A), supported(A), uf Loop(A).}
Fig. 5. Transformation πmap = πt−int ∪ πics ∪ πprune
Module πt−int ensures that atoms int and t are mapped which effectively maps
provenance and debugging at the interpretation level, while πics guarantees that
violated ICs are corrected by removing them. The combined program is J(Π) =
πint ∪ πsat ∪ πsupp ∪ πuf Loop ∪ πas (Π) ∪ πmap ∪ D0 (Π), where in order to determine
provenance for a given AS, D0 (Π) is obtained from D(Π) by substituting πap with
πapttu and removing πnoas .
Intuitively, an interpretation is guessed (represented by int/1), and one then
forces the correspondence of t/1 with int/1. The repaired program (removing
rules or adding missing facts) is guessed, and generates the extension of t/1, and it
is always possible to trivially repair a program and obtain any desired interpretation
by removing all rules and adding all missing facts. We now look at error-indicating
predicates to detect problems with Π.
Theorem 3
Let M be an AS of D(Π). Then, there is an AS M 0 of meta-program J(Π) s.t.,
M \ ({noAnswerSet} ∪ {ap(ri ), bl(ri ) | ri is a rule identifier}) ⊆ M 0 .
So, we are able to detect every error pointed out by error-indicating predicates
of (Gebser et al. 2008). There is however a subtle difference: we prune debugging
answer-sets which are not supported by the repaired program. Their exact relation-
ship is captured next:
Theorem 4 (Mapping)
Let M 0 be an answer-set of J(Π). Then,
• If unsatisf ied(ri ) or violated(ri ) ∈ M 0 then removeRule(ri ) ∈ M 0 ;
• If unsupported(ri ) ∈ M 0 then missingF act(ri ) ∈ M 0 ;
• If uf Loop(a1 ..an ) ∈ M 0 then ∃i ∈ [1, . . . , n] s.t., missingF act(ai ) ∈ M 0 . Also,
∃M 00 ∈ AS(J(Π)) s.t. uf Loop(a1 ..an ) ∪ missingF act(a1 ..an ) ∈ M 00 .
12 C. V. Damásio and J. Moura and A. Analyti
However, some provenance answer-sets may be considered redundant (even though
correct) but module πprune in Fig. 5 can be used to prune them. It disallows re-
moving blocked rules (bl/1), adding facts which are not in unfounded loops but are
already supported, and forces a missingF act to be added to every atom in detected
unfounded loops.
Example 5
Take again Ex. 1 in (Viegas Damásio et al. 2013) and include relevant modules
of transformation D. We show next a sample of its answer-sets, having F =
{keepRule(r1; r2; r3; r4; r6), unsupported(a; b), missingF act(a; b), noF act(c; e)}
in common.
F ∪ {removeRule(r5), unsupported(d; f ), unsatisf ied(r5), missingF act(d; f )}
F ∪ {removeRule(r5), unsatisf ied(r5), supported(c; e), noF act(d), unsupported(f ),
missingF act(f )}
F ∪ {keepRule(r5), supported(c), unsupported(d), missingF act(d), noF act(f )}
F ∪ {keepRule(r5), supported(c), noF act(d; f )}
4 Conclusions and Future Work
We provide a transformation to compute WnP models under the WF and AS
semantics by computing the answer-sets of meta-programs that capture the original
programs and include some necessary extra atoms. We do this in a modular way,
preserving compatibility with the previous work of (Viegas Damásio et al. 2013)
and computing the models directly without first obtaining the provenance formulas
for certain interpretations. This enables computing provenance answer-sets in an
easy way by using AS solvers. Having this, we align provenance and debugging
answer-sets in a unified transformation and show that the provenance approach
generalizes the debugging one, since any error has a counterpart provenance but not
the other way around. Since the proposed method is based on meta-programming,
we extended an existing tool (Gebser et al. 2007) and developed a proof-of-concept
(http://cptkirk.sourceforge.net) built solely to allow computing our models.
Our mapping allows generating answer-sets capturing errors and justifications for
(intended) models. As expected, they are exponential. One direction to explore is to
obtain prime implicant by optimizing these models using reification and then subset
inclusion preference ordering (Gebser et al. 2007; Gebser et al. 2011) via a saturation
technique (Eiter and Gottlob 1995). Note that deciding if an AS is optimal for a DLP
is a Πp2 -complete problem. Alternative offline justifications (Pontelli et al. 2009)
(which are also exponential) can be extracted from models of J(Π) by adding extra
constraints to the transformed program guaranteeing: only one rule is kept for true
atoms (providing support); literals assumed false have all rules removed (which are
undefined in the WFM); false literals have to keep all their rules; the dependency
graph is acyclic; The major difference to Pontelli’s approach is that we provide
justifications for the full model from which we may obtain their justifications, but
our approach subsumes it since we are capable of findng more justifications as well
as errors in the program.
Unifying Justifications and Debugging for Answer-Set Programs 13
References
Brain, M., Gebser, M., Pührer, J., Schaub, T., Tompits, H., and Woltran, S.
2007. Debugging asp programs by means of asp. In LPNMR 2007 (2007-06-06),
C. Baral, G. Brewka, and J. S. Schlipf, Eds. Lecture Notes in Computer Science, vol.
4483. Springer, 31–43.
Bsusoniu, P.-A., Oetsch, J., Pührer, J., Skočovsky, P., and Tompits, H. 2013.
Sealion: An eclipse-based ide for answer-set programming with advanced debugging
support. Theory and Practice of Logic Programming 13, 657–673.
Cabalar, P. and Fandiño, J. 2013. An algebra of causal chains. In Logic Programming
and Nonmonotonic Reasoning, P. Cabalar and T. Son, Eds. Lecture Notes in Computer
Science, vol. 8148. Springer Berlin Heidelberg, 530–542.
Eiter, T., Fink, M., Schüller, P., and Weinzierl, A. 2010. Finding explanations of
inconsistency in multi-context systems. KR 10, 329–339.
Eiter, T. and Gottlob, G. 1995. On the computational cost of disjunctive logic pro-
gramming: Propositional case.
Ferraris, P., Lee, J., and Lifschitz, V. 2007. A new perspective on stable models. In
Proceedings of the 20th international joint conference on Artifical intelligence. IJCAI’07.
Morgan Kaufmann Publishers Inc., San Francisco, CA, USA, 372–379.
Gebser, M., Kaminski, R., and Schaub, T. 2011. Complex optimization in answer set
programming. Theory and Practice of Logic Programming 11, 821–839.
Gebser, M., Kaufmann, B., Neumann, A., and Schaub, T. 2007. clasp: A conflict-
driven answer set solver. In Logic Programming and Nonmonotonic Reasoning. Springer
Berlin Heidelberg, 260–265.
Gebser, M., Puehrer, J., Schaub, T., and Tompits, H. 2008. A meta-programming
technique for debugging answer-set programs. In AAAI-08/IAAI-08 Proceedings, D. Fox
and C. P. Gomes, Eds. 448–453.
Gebser, M., Pührer, J., Schaub, T., Tompits, H., and Woltran, S. 2007. spock:
A Debugging Support Tool for Logic Programs under the Answer-Set Semantics. In
Proceedings of the 21st Workshop on (Constraint) Logic Programming, (WLP’07),
Würzburg, Germany, D. Seipel, M. Hanus, A. Wolf, and J. Baumeister, Eds. Technical
Report 434, Bayerische Julius-Maximilians-Universität Würzburg, Institut für Infor-
matik, 258–261.
Lee, J. 2005. A model-theoretic counterpart of loop formulas. In Proceedings of Inter-
national Joint Conference on Artificial Intelligence (IJCAI). Professional Book Center,
503–508.
Oetsch, J., Pührer, J., and Tompits, H. 2010. Catching the ouroboros: On debugging
non-ground answer-set programs. Theory Pract. Log. Program. 10, 4-6 (July), 513–529.
Pemmasani, G., Guo, H.-F., Dong, Y., Ramakrishnan, C., and Ramakrishnan, I.
2004. Online justification for tabled logic programs. In Functional and Logic Program-
ming, Y. Kameyama and P. Stuckey, Eds. Lecture Notes in Computer Science, vol. 2998.
Springer Berlin Heidelberg, 24–38.
Pereira, L. M., Damásio, C. V., and Alferes, J. J. 1993. Diagnosis and debugging
as contradiction removal. In Proceedings of the 2nd International Workshop on Logic
Programming and Non-monotonic Reasoning. MIT Press, 316–330.
Polleres, A., Frhstck, M., Schenner, G., and Friedrich, G. 2013. Debugging
non-ground asp programs with choice rules, cardinality and weight constraints. In Logic
Programming and Nonmonotonic Reasoning, P. Cabalar and T. Son, Eds. Lecture Notes
in Computer Science, vol. 8148. Springer Berlin Heidelberg, 452–464.
14 C. V. Damásio and J. Moura and A. Analyti
Pontelli, E., Son, T. C., and El-Khatib, O. 2009. Justifications for logic programs
under answer set semantics. TPLP 9, 1, 1–56.
Viegas Damásio, C., Analyti, A., and Antoniou, G. 2013. Justifications for logic pro-
gramming. In Logic Programming and Nonmonotonic Reasoning, P. Cabalar and T. C.
Son, Eds. Lecture Notes in Computer Science, vol. 8148. Springer Berlin Heidelberg,
530–542.