Unifying Justi cations and Debugging for Answer-Set Programs

Abstract

Recently, (Viegas Damasio et al. 2013) introduced a way to construct propositional formulae encoding provenance information for logic programs. From these formulae, justi cations 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 transformations. 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, suggesting 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 justi cation 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 identi ed 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) { justi cations { while understanding why some other interpretation is not an AS { debugging.

Example 1

Consider = fr1 : a b: r2 : a not b:g. 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 justi cation (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 justi cation being that rule r2 is unsatis ed.

In (Viegas Damasio 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 j= W hy(a) is an intuitive justi cation 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 j= :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 authors, and the most e ective 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 ne grained, these are designed to pinpoint errors in LPs. Provenance formulas are inspired by a program transformation previously de ned for declarative debugging of LPs (Pereira et al. 1993) and have been conjectured to be related (Viegas Damasio 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 justi cations 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 justi cations, de ne 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 where each Ai is a logical atom without function symbols. Let Head(r) = fA1g, Body+(r) = fA2; : : : ; Amg, Body (r) = fAm+1; : : : ; Ang, 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 de nite (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 = fa j not a 2 J g [ fnot a j a 2 J s.t., for each b, a 6= not bg. 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 unde ned).

A two-valued interpretation I corresponds to the partial interpretation I[not (H n I). The least model least( ) of a de nite program is the least xpoint of operator T (I) = fHead(r) j r 2 ^ Body(r) Ig, where I is a two-valued interpretation.

The answer-sets of NLP are xpoints of (I) = least( I ), where I = fHead(r) Body+(r) j r 2 ; Body (r) \ I = ;g.

The well-founded model (WFM) of is T [ not F where T and F are interpretations s.t., T \ F = ;, T is the least xpoint T = ( (T )) = 2(T ) and F = H n (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 nding 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 relevant parts. The main question addressed is: "Why are interpretations expected to be answer-sets, not answer-sets of a given ASP program?" Thus it nds semantic 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: Unsatis ed rules: If rule r 2 Gr( ), with nonempty Head(r), is unsatis ed by I, the logical implication expressed by r is false under I, i.e. I j= Body(r) and Head(r) 62 I, and thus I is not a classical model of .

Violated integrity constraints: If an IC c 2 Gr( ) is applicable under I, the fact that

Head(c) 6= ; implies I 6j= Body(c), and thus I cannot be an answer-set of . Unsupported atoms: If fag 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 . Unfounded loops: If a loop I of acyclic derivation for the atoms in

is unfounded with respect to I, there is no , and thus I is not a minimal model of I .

They construct a meta-program (Fig. 1.2) from a given program and interpretation 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 uf Loop(la) indicates that an atom a belongs to some unfounded loop r 2 Gr( ) is unsatis ed by I; violated(lc) indicates that an IC c 2 Gr( ) is violated under I; unsupported(la) indicates that an atom a 2 I is unsupported; and I of with respect to I.

int =fint(A) int(A) atom(A); not int(A): atom(A); not int(A):g sat = fhasHead(R) someHInI(R)

violated(C) unsatisf ied(R) head(R; ): head(R; A); int(A): ap(C); not hasHead(C):hasHead(R); ap(R); not someHInI(R):g supp =funsupported(A)

supported(A) otherHInI(R; A1) noas =fnoAnswerSet noAnswerSet ap =fbl(R) bl(R) ap(R) ufloop =fuf Loop(A)

uf loop(A) someBInLoop(R) someHOutLoop(R) dpcy(A1; A2) dpcy(A1; A2) int(A); not supported(A): head(R; A); ap(R); not otherHInI(R; A): head(R; A2); int(A2); head(R; A1); A1 6= A2:g unsatisf ied( ): unsupported( ): not noAnswerSet:g Body+(R; A); int((A): Body (R; A); int(A):g rule(R); not bl(R): noAnswerSet noAnswerSet violated( ): uf Loop( ): %blocked rules %applicable rules int(A); supported(A); not uf loop(A): int(A); not uf Loop(A): Body+(R; A); uf Loop(A): head(R; A); uf loop((A): dpcy(A1; A3); dpcy(A3; 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):g

In (Gebser et al. 2008) , the authors de ne the input meta-program in( ) from (note that we restrict our discussion to NLPs) as the followj r 2

; a 2 Head(r)g[ fBody+(lr; la) in( ) = fatom(la) ja 2 At( )g[ frule(lr) fBody (lr; la) j r 2 ing which rules and atoms occur in ; a 2 Body (r)g. Program

in( and, for each rule r 2 contained in Head(r), Body+(r), and Body (r), respectively. Given in( ), the non-disjunctive meta-program D( ) is de ned as follows:

Let be a ground DLP. Then, the meta-program D( ) for consists of in( ) j r 2 ) consists of facts stat

j r 2 g[ ; a 2 Body+(r)g[ , which atoms are together with the modules of Fig. 1, i.e., D( ) = in( ) [ int [ ap [ sat [ supp [

Example 2

Consider program fr1 : a b; c: r2 : b d: r3 : b not e: f1 : c: f2 : d:g, for which an intended AS is I = fb; c; d; e; f g. An explanation for I not being an AS is that r1 is unsatis ed and e is unsupported. On the onther hand, (Gebser et al. 2008) cannot say why fa; b; c; dg is an AS because a is true due to d being true due to e being false.

1.3 Provenance

In turn, (Viegas Damasio 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 (Viegas Damasio et al. 2013) to extend the approaches of evidence graphs (Pemmasani et al. 2004) and o -line justi cations (Pontelli et al. 2009) . In the remaining of this section, assume that an LP over H is given. Why not provenance is de ned in (Viegas Damasio et al. 2013) and summarized bellow:

Let B be the free Boolean algebra generated by propositional variables H [ not(H ) [ frij1 i j jg, where for each rule of there is a unique and distinct rule identi er ri. Elements of B are the equivalence classes of propositional formulas under logical equivalence, and the partial ordering of B is entailment: [ ] [ ] i j= . Thus B is a lattice, with join and meet de ned by [ ] [ ] = [ _ ], [ ] [ ] = [ ^ ], and let [ ] [ ] = [ ^ : ]. WnP is extracted with monotonic multivalued programs and a WnP program P over H is de ned as:

Let a WnP program P be formed by rules of the form A ( [J ] B1 : : : Bm with m 0, and where [J ] 2 B and A; B1; : : : ; Bm 2 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 satis es a rule A ( [J ] B1 : : : Bm of program P i I(A) [J ] I(B1) : : : I(Bm) i J ^ I(B1) ^ : : : ^ I(Bm) j= I(A). Interpretation I is a model of P i I satis es 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 de ned. 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 justi cation for A is [A] meaning there is a fact for A. Other justi cations 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 justi cation for not A which has WnP formula [:(ri ^ W hyi) ^ : : : ^ :(rj ^ W hyj ) ^ not(A)], expressing that all bodies must be falsi ed and [not(A)] holds.

Provenance program PI is constructed from follows:

For the ith rule A B1; : : : ; Bm; not C1; : : : ; not Cn (m + n 1) in provenance rule A ( [ri ^ :I(C1) ^ : : : :I(Cn)] B1 : : : Bm to PI ; 8A 2 H , if A 2 (resp. A 2= ) add A ( [A] (resp. A ( [:not(A)]) to PI . Operator G (I) = M P returns the least model of PI .

I and WnP interpretation I as add

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 unde ned in the WFM of . The following de nitions 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 Damasio et al. 2013))

Let G 2= and F 2 (resp. R 2 ) be sets of facts (resp. rules). Literal L 2 W F M (( n(F [R))[G) i there is a conjunction of literals C j= 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) = fA: j A 2 F g RemoveFacts(C) = fA: j :A 2 F g KeepRules(C) = fri : A Body j ri 2 R and ri 2 g RemoveRules(C) = fri : A Body j :ri 2 R and ri 2 g

NoFacts(C) = fA: j not(A) 2 Gg MissingFacts(C) = fA: j :not(A) 2 Gg

Example 3 (From (Viegas Damasio 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) = 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 unsatis ed 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. [not(e)] One obtains AS provenance from the WFM provence basically by forcing all atoms to be either positive or negative, i.e., non-unde ned, and using the provenance determined for the WF semantics (see examples in Section 2).

Justi cations are de ned as: Given a logic program and a literal l, a justi 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 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 Damasio et al. 2013) that evidence graphs (Pemmasani et al. 2004) and o -line justi cations (Pontelli et al. 2009) models can all be captured by WnP implicants, but some of our justi cations cannot be mapped by them. Also related to provenance are causal chains (Cabalar and Fandin~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 re ecting some sequence of rule applications.

2 Contributions: Meta-Transformation for Provenance Formulae

We de ne 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 speci c transformations for WF and AS semantics; (2) WF speci c modules 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.

fact = ff act(X) hasBody(R) hasBody(R) Rules = fkeepRule(X)

removeRule(X) F acts = fmissingF act(X) noF act(X) rule(R); head(R; X); not hasBody(R): rule(R); bodyP (R; A): rule(R); bodyN (R; A):g rule(X); not removeRule(X): rule(X); not keepRule(X):g atom(X); not f act(X); not noF act(X): atom(X); not f act(X); not missingF act(X):g

Module fact 2 common de nes facts as rules in the program having empty bodies. Module fact assumes that module in 2 D( ) (Fig. 1.2) will also be applied, since it depends on all facts de ned 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 identi ers. ttu = f t(H) t(H) tu(H) tu(H) tu(H) atom(A); t(A); not tu(A): head(R; H); not ap(R; t); not ap(R; tu); not undef (H); removeRule(R): head(R; H); keepRule(R); ap(R; t); not undef (H): atom(H); missingF act(H); not f act(H); not undef (H): head(R; H); keepRule(R); ap(R; tu): atom(H); missingF act(H); not f act(H): atom(H); undef (H):g apttu( ) = fap(ri; t) ap(ri; tu) j A t(B1); : : : t(Bm); not tu(C1); : : : ; not tu(Cn):; tu(B1); : : : tu(Bm); not t(C1); : : : ; not t(Cn):

B1; : : : Bm; not C1; : : : ; not Cn 2 and identi ed by ri:g

2.1 Provenance for the WF Semantics

A provenance program under the WF semantics is captured by wfs combined with debugging modules common and in. Module ttu encodes the 2 operator for the program subject to changes de ned 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 unde ned (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 unde ned, 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 [ wfs( ) s.t.: If A 2 H s.t., fact A 2 and A 2 M then keepRule(rA ) 2 M 0 and removeRule(rA ) 62 M 0 If A 2 H s.t., fact A 2 and A 62 M then keepRule(rA ) 62 M 0 and removeRule(rA ) 2 M 0 If not(A) 2 H s.t., no fact A in and not(A) 62 M then missingF act(A) 2 M 0 and noF act(A) 62 M 0 If not(A) 2 H s.t., no fact A in and not(A) 2 M then missingF act(A) 62 M 0 and noF act(A) 2 M 0 If ri 2 M then keepRule(ri) 2 M 0 and removeRule(ri) 62 M 0

If ri 62 M then keepRule(ri) 62 M 0 and removeRule(ri) 2 M 0

For the converse direction extra answer-sets of W ( ) may be generated. When we x the changes to all partial stable models (PSM) of the changed program are obtained, i.e. all xpoints of 2, instead of solely the least xpoint of 2. These models can be ltered out by guaranteeing minimality of the model. This is captured in the following Lemmata:

Lemma 2

Let M 0 2 AS(W ( ) = in( ) [ common [ wfs( )) and M odel(M 0) = fA j t(A) 2 M 0g [ fnot A j tu(A) 62 M 0g. Construct program 0 by deleting from every rule identi ed by ri s.t., removeRule(ri) 2 M 0, and adding a fact A in 0 for every missingF act(rA ) 2 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 [ wfs( ), 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 2 M 0.

Example 4

Recall now Ex. 2, to which we apply transformation W ( ) where in( ) = fhead(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):g. 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 correspondence 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 fnoF act(a); removeRule(r1); keepRule(f1; f2); missingF act(e)g, corresponding to conjuncts not(a); :r1; c; d; :not(e) of the previous formula and are ltered for readability: fkeepRule(r2; r3); missingF act(b)g fkeepRule(r2; r3); noF act(b)g fkeepRule(r2); removeRule(r3); missingF act(b)g fkeepRule(r2); removeRule(r3); noF act(b)g fremoveRule(r2); keepRule(r3); missingF act(b)g fremoveRule(r2; r3); missingF act(b)g 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 unde ned 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 rst we need an auxiliary notion de ning what is the WnP of an intended AS: 1 we denote a set of predicates fa(X); :::; a(Y )g as a(X; :::; Y ) as( ) = common [ wfs( ) [ f atom(A); tu(A); not t(A):

atom(A); undef (A):g

De nition 1 (Why not provenance for an interpretation )

Let be a logic program and I an interpretation. The AS WnP for I is: AnsW hyI = ^ AnsW hy (A) ^ AnsW hy (not A) ^ f:rjA 2 Head(r)g 8A2I 8A62I 8A62I

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 2 s.t., an atom A 2= I belongs to Head(r) which e ectively avoids considering rules giving support to unintended atoms, and thus providing unnecessary justi cations. 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 transformed program S( ) = in( ) [ as( ) s.t., M odel(M ) = I are in 1:1 correspondence with the models of AnsW hyI .

These models are complete in the sense they provide all possible justi cations 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: fa c; not b: b not a: d not c; not d: c not e: e f: f e:g. This program has answer-sets A1 : fa; cg and A2 : fb; cg. Below are some of the 144 WnP models for A1 from which we select the ones presenting intuitive explanations (model selection is clari ed next) from all of which the following literals are omitted: F = fkeepRule(r2; r3; r5; r6); noF act(b; d; e; f ); t(a; c)g: (1) fremoveRule(r1); keepRule(r4); missingF act(a; c)g (2) fremoveRule(r1; r4); missingF act(a; c)g (3) fremoveRule(r1); keepRule(r4); missingF act(a); noF act(c)g (4) fkeepRule(r1); removeRule(r4); noF act(a); missingF act(c)g (5) fkeepRule(r1; r4); missingF act(a; c)g (6) fkeepRule(r1; r4); noF act(a); missingF act(c)g (7) fkeepRule(r1; r4); missingF act(a); noF act(c)g (8) fkeepRule(r1); removeRule(r4); missingF act(a; c)g (9) fkeepRule(r1; r4); noF act(a; c)g

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 existing answer-sets, while the debugging approach is capable of obtaining more speci c results regarding the non-existence of answer-sets, namely in the presence of unfounded 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 (corresponding to the debugging part) and the other o ering a justi cation for why this interpretation is a model of the program (corresponding to the provenance part). t int = f

ics = f prune = f atom(A); int(A); not t(A): atom(A); int(A); t(A):g rule(R); violated(R); keepRule(R):g 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):g

Fig. 5. Transformation map = t int [ ics [ prune

Module t int ensures that atoms int and t are mapped which e ectively 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 [ ufLoop [ 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 n (fnoAnswerSetg [ fap(ri); bl(ri) j ri is a rule identi erg) 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 di erence: we prune debugging answer-sets which are not supported by the repaired program. Their exact relationship is captured next:

Theorem 4 (Mapping )

Let M 0 be an answer-set of J ( ). Then,

If unsatisf ied(ri) or violated(ri) 2 M 0 then removeRule(ri) 2 M 0; If unsupported(ri) 2 M 0 then missingF act(ri) 2 M 0; If uf Loop(a1::an) 2 M 0 then 9i 2 [1; : : : ; n] s.t., missingF act(ai) 2 M 0. Also, 9M 00 2 AS(J ( )) s.t. uf Loop(a1::an) [ missingF act(a1::an) 2 M 00.

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 removing 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 Damasio et al. 2013) and include relevant modules of transformation D. We show next a sample of its answer-sets, having F = fkeepRule(r1; r2; r3; r4; r6); unsupported(a; b), missingF act(a; b); noF act(c; e)g in common.

F [ fremoveRule(r5); unsupported(d; f ); unsatisf ied(r5); missingF act(d; f )g F [ fremoveRule(r5); unsatisf ied(r5); supported(c; e); noF act(d); unsupported(f ); missingF act(f )g F [ fkeepRule(r5); supported(c); unsupported(d); missingF act(d); noF act(f )g F [ fkeepRule(r5); supported(c); noF act(d; f )g

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 Damasio et al. 2013) and computing the models directly without rst 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 uni ed 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 justi cations for (intended) models. As expected, they are exponential. One direction to explore is to obtain prime implicant by optimizing these models using rei cation 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 2p-complete problem. Alternative o ine justi cations (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 unde ned in the WFM); false literals have to keep all their rules; the dependency graph is acyclic; The major di erence to Pontelli's approach is that we provide justi cations for the full model from which we may obtain their justi cations, but our approach subsumes it since we are capable of ndng more justi cations as well as errors in the program.

References

Brain , M. , Gebser , M. , Puhrer, 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. , Puhrer, J., Skocovsky , 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 Fandin~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. , Schuller, 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 programming: 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 Arti cal 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 con ictdriven 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. , Puhrer, 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) , Wurzburg, Germany, D. Seipel , M. Hanus , A. Wolf , and J. Baumeister, Eds. Technical Report 434 , Bayerische Julius-Maximilians-Universitat Wurzburg, Institut fur Informatik , 258 { 261 .

Lee , J. 2005 . A model-theoretic counterpart of loop formulas . In Proceedings of International Joint Conference on Arti cial Intelligence (IJCAI) . Professional Book Center , 503 { 508 .

Oetsch , J. , Puhrer, 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 justi cation for tabled logic programs . In Functional and Logic Programming , Y. Kameyama and P. Stuckey, Eds. Lecture Notes in Computer Science , vol. 2998 . Springer Berlin Heidelberg, 24 { 38 .

Pereira , L. M. , Damasio , 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 .

Pontelli , E. , Son , T. C. , and El-Khatib , O. 2009 . Justi cations for logic programs under answer set semantics . TPLP 9 , 1 , 1 { 56 .

Viegas Damasio , C. , Analyti , A. , and Antoniou , G. 2013 . Justi cations for logic programming . 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 .