Witnesses for Answer Sets of Basic Logic Programs

1 Introduction

Explanation tasks in AI include justifying the behavior of autonomous agents, debugging machine learning models, explaining medical decision making, and explaining classifier predictions [Burkart and Huber, 2021; Dazeley et al., 2021]. The subject has been attracting growing attention with the success of deep learning neural networks [Marques-Silva and Huang, 2024; Weber et al., 2024]. Notably, explaining symbolic reasoning has been extensively studied in the past in several different contexts, including database query languages such as Datalog [Cheney et al., 2009; Arioua et al., 2015], ontological reasoning under description logics [Bienvenu et al., 2019; Pe˜naloza, 2020] and existential rules [˙Ismail ˙Ilkan Ceylan et al., 2025].

Logic programming under answer set (stable model) semantics (ASP in short) is a declarative problem solving paradigm [Baral, 2003; Brewka et al., 2011]. It encodes the specifications of a problem in a logic program whose answer sets correspond to the solutions of the problem, which has been widely and successfully applied in planning, diagnosis, scheduling [Gebser et al., 2012; Brewka et al., 2016; Lifschitz, 2019] thanks to the efficient ASP solvers clingo and DLV. An explanation for the answer sets of a logic program amounts to answering "why a set of atoms is an answer set in a well-justified manner, instead of by definition" [Fandinno and Schulz, 2019]. This is quite useful for debugging ASP programs. From the perspective of knowledge representation, an explanation for a solution may be equally or more important than the solution itself [Sosa, 2019]. This challenging task has been extensively investigated from the perspective of off-line justification [Pontelli et al., 2009], causal graph [Cabalar and Fandinno, 2016], minimal assumption set and well-founded derivation [Alviano et al., 2024] and so forth. Various explaining ASP tools and systems are available, such as DiscASP [Li et al., 2021], s(CASP) [Arias et al., 2020], xclingo [Cabalar et al., 2020] and xASP [Alviano et al., 2024].

