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.