Abstract constraint atoms (c-atoms) [Marek and Truszczynski, 2004] are a general framework to capture complex constructors in logic programs, such as weight constraints [Simons et al., 2002] and aggregates [Dell'Armi et al., 2003; Faber et al., 2004; Ferraris, 2011]. Such constructors are widely used in practical ASP languages, and they usually complicate the answer set semantics of logic programs [Son et al., 2007; Liu et al., 2010; Shen et al., 2009; Gelfond and Zhang, 2019; Alviano et al., 2023]. Very recently, the explanation issue for answer sets was investigated from the perspective of witness for disjunctive logic programs [Wang et al., 2023], and mjustifications and r-justifications for FLP-answer sets [Faber et al., 2004] of logic programs with abstract constraint atoms [Eiter and Geibinger, 2023]. It is well-known that FLPanswer sets suffer from circular justifications.

This paper follows the idea of the witness approach to the explanation issue of another answer set semantics of logic programs with abstract constraint atoms, namely SPT-answer sets [Son et al., 2007; Shen et al., 2009; Shen et al., 2014]. These answer sets have the property of excluding circular justification in FLP-answer sets, which makes the SPT-semantics particularly attractive. Informally, witnesses are resolution proofs in the context of an answer set that respect dependencies among atoms. The main contributions of the paper are as follows.

• We present a general minimal reduct for logic programs with c-atoms. Informally, the minimal reduct is to properly remove all the assumed false atoms from a logic program [Wang et al., 2023]. With the help of minimal reduct, a new characterization of SPT-answer sets is established and the minimal model decomposition theorem [Angiulli et al., 2022] is then extended to logic programs without nonmonotonic c-atoms.
• We propose a notion of CA-resolution for rules with catoms to resolve a c-atom at one resolution step. We show that every atom in an SPT-answer set of a logic program has a sound CA-resolution proof from the minimal reduct of the logic programw.r.t. the SPT-answer set.
• Finally, we present the notions of α-witness and βwitness to explain why an atom is in an SPT-answer set in terms a CA-resolution proof. While α-witnesses are concerned with a set of atoms in each step, β-witness are concerned with a single atom.

Since the current well-known ASP solvers compute FLPanswer sets and SPT-answer sets are non-circular FLP-answer sets, this "resolution proof"-based witness has potential practical applications for ASP, e.g., debugging of ASP programs.

The remainder of the paper is outlined as follows. In the next section, we present the basic notions and notations of logic programs with c-atoms. Section 3 presents minimal reduct and its properties about minimal model decomposition. Section 4 contains the CA-resolution. The α-witness and βwitness are presented in Section 5. We compare the β-witness with r-justification in Section 6. Finally, concluding remarks and future work are discussed in Section 7.

2 Preliminaries

In this section, we recall some basic notions and notations of logic programs with abstract constraint atoms [Marek and Truszczynski, 2004; Faber et al., 2004; Son et al., 2007; Liu et al., 2010; Shen et al., 2009] and the dependency graph of logic programs [Angiulli et al., 2022].

2.1 Syntax and semantics

We assume an underlying propositional language L over a finite set A of atoms. The notions of atoms, literals, interpretations, satisfaction, models, minimal models, least models, and logical consequences are the standard ones in L.

An abstract constraint atom (c-atom in short) is a tuple A = (D, C), where D ⊆ A is its domain and C ⊆ 2D is the set of candidate solutions of A. For a c-atom A = (D, C), we denote Ad = D and Ac = C. We use ⊤ to denote (D, 2D ) and ⊥ for (D, ∅). Any propositional atom a can be expressed by the c-atom ({a}, {{a}}). We call the latter elementary, and whenever convenient, we identify it with a. The complement of a c-atom A = (D, C) is A = (D, C) where C = 2D \ C. It is evident A = A. A c-literal is either a c-atom A (positive c-literal) or its (default) negation not A (negative c-literal).

Let A = (D,C) be a c-atom. It is monotonic if S ∈ C implies S′ ∈ C for all S and S′ with S ⊆ S′ ⊆ D. It is convex if S′′ ∈ C implies S′ ∈ C for all S, S′ and S′′ with S ∈ C and S ⊆ S′ ⊆ S′′ ⊆ D. It is anti-monotonic if for every S ⊆ D, S ∈ C implies S′ ∈ C for every S′ ⊆ S.

A (disjunctive) logic program (with abstract constraint atoms) is a finite set of rules of the form,

where Ai (1 ≤ i ≤ n) are c-atoms.

Let r be a rule of the form (1). We denote the head of r by hd(r) = {Ai | 1 ≤ i ≤ l}, the positive body of r by bd+(r) = {Ai | l + 1 ≤ i ≤ m}, the negative body of r by bd-(r) = {Ai | m+ 1 ≤ i ≤ n} and the body of r by bd(r) = bd+(r) ∪ not bd-(r), with not S = {not s | s ∈ S}. For simplicity, a rule r is usually written as

A rule of form (1) is called normal if l = 1, a constraint if l = 0, a fact if l = n = 1 and A1 is elementary and in this case the "←" is usually omitted, positive if n = m, definite if it is normal and m = n, basic if every Ai (1 ≤ i ≤ l) is elementary 1 ; convex if every Ai, for 1 < i ≤ n, is convex. A logic program is normal (positive, definite, basic and convex, respectively) if all its rules are normal (positive, definite, basic, and convex respectively). In the present paper, we focus on the fragment of basic logic programs and assume that logic programs are of this form unless explicitly stated otherwise.

Let I be an interpretation (a set of atoms). The satisfaction relation (model) |= is defined below: let A be a c-atom, S be a set of c-literals, r be a rule, P be a logic program,

• I |= A if I ∩Ad ∈ Ac;
• I |= notA if I does not satisfy A;
• I |= S if I |= s for every s ∈ S;
• I |= r if I |= bd(r) implies I |= h for some h ∈ hd(r);
• I |= P if I |= r for every r ∈ P.

Let M and S be two sets of atoms. We say that S conditionally satisfies a c-atom A w.r.t. M, written S |=M A, if S |= A and I ∈ Ac for every I with S ∩ Ad ⊆ I ⊆ M ∩ Ad. By S |=M T for a set T of c-atoms we mean S |=M A for every A ∈ T.

Let P be a normal basic logic program with c-atoms. A set M ⊆ A is an SPT-answer set of P whenever M = T ∞ P M (∅, M) where

• P M is obtained from P by
• removing every rule r from P if M |= A for some A ∈ bd-(r), and
• removing all the remaining not A from P where A is a c-atom;
• the operator TP : 2A × 2A → 2A is defined as, for a definite basic logic program P ,

A set M ⊆ A is an FLP-answer set of a logic program P if M is a minimal model of the FLP-reduct P M,FLP of P w.r.t. M, given by P M,FLP = {r ∈ P | M |= bd(r)}.

1 This is different from the one in [Shen et al., 2009] in which it requires l = 1 additionally. Thus, the notion of "basic" in [Shen et al., 2009] corresponds to "normal basic" in this paper.

Let W and V be two disjoint subsets of A. The W-prefixed power set of V is the family W ⊎ V = {W ′ | W ⊆ W ′ ⊆ W ∪ V } of all subsets W ′ between W and W ∪ V ; it is maximal in a c-atom A if W⊎V ⊆ Ac and there is no other W ′ and V ′ such that W ′ ⊎V ′ ⊆ Ac andW ⊎V ⊂W ′ ⊎V ′ . The set of all maximal prefixed power sets of A is denoted by A∗c . Intuitively, A∗c contains all maximal intervals [W,W ∪ V ] of the powerset lattice in Ac; computing A∗c fromAc is tractable, cf. Theorem 3.5 of [Shen et al., 2009].

Definition 1. Let A be a c-atom and I an interpretation. W ⊎ V ∈ A∗c is an abstract satisfiable set of A w.r.t. I if I ∩Ad ∈ W ⊎ V . In this case, W is called a satisfiable set of A w.r.t. I ∩ Ad.

Given a basic logic program P and an interpretation I, the generalized Gelfond-Lifschitz reduct of P w.r.t. I, written as P I,SY Y , is the basic logic program obtained from P by:

• (a) removing from P all rules whose bodies contain either a negative c-literal notA such that I |= A or a c-atom A such that I ̸|= A,
• (b) removing all negative c-literals from the remaining rules,
• (c) replacing each c-atom A in the body of a rule with a special elementary atom θA and introduce a new rule

for each satisfiable set W = {a1, . . . , am} of A w.r.t. I ∩ Ad,

• (d) replacing hd(r) with hd(r) ∩M,

Definition 2. An interpretation I ⊆ A is a stable model of a logic program P if P I,SY Y has a minimal model M such that I = M ∩ A.

It has been shown that, for every positive normal logic program P , M ⊆ A is an SPT-answer set of P according to [Son et al., 2007] if and only if M is a stable model of P by Definition 2, cf. Theorem 6.2 of [Shen et al., 2009]. We thus refer to stable models by Definition 2 also as SPT-answer sets.

Note that if P is a positive logic programwithout c-atoms, i.e., all atoms are elementary, then the answer sets of P are exactly the minimal models of P . However, if P is a positive logic program with c-atoms, a minimal model of P may not be an FLP-answer set of P, and thus not an SPT-answer set of P 2 . For example, let P = {a ← ({a, b}, {∅, {a, b}})}. The set M = {a} is a minimal model of P . But M is not an FLP-answer set of P. In fact, P has no FLP-answer set.

2.2 Dependency graph

The (positive) dependency graph 3 GP of a logic program P is the directed graph (V, E), where

• V consists of all the atoms occurring in P and,
• (q, p) ∈ E if, for some r ∈ P and A ∈ bd+(r), p ∈ hd(r) and some W exists s.t. q ∈ W and W ⊎ V ∈ A∗c .

2 For positive basic logic programs, SPT-answer sets are welljustified FLP-answer sets, cf, Theorem 9 of [Shen et al., 2014].

3 The dependency graph defined below coincides with the one in [Angiulli et al., 2022]. But the direction of edge or arc is opposite to that given in [Lin and You, 2002; Shen et al., 2009].

For a directed graph G = (V, E) and v ∈ V , we denote by DG(v) the set of all ancestor nodes u of v in G, i.e., G has a path v0, . . . , vn+1 with v0 = u and vn+1 = v; for any set V ′ ⊆ V we let DG(V ′ ) = ⋃v′∈V ′ DG(v′ ). A vertex v is a source of G if DG(v) = ∅. If P is clear from its context, i.e., G is the dependency graph of P , we also call v a source of P .

The SCC-graph of a directed graph G = (V,E) is the directed acyclic graph (DAG) SG = (V, E) [Leone et al., 1997] where

• V is the set of the strongly connected components (SCCs) of G, i.e., every C ∈ V is a maximal subgraph G′ = (V ′ ,E′ ) of G such that G′ has a path from any vertex v′ ∈ V ′ to every other vertex in V ′ ; we also denote C by V ′ when it is clear from its context, and
• E consists of all edges (C, C ′ ) such that E∩(C×C ′ ) ̸= ∅, i.e., there are p ∈ C and q ∈ C ′ for some (p, q) ∈ E.

For a logic program P, we write SP instead of SGP for convenience. The atom-clause dependency graph of a basic logic program P is the directed graph GP = (V, E), where

• V consists of the atoms and rules occurring in P;
• for each rule δ ∈ P, E contains edges (q, δ) ∈ E and (δ, p) ∈ E for all p ∈ hd(δ) and q ∈ W for some A ∈ bd+(δ) and W ⊎ V ∈ A∗c for some V , respectively.

Intuitively, if both (A, δ) and (δ,B) are in E, then A depends on B by rule δ. The super-dependency graph SGP of P is then the collapsed dependency graph of GP , i.e., SGP =SGP . We call a source of SGP also a source of P .

The example below demonstrates these dependency graphs.

Example 1. Let P consist of the following rules:

where A = ({a, b}, {{a}, {b}}). Then, A∗c = {{a}⊎∅, {b}⊎ ∅}. The various dependency graphs for P are as follows:

• GP = (V1, E1) with V1 = {a, b, c} and E1 = {(b, a), (a, b), (a, c), (b, c)}. Notice that this graph has no source, and that the SCCs of GP are {c} and {a, b}.
• Hence, SP = (V2, E2) with V2 = {v1, v2}, v1 = {a, b}, v2 = {c} and E2 = {(v1, v2)}.
• GP = (V3, E3) with V3 = V1∪{r1, r2, r3, r4} and E3 = {(r1, a), (b, r1)} ∪ {(r2, b), (a, r2)} ∪ {(r3, a), (r3, b)}∪ {(r4, c), (a, r4), (b, r4)}. Its SCCs are {r3}, {r4}, {r1, r2, a, b}, and {c}.
• Hence, SGP = (V4,E4) with V4 = {v1, v2, v3, v4}, v1 = {a, b, r1, r2}, v2 = {r3}, v3 = {r4}, v4 = {c} and E4 = {(v1, v2), (v1, v3), (v3, v4)}. Here, v1 is its unique source.

3 Minimal Reduct andModel Decomposition

In this section, we propose the notion of minimal reduct and prove our minimal model decomposition theorem for basic logic programs.

3.1 Minimal reduct

Let A be a c-atom and M ⊆ A. The (extended) minimal reduct of A w.r.t. M, written MR(A,M), is defined as

• (a) ⊥ if M ̸|= A,
• (b) ⊤ if either M |= A and Ad ∩ M = ∅, or 2Ad∩M = {S ∩M | S ∈ Ac},
• (c) (Ad ∩ M,Bc) where Bc = {Z | there is W ⊎ V ∈ A∗c such that M∩Ad ⊆W∪V andW ⊆ Z ⊆M∩Ad} if M |= A and M ∩ Ad ̸= ∅.

Intuitively, given the assumption M ⊆ A that the atoms in M are true and the others are false, the minimal reduct MR(A,M) of a c-atom A removes from A the assumed false atoms and candidate solutions in which they are true. For instance, let A = ({a, b}, {{a}, {b}}). Recall that A∗c = {{a} ⊎ ∅, {b} ⊎ ∅}. We have MR(A, {a, b}) = ⊥ since {a, b} ̸|= A and MR(A, {a}) = ({a}, {{a}}).

Note that for an elementary atom a, the corresponding catom is A = ({a}, {{a}}). Thus, MR(A, M) = A if M |= A and ⊥ otherwise. For the c-atom A = ({a}, {∅}), M |= A whenever M ∩ {a} = ∅. In this case, MR(A,M) = ⊤ if M |= A and ⊥ otherwise.

Let P be a basic logic program, and M ⊆ A. The minimal reduct of P w.r.t. M, written MR(P,M), contains for each r ∈ P with M |= bd(r), the rule

Please note that MR({r},M) = ∅ if M ̸|= bd(r). Thus, this minimal reduct for basic logic programs is indeed a generalization of the same notion for logic programs without c-atoms.

Intuitively, the minimal reduct MR(P,M) of a logic program P w.r.t. M keeps the rules whose body is satisfied by M and applies the minimal reduct to all c-atom in their heads and positive bodies, and it removes the negative bodies; furthermore, simplications (remove ⊤ in bodies, ⊥ in heads) are made. We note that the minimal reduct for basic logic programs generalizes the one for disjunctive logic programs [Wang et al., 2023]. It is different from the GL-reduct [Gelfond and Lifschitz, 1988], FLP-reduct [Faber et al., 2004], and Ferraris's reduct [Ferraris, 2011].

Proposition 1. Let r be a basic rule and M ⊆ A. The following statements are equivalent to each other.

• (i) M |= r.
• (ii) M |=MR({r},M).
• (iii) M ∗ |= {r}M,SY Y where M ∗ = M ∪ {θA | A ∈ bd+(r),M |= bd(r)}.

In terms of the minimal reduct, we obtain a new characterization for SPT-answer sets as follows.

Theorem 1. Let P be a basic logic program, and M ⊆ A. Then, the following statements are equivalent to each other.

• (i) M is an SPT-answer set of P.
• (ii) M ∗ is the least model of P M,SY Y where M ∗ = M ∪ {θA | r ∈ P,M |= bd(r), A ∈ bd+(r)}.
• (iii) M is the least model of MR(P,M).

The following example confirms the new characterization of SPT-answer sets in terms of the minimal reduct.

Example 2 (Continued from Example 1). Let M = {a, b}. One can check that M is the unique minimal model of P and an SPT-answer set of P: MR(P,M) = {r1, r2, r3} and the least model of MR(P,M) is M.

3.2 Minimal model decomposition

In this section, we present a theorem for decomposing minimal models of basic logic programs generalizing previous results.

Let Σ be a basic positive program. We call a source S of SGΣ empty, if S ∩ A = ∅, and denote by ΣS the set of rules in Σ that mention only atoms from S.

For a basic positive program Σ and X ⊆ A, the logic program Reduce(Σ, X) is obtained from Σ by

• (a) removing every rule r if hd(r) ∩X ̸= ∅,
• (b) removing every c-atomA from rule bodies if Ad \X = ∅ and X ∩ Ad ∈ Ac,
• (c) replacing each remaining c-atomA by A′ where A′d = Ad \ X and A′c = {S \ X | S ∈ Ac}.

Clearly, if in Step (b) the c-atom A is an elementary atom a ∈ X, then A is removed. Thus, this reduction generalizes Reduce(Σ,X, ∅) for propositional clause theories Σ [BenEliyahu-Zohary et al., 2017; Angiulli et al., 2022], which replaces every atom p occurring in Σ by true if p is in X.

Proposition 2. Let P be a basic positive program with merely monotonic c-atoms. A set M ⊆ A is a minimal model of P if and only if M is the least model of MR(P,M).

We note that the monotonicity condition in the above proposition is necessary and can not be relaxed to convexity:

• Let P1 = {a ← ({a}, {∅})}. The c-atom in the rule body is convex, and clearly {a} is the unique minimal model of P1. But P1 has no SPT- and no FLP-answer set.
• Let P2 = {a ← ({a, b}, {∅, {b}})). The c-atom in the rule body is convex and nonmonotonic. The set {a} is the unique minimal model of P but neither an SPT- nor an FLP-answer set of P2.

Theorem 2 (Minimal model decomposition). Let P be a basic program without nonmonotonic c-atoms, M be a minimal model of P and Q = MR(P,M). Then, for any nonempty source S of Q, X = M ∩ S is a minimal model of QS, and M \ X is a minimal model of Reduce(Q, X).

Based on Theorem 2, a minimal model verification algorithm is presented in Algorithm 1. It generalizes similar ones for propositional clause theories [Ben-Eliyahu-Zohary et al., 2017; Angiulli et al., 2022] and for disjunctive logic programs without c-atoms [Wang et al., 2023].

Note that a model M of a clause theory T is minimal if and only if the clause theory T ∪ {¬p | p ∈ A \ M} ∪ {∨{¬p | p ∈ M}} is unsatisfiable, where ∨ S is the disjunction of all elements in S. The above algorithm CheckMinMRCA decomposes the minimal model checking (unsatisfiability) to a series of minimal model checks in terms of modularity i.e., Theorem 2. The following result states its correctness.

Algorithm 1: CheckMinMRCA (Π, N)

Input: A basic positive program Π with merely

• monotonic c-atoms and a model M of Π Output: true if M is a minimal model of Π, else false 1 Σ←MR(Π,M); N ←M; G← SGΣ; 2 Recursively delete from G all empty sources; 3 while G has some nonempty source S do 4 if S ∩ N is not a minimal model of ΣS then break Σ ← Reduce(Σ, N ∩ S); 5 N ←N -S; 6 G← SGΣ; 7 Recursively delete fromG all empty sources; 8 end
• 9 if N = ∅ then return true else return false

Theorem 3. Let P be a basic positive program without nonmonotonic c-atoms and M be a model of P. Then M is a minimal model of P iff CheckMinMRCA(P,M) returns true.

4 Resolution of c-atoms

In this section, we present the notion of resolution proof for basic positive rules, which we also call clauses with c-literals (CA-clauses in short).

Definition 3 (CA-resolution). Let r, r1, . . . , rn (n ≥ 1) be CA-clauses such that

• ai ∈ hd(ri) (1 ≤ i ≤ n),
• A ∈ bd(r) and some W exists such that W = {a1, . . . , an} and W ⊎ V ∈ A∗c .

The result of CA-resolution r, r1, . . . , rn on W of A, written res(r, r1, . . . , rn, A,W), is the following CA-clause:

which we call the resolvent of CA-resolution r, r1, . . . , rn on W of A. In this case, we call r, r1, . . . , rn resolvable on A w.r.t. W.

Please note that if A is elementary, then there are exactly two CA-clauses involved in the CA-resolution. Thus, the CA-resolution is indeed a generalization of the resolution for propositional clauses. The CA-resolution for the resolvent res(r, r1, . . . , rn,A,W) is sound if every model of {r, r1, . . . , rn} is also a model of res(r, r1, . . . , rn, A,W).

Example 3. Let us consider the following CA-clauses:

We can check that both res(r, r1, r2,A, {a1, a2}) and res(r, r1,B, {b1}) are sound. However, CA-resolution is not sound in general E.g., consider the following CA-clauses:

We then have res(r, r1, A, {a}) = c ←. Clearly M = {a, b} satisfies both r1 and r, but M ̸|= c.

Lemma 1. Let N ⊆ A, P be a basic positive logic program such that MR(P,N) = P and rules R = r, r1, . . . , rn in P are resolvable on A w.r.t. W. Then

• (i) MR(res(R,A,W),N) = res(R,A,W).

A CA-resolution proof of a CA-clause c from a set Σ of CA-clauses is a sequence

where Ri = ri , ri1 , . . . , rini , 0 ≤ i ≤ k, of CA-resolutions such that c = res(Rk , Ak ,W k ), and for every i, 0 ≤ i ≤ k,

• Ai ∈ bd(ri ), Wi = {ai,1, . . . , ai,ni },
• W i ⊎ V i ∈ Aic ∗ for some V i and
• ri , rij , 1 ≤ j ≤ ni, are from Σ ∪ {res(Rt ,At ,W t ) | 0 ≤ t < i}.

The CA-resolution proof (5) is sound if each CA-resolution for the resolvent of (5) is sound. By Σ ⊢CA c we denote that there is a CA-resolution proof of c from Σ, meaning that Σ can "derive" c (by a CA-resolution proof).

From item (ii) of Lemma 1 and the definition of minimal reduct, we obtain the following result.

Proposition 3. Let P be a basic logic program and M ⊆ A such that MR(P,M) = P . Then every CA-resolution proof of a clause c from P is sound.

For convenience and in abuse of notation, we let in what follows a ⊢CA a for atoms a ∈ A, i.e., any fact can derive itself by a CA-resolution proof.

The following theorem shows that for any SPT-answer set M of a basic logic program P, every atom in M admits a CA-resolution proof from the minimal reduct of P w.r.t. M. In this sense, such proofs can be taken as the justification for SPT-answer sets.

Theorem 4. Let M be an SPT-answer set of a basic logic program P. Then there is a sound CA-resolution proof for every a ∈ M from MR(P, M).

5 Witnesses

We are now in the position to present the notion of witnesses for SPT-answer sets of basic logic programs.

We first present the notion of minimal witness to capture the "minimal sufficient subprogram" (under set inclusion) for the CA-resolution proof.

Definition 4 ((minimal) Witness). Let M ⊆ A and B, S be disjoint subsets of M. A basic logic program P is a witness of B under S w.r.t. M if MR(P,M)∪S ⊢CA B. Moreover, P is minimal if no P ′ ⊂ P exists such that MR(P ′ , M)∪S ⊢CA B.

The set of all minimal witnesses P ′ ⊆ P of B under S w.r.t. M is denoted by MW(B, P, S, M).

In other words, under the assumption M (to be justified as an SPT-answer set of a basic logic program P ) and the justified subset S of M, the (minimal) witness of B under S w.r.t. M is

Algorithm 2: MinWitness(Π, B, S, M)

Input: A basic logic program Π, a nonempty SPT-answer set M of Π, and two disjoint subsets B, S of M Output: A minimal witness Π′ ⊆ Π of B under S w.r.t.M 1 Π′ ←MR(Π,M); 2 Π′′ ←Π; 3 foreach r ∈ Π′ do 4 if Π′ - {r} ∪ S ⊢CA B then 5 Π′ ← Π′ - {r}; 6 Π′′ ← Π′′ - {r′ ∈ Π | {r′ } = MR({r}, M)}; 7 end 8 end 9 return Π′′ ;

a (minimal) subprogram P ′ of P such that every atom in B has a CA-resolution proof from the minimal reduct MR(P ′ ,M) and the as justified regarded atoms in S. Algorithm 2 can be used to compute such a minimal witness.

Example 4. Let P consist of the following rules:

where A = ({a, b}, {{a}}) and A∗c = {{a} ⊎ ∅}. Then M = {a, c} is an SPT-answer set of P .

The CA-resolution res(r3, r1, A, a) is c ←, and P ′ c = {r1, r3} is the only minimal witness of {c} under ∅ w.r.t. M. Under M and the justified a, the minimal sufficient subprogram to "justify" c is {r3}, i.e., MW({c}, P, {a},M) = {{r3}}.

5.1 α-witness and α⋆ -witness

The following notions of α-witness and α⋆ -witness capture the structural witness for SPT-answer sets. They serve to explain why a group of atoms are in an SPT-answer set.

Definition 5 (α∗ -witness and α-witness). Let P be a basic logic program, M ̸= ∅ be an SPT-answer set of P , B and S be disjoint subsets of M. An α⋆ -witness of B under P and S w.r.t. M is a directed acyclic graph G = ({(Si, Pi)|1 ≤ i ≤ n}, E) where

• {Si | 1 ≤ i ≤ n} is a partitioning of B (i.e., ⋃ni=1 Si = B, Si ∩ Sj = ∅ (i ̸= j) and Si ̸= ∅), and
• for every i, 1 ≤ i ≤ n,

(i) Pi ⊆ P is a witness of Si under S ∪Xi w.r.t. M, (ii) Pi is not a witness of Sj under S ∪ Xi w.r.t. M, for every 1 ≤ j ̸= i ≤ n and (Sj, Pj) /∈

• DG((Si, Pi))4 , where for each k (1 ≤ k ≤ n),

If G induces a total order (S1, P1) < (S2, P2) < · · · < (Sn, Pn), i.e., E = {((Si, Pi), (Si+1, Pi+1)) | 1 ≤ i < n}, then we call it an α-witness of B under P and S w.r.t. M, and denote it as

4 If (Sj , Pj) ∈ DG((Si, Pi)) then Sj ⊆ Xi and Q∪Xi ⊢CA Sj for any basic logic program Q.

We call G minimal, if every Pi is minimal and G is compact, if in addition to minimality Pi ∩Pj = ∅ for all 1 ≤ i < j ≤ n. If B = M and S = ∅, we call G a (minimal, compact) α⋆ - witness resp. α-witness of M w.r.t. P .

Note that Definition 5, requires M ̸= ∅. This means that for an empty SPT-answer set (= ∅) of a logic program, no witness is defined; however, in this case no atom needs to be justified.

While α⋆ -witnesses are any directed acyclic graphs, αwitnesses are chains. Intuitively, for each node (Si, Pi) of a witness, the atoms in Si can be "derived" from Pi with the help of those "derived" atoms in Xi, that are on the paths of G to (Si, Pi). In this sense Pi is a justification for why the atoms in Si are in an SPT-answer set, i.e., Pi is minimal such that MR(Pi,M) ∪Xi can "derive" the atoms in Si.

Example 5. Let us consider the logic program P in Example 4. The SPT-answer set M = {a, c} of P has two α⋆ -witnesses:

• G1 = (V1, ∅) with V1 = {({a, c}, {r1, r3})};
• G2 = ({v1, v2}, {(v1, v2)}) with v1 = ({a}, {r1}) and v2 = ({c}, {r3}).

Notice that both G1 and G2 are α-witnesses since they can be written as W1 = [({a, c}, {r1, r3})] and W2 = [({a}, {r1}), ({c}, {r3})], respectively. It is easy to check that both G1 and G2 are compact.

The next proposition shows that every nonempty SPTanswer set of a basic logic program has a compact α⋆ -witness.

Proposition 4. Let P be a basic program, M ̸= ∅ be an SPT-answer set of P and Q = MR(P,M). Then, the DAG G = ({(Si,Qi) | 1 ≤ i ≤ n},E′ ) obtained from SQ = ({S1, . . . , Sn}, E) such that

• Qi ∈ MW(Si, P, S▷i,M), where S▷i = ⋃ DSQ (Si), 1 ≤ i ≤ n, and
• ((Si,Qi), (Sj,Qj)) ∈ E′ if (Si, Sj) ∈ E

is a compact α⋆ -witness of M w.r.t. P .

The compact α⋆ -witness constructed in Proposition 4 is called the full-split α⋆ (α⋆ fs )-witness of M w.r.t. P. The proposition also implies that DSG (Si) can be utilized to form different compact α⋆ -witnesses for M w.r.t. P . For example, if there is a path ((Si,Qi), (Si+1,Qi+1, . . . , (Sk,Qk)) in the DAG G = (V,E′ ) of Proposition 4, then the DAG G′ = (V ′′ , E′′ ) with

• V ′′ = V ′ \ {(Si′ ,Qi′), . . . , (Sk′ ,Qk′)} ∪ (⋃k′ j=i′ Sj, ⋃k′ j=i′ Qj) where i ≤ i′ ≤ k′ ≤ k, and
• ((Sv,Qv), (Su,Qu)) ∈ E′′ if ((Sv,Qv), (Su,Qu)) ∈ E′ and at most one of (Su,Qu) and (Sv,Qv) is combined in V ′′ , i.e., |{u, v} ∩ {i′ , . . . , k′ }| ≤ 1

is a compact α⋆ -witnesses for M w.r.t. P .

5.2 β-witness and β⋆ -witness

The notion of α-witness addresses the justifications for a group of atoms simultaneously. However, in many situations, including debugging, engineers are more concerned with the justification of individual atoms. This leads to the following more refined testimony.

Algorithm 3: MinBetaWitness(Π, B, S, M)

Input: A basic logic program Π, a nonempty SPT-answer Output: A minimal β-witness of B under Π and S w.r.t.

set M of Π, and two disjoint subsets B, S of M M 1 T ←S; Π′ ← [ ]; Σ←MR(Π,M); 2 while B - T ̸= ∅ do 3 while ∃r ∈ Σ s.t. bd+(r) ⊆ T, hd(r) = {p}, p ∈M -T do 4 T ← T ∪ hd(r); 5 Π′ .append((p, rm({r}, Π, M))); 6 end 7 if M = T then break Let u ∈ B - T ; 8 Σu ←MinWitness(Σ, {u}, T,M); 9 while Σu ∪ T ⊢ v for some v ∈M - ({u} ∪ T) do 10 Σv ← MinWitness(Σu, {v}, T, M); 11 u ← v; 12 Σu ← Σv; 13 end 14 Π′ .append((u, rm(Σu,Π,M))); 15 T ← T ∪ {u}; 16 end 17 return Π′ ;

Definition 6 ( (minimal, compact) β∗ - and β-witness). Let P be a basic logic program, M ̸= ∅ an SPT-answer set of P, and B, S be two disjoint subsets of M.

• Every α⋆ -witness G = ({(Si, Pi)|1 ≤ i ≤ n}, E) of B under P and S w.r.t. M such that Si = {pi} for some atom pi, 1 ≤ i ≤ n, is a β⋆ -witness of B under P and S w.r.t. M, also written as G = ({(pi, Pi)|1 ≤ i ≤ n}, E).
• The notions of β-witness and minimal/compact β⋆ resp. β-witness of B under P and S w.r.t. M are defined analogously to α-witness and minimal/compact α⋆ - resp. α-witness of B under P and S w.r.t. M.

In particular, if B = M and S = ∅, then we call G a (minimal, compact) β⋆ -witness, respectively, β-witness of M w.r.t. P .

Clearly β-witnesses and β⋆ -witnesses are special cases of α-witnesses and α⋆ -witnesses, respectively. It has been shown that an answer set of a logic program containing merely elementary atoms may not have a compact β-witness, and that deciding whether some compact β-witness exists is Σp2 - complete [Wang et al., 2023]. This motivates us to confine computation to minimal β-witnesses, which always exist.

Algorithm 3, MinBetaWitness, computes a minimal βwitness of B under a basic logic program P relative to S w.r.t. M. It uses a function rm(Σ,Π,M) that returns, given basic logic programs Σ, Π and M ⊆ A, a minimal subset Π′ of Π such that MR(Π′ ,M) = Σ. The external while-loop (line 2-17) checks whether all atoms in M have a minimal witness. The first inner while-loop identifies the atoms by unit propagation, while the second inner while-loop searches for an atom u and its minimal witness Σu under T such that there is no atom v in {u} ∪ T that can be observed by Σu ∪ T .

The next proposition shows the correctness of Algorithm 3. Thus, every nonempty SPT-answer set of a basic logic program has a minimal β-witness.

Proposition 5. If M is an SPT-answer set of a basic logic program P then MinBetaWitness (P, M, ∅, M) returns a minimal β-witness of M w.r.t. P .

Example 6. Let us consider the logic program P with aggregates from Example 14 in [Eiter and Geibinger, 2023], which consists of the following rules:

The formulas involving #sum are aggregate atoms of the form#sum{wi : li | 1 ≤ i ≤ n} ⪯ w where wi and w are numbers, ⪯ is an arithmetic comparison operator and li is a (possibly negated) atom. An interpretation M satisfies such an aggregate atom if (∑ni=1,M|=li wi) ⪯ w.

Hence the aggregate atoms #sum{1 : b, 2 : d}>2 and #sum{3 : d, 2 : c}<5 can be modeled as abstract constraint atoms A = ({b, d}, {{b, d}}) and B = ({c, d}, {∅, {c}, {d}}), respectively. Thus, rule r1 can be represented as

It is not hard to check that M = {a, b, d} is an SPT-answer set of P . We note that MR(B, M) = ⊤ as 2{c,d}∩M = {S ∩M | S ∈ {∅, {c}, {d}}} = {∅, {d}}. Thus, MR({r′1 , r2, r3},M) consists of following rules, where A′ = ({b, d}, {{b, d}}):

Furthermore, M has a unique compact β-witness, namely:

Informally, b ∈ M is justified by rule r3, as MR({r3},M) = {r′3 } (minimally) "derives" b. Then, with the help of b, MR({r2},M) = {r′2 } (minimally) "derives" d. Finally, with the help of b and d, MR({r1}, M) minimally "derives" a.

6 RelatedWork

There have been various notions for explaining answer sets of logic programs and some systems have been available. The difference between witness-based explanations, off-line justifications, and causal graph based ones have been discussed in [Wang et al., 2023]. To our best knowledge, only r-justification [Eiter and Geibinger, 2023] can deal with abstract constraint atoms. We firstly recall some basic notations and notions about r-justification.

A partial interpretation is a tuple I = 〈I +, I -〉, where I +, I - ⊆ A and I + ∩ I - = ∅; it is total on a set S of atoms if S ⊆ I + ∪ I -. For two partial interpretations J1, J2, we denote by J1 ≤ J2 that J + 1 ⊆ J + 2 and J - 1 ⊆ J - 2 , and by J1 < J2 that J1 ≤ J2 and J1 ̸= J2. A partial interpretation I = 〈I +, I -〉 satisfies a c-atom A if I + ∩ Ad ∈ Ac and, for each U ∈ Ac with I + ∩ Ad ⊂ U, U ∩ I - ̸= ∅ holds. The latter intuitively means that I + cannot be extended (under the restriction of I -) to falsify A. In other words, U ∈ Ac for every U s.t. Ad ∩ I + ⊆ U ⊆ Ad \ I -. If I is total (on Ad), then I |= A whenever I + ∩ Ad ∈ Ac.

Definition 7 (Presumptuous Entailment). Let P be a program, J be a partial interpretation and A be a c-atom. Then P |=J A if every total model I of P s.t. I ≥ J fulfills I |= A.

Definition 8 (Failed Support). Let r be a rule and I be a total model of r. Then, r is a failed support for atom a w.r.t. I if I ̸|= bd(r) and for every I ′ , I ′ |= a if I ′ |= r and I ′ |= bd(r).

Definition 9 (r-justification). Let P be a program, I be an answer set of P and a be an atom. Then, a triple (a◦ , Q, J), where ◦ ∈ {+,-}, Q ⊆ P is a set of rules, and J ≤ I, is a partial interpretation, is an r-justification for a w.r.t. P and I if the following conditions hold:

• (a) If a ∈ I, then ◦ = +, QI |=J a and there is no R ⊂ Q such that RI |=J a.
• (b) If a ̸∈ I, then ◦ = -, Q = {r ∈ P | r is a failed support of a w.r.t. I}, and for every r ∈ Q, J |= A for some A ∈ bd(r).

The r-justification is concise if J is ≤-minimal.

Definition 10 (r-justification chain). A sequence J = (a◦1 ,Q1, J1), · · · , (a◦n ,Qn, Jn) of r-justifications w.r.t. P and I is an r-justification chain for a1, if for every (a◦i , Qi, Ji) (1 ≤ i ≤ n), it holds that

• (a) for each a ∈ J + i some (a+j ,Qj, Jj) exists such that aj = a and either j > i or aj = a1 and there is no subsequence (a+k1 , Qk1, Jk1 ), · · · , (a+kℓ , Qkℓ , Jkℓ ) of J where k1 = 1, kℓ = i, and akh+1 ∈ J + kh , for all 1 < h < ℓ;
• (b) for each a ∈ J - i some (a-j ,Qj, Jj) exists s.t. aj = a;
• (c) if i > 1, then some (a◦j ,Qj, Jj) exists such that ai ∈ J ◦ j and j < i; and
• (d) ai = aj for 1 ≤ j ≤ n implies i = j.

It was shown that, for every logic program P and every FLP-answer I of P, every atom in I has an r-justification chain w.r.t. P and I, cf. Theorem 4 of [Eiter and Geibinger, 2023].

The next example shows some subtle difference between r-justification and witness.

Example 7. Let us consider the basic logic program P consisting of the following rules, where A = ({b, a}, {∅, {b, a}}): 5

It is not difficult to verify that I = {a, b} is the unique SPTanswer set of P. Note that A∗c = {∅ ⊎ ∅, {a, b} ⊎ ∅} and MR(P, I) consists of

Clearly {α1, α4} ⊢CA a and {α2, a} ⊢CA b. Thus, we have the following compact β-witness W for I w.r.t. P:

From this β-witness and the fact that the total models of {r1, r4} that extend the partial interpretation 〈∅, ∅〉

5 This logic program is similar to the one P7 ∪ P8 in Example 13 of [Eiter and Geibinger, 2023]

are 〈{a}, {b}〉 and 〈{a, b}, ∅〉, we obtain the following rjustification chain J for b:

Note that the FLP-reduct P I of P w.r.t. I is P. The total models of {r1, r3} are 〈{a}, {b}〉 and 〈{a, b}, ∅〉, i.e., the classical interpretations {a} an {a, b}. It is tedious but not difficult to check that(a+, {r1, r3}, 〈∅, ∅〉) (7)

is an r-justification for a w.r.t. P and I since {r1, r3} is (subset) minimal s.t. {r1, r3}I = {r1, r3} and {r1, r3}I |=〈∅,∅〉 a (every total model of {r1, r3} that extends the partial interpretation 〈∅, ∅〉 satisfies a). The r-justification chain (7) is indeed a chain. It explains why a is in the FLP-answer set by the argument that every total model of {r1, r3} that extends 〈∅, ∅〉 satisfies a. Due to the fact that MR({r1, r3}, I) = {α1, α3}, we have MR({r1, r3}, I) ̸⊢CA a; hence, this r-justification for a cannot be mapped to a witness for a. For the same reason, the following r-justification chain

for b cannot be mapped to a witness for b yet. Since {r1, r4} can derive a by classical resolution, while {r1, r3} cannot, the justification chain J is more intuitive than J ′ .

The next proposition shows that every minimal witness can capture an r-justification. Its converse does not hold, as shown by Example 7.

Proposition 6. Let P be a basic logic program, I be an SPT-answer set of P, S ⊆ I, and p ∈ I \ S. If Q ∈ MW({p}, P, S, I), then (p+,Q, 〈S, I〉) is an r-justification for p w.r.t. P and I.

Hence, when we consider r-justifications under SPT-answer set semantics, the minimal witness provides a more selective and intuitive way to chose rules as justifications as seen the J and J ′ in Example 7.

7 Conclusion

For logic programs with abstract constraint atoms, we have proposed the notions of minimal reduct, the resolution proof, and witness for SPT-answer sets. We showed that this minimal reduct provides a new characterization for SPT-answer sets of basic logic programs. It also facilitates an extended resolution for atoms in SPT-answer sets. Thus, an explanation in terms of "proof" can be obtained for the SPT-answer sets.

It is well-known that the problem of finding shorter resolution proofs in propositional logic is intractable [Haken, 1985]. To construct short CA-resolution-based explanations for SPTanswer sets is a challenge, but it deserves further investigation. In addition, we will analyze the computational complexity of (compact) α-witnesses and β-witnesses.

Acknowledgments

This research has been partially supported by the National Natural Science Foundation of P.R. China under grants 62376066 and 61976065 and was funded in whole or in part by the Austrian Science Fund (FWF) 10.55776/COE12.