A Sequent Calculus for Answer Set Entailment

1 Introduction

Answer Set Programming (ASP) is a symbolic rule-based reasoning formalism that has been used for various AI applications in numerous domains [Erdem et al., 2016; Falkner et al., 2018], among them scheduling [Ali et al., 2023; Abels et al., 2019; Yli-Jyr¨a et al., 2023], product configuration [Comploi-Taupe et al., 2022], life sciences [Erdem and Oztok, 2015], health insurance [Beierle et al., 2005], or psychology [Inclezan, 2015], to mention a few. ASP allows for a declarative encoding of problems in a succinct manner. Solutions for them are obtained from answer sets, which result from the evaluation of the encoding using an ASP solver. In this work, we study answer set entailment, which intuitively formalises which sentences hold in every answer set of a program. This concept itself is already of practical interest, and has been applied for diagnosis [Eiter et al., 1999] and planning [Eiter et al., 1997]. Notably, answer set entailment is at the core of abductive explanations [Eiter et al., 1997].

Given the practical usage of ASP, questions of explainability have been raised. Those questions or problems generally concern themselves with either answering why certain literals hold in a particular answer set or why there is no answer set at all, cf. Fandinno and Schulz [2019] for a survey. Both these questions can be formulated through answer set entailment. However, simply stating a valid entailment is in general not an explanation on its own and needs to be justified. Such justifications can be obtained via a formal proof system, incorporating the logical base of ASP in its inference rules.

For such a system of inference rules, i.e., proof system, to be meaningful for explainability, we argue that it should adhere to the following informal requirements: (R1) the rules and axioms of the proof system should be, like classical proof calculi, local and encode simple semantic concepts, (R2) the proof system should support commonly used language features of ASP, and (R3) the proofs should be concise and interpretable. Of course, those requirements are open to interpretation, but they are nonetheless useful desiderata for our purposes.

Although ASP has some efficient solvers available [Leone et al., 2006; Gebser et al., 2019; Alviano et al., 2013] and its model-theoretic properties have been studied extensively, the same cannot be said for proof-theoretic investigations.

Given the nonmonotonic nature of ASP, obtaining a proof calculus which fulfils all those criteria is non-trivial, but requirements (R1-R3) are important if one really wants to characterise the semantics in a way that can serve the explainability of the formalism. The few proof systems that do exist for answer set entailment [Gebser and Schaub, 2013; Bonatti et al., 2008; Pearce et al., 2000] are arguably weak on at least one of the requirements each.

In this work, we introduce a sound and complete sequent proof calculus for entailment in equilibrium logic (EL). The latter generalises ASP to arbitrary propositional theories and serves as a theoretical foundation of stable model semantics. Our calculus is very close to the original sequent calculus for classical logic invented by Gentzen [1935] and also takes inspiration from sequent calculi that were defined so related, but distinct, nonmonotonic formalisms [Olivetti, 1992; Bonatti and Olivetti, 1997a; Bonatti and Olivetti, 1997b]. In particular, we similarly use an anti-sequent calculus, which is a calculus that axiomatises non-entailment. As we will argue, without this component, even simple entailments may not be provable and that by adding a single non-entailment rule, which encodes the nonmonotonic stability condition inherent in ASP, we achieve a complete characterisation of answer set entailment.

Arguably, our approach is to be more aligned with the requirements (R1-R3) from above as previous calculi. The generated sequent proofs are, given some knowledge of proof theory, easy to parse and do not require multiple stages, auxiliary concepts, or complicated side conditions.

Briefly summarised, our main contributions are as follows:

• We provide an axiomatisation of answer set entailment in the form of a sequent calculus.
• We discuss an alternative characterisation that does not use the anti-sequent calculus, but requires rules which can only be applied in certain language fragments.
• We investigate how the calculus behaves when restricted to ASP programs and show which rules remain necessary.
• We show that answer set entailment is a useful framework for explainability and our calculus strengthens this by providing a formal way to justify entailment.

Our work enriches the rather sparse set of proof systems for ASP and equilibrium logic. Furthermore, the provided proofs are interpretable and can be translated into natural language as a basis for human-understandable explanations.

Missing proofs of the results are included in an extended version.

2 Background

Propositional equilibrium logic (EL) [Pearce, 1996; Pearce, 2006] generalises ground ASP semantics to arbitrary propositional formulas i.e. no restriction to rules.

We assume a denumerable set of propositional variables At . Formulas of EL are then defined in the usual manner over logical connectives ∧, ∨, ⊃, ¬ and logical constant ⊥.

The semantics of EL is based on the logic of here and there (also called HT logic), which is defined over the same language. An interpretation in HT logic is a pair ⟨H, T ⟩ where H ⊆ T ⊆ At. Whether an HT interpretation ⟨H, T⟩ is a model of a formula φ (denoted by ⟨H, T⟩ |= φ) is inductively defined as follows: ⟨H, T⟩ ̸|= ⊥, ⟨H, T⟩ |= p iff p ∈ H; ⟨H, T⟩ |= φ∧ψ iff ⟨H, T⟩ |= φ and ⟨H, T⟩ |= ψ; ⟨H, T⟩ |= φ ∨ ψ iff ⟨H, T⟩ |= φ or ⟨H, T⟩ |= ψ; ⟨H, T⟩ |= φ ⊃ ψ iff T |= φ ⊃ ψ, and ⟨H, T⟩ ̸|= φ or ⟨H, T⟩ |= ψ; ⟨H, T⟩ |= ¬φ iff T ̸|= φ and ⟨H, T ⟩ ̸|= φ.

Note that whenever H = T, ⟨H, T⟩ |= φ corresponds to the satisfaction relation of classical propositional logic. By slight abuse of notation, we use T |= φ to refer to ⟨T, T⟩ |= φ and call such models classical or total.

From the above semantics, two useful observations follow. The first is that ⟨H, T⟩ |= φ implies ⟨T, T⟩ |= φ. This property is also called persistence. The other important property is that ⟨H, T⟩ |= ¬φ iff T |= ¬φ, i.e., negation is only evaluated over T .

An HT model ⟨H, T⟩ of a formula φ is an equilibrium model iff H = T and for any other HT interpretation ⟨H′ , T⟩ such that H′ ⊂ H, ⟨H′ , T⟩ ̸|= φ. The latter conditions is also referred to as stability. We denote an equilibrium model ⟨T, T⟩ by T whenever convenient and we use a single set I to refer to classical interpretations. As usual, a set of formulas is called a theory, and we say that an interpretation is a model of a theory if it satisfies all contained formulas.

ASP programs are generally sets of rules of the form H ← B, where H and B are sets of literals. In EL, such a rule is encoded as an implication ∧ B ⊃ ∨ H and a program is then a theory consisting such an implication for each rule. As has been shown by Pearce [1996], the equilibrium models of such an encoded program amount to its answer sets.

From now on, whenever we talk about a program, we refer to a theory which encodes an ASP program as described above.

We use Γ |= φ to denote that a theory classically entails φ and Γ |=HT φ for entailment in HT.

Furthermore, by Var(Γ) we denote the set of atoms appearing in Γ and given a set S of atoms, we define ¬S = {¬p | p ∈ S} and ¬¬S = {¬¬p | p ∈ S}. Whenever Γ is clear from context, S = Var(Γ) \ S denotes the complement of S.

Sequent calculus was invented by Gentzen [1935] for intuitionistic as well as classical propositional and predicate logic. It performs syntactic operations on pairs of sequences of rules creating proof trees. We will make use of a so called antisequent calculus for HT. This calculus, introduced by Oetsch and Tompits [2011] is a refutation calculus and thus axiomatises non-entailment. An anti-sequent Γ ⊣HT ∆ consists of sets of formulas Γ and ∆. Figure 1 shows the rules of the antisequent calculus for HT; they are slightly reformulated but equivalent to the original calculus. An anti-sequent Γ ⊣HT ∆ is an initial sequent if Γ and ∆ are disjoint sets of literals and Γ is consistent, i.e., does not contain both an atom and its negation. Γ ⊣HT ∆ can be derived with the above rules and axioms iff Γ ̸|=HT ∆ holds.

3 EquilibriumEntailment

The inference relation we seek to axiomatise is the following. Definition 1 (Equilibrium Entailment). Given theories Γ and ∆, we say that Γ equilibrium entails ∆, written Γ ∣≈ ∆, if for every equilibrium model I of Γ, I |= φ for some φ ∈ ∆.

This notion is slightly different from the equilibrium entailment defined by Pearce [2006] but more aligned with answer set entailment. In the definition of Pearce, equilibrium entailment falls back to classical entailment whenever Γ has no stable models, which is not suitable for our intentions as we would like Γ ∣≈ ⊥ whenever Γ has no equilibrium models.

We argue that equilibrium entailment is a useful concept w.r.t. justification and explainability. We have already mention the special case when Γ ∣≈ ⊥ indicates that Γ is infeasible. By providing a proof of said inference, one effectively justifies that Γ and, given that the rules of the proof system are simple and interpretable, provides a baseline as to how an explanation should proceed. This of course also holds in the general case when one wants to know why a particular literal or sentence holds in every equilibriummodel. Furthermore, equilibrium entailment is also applicable when one already has a particular equilibrium model I and seeks to explain why certain atoms are, respectively, are not, in the model.

To apply entailment here, one needs to handle the nondeterminism inherent in stable model semantics. This motivates the next definition, which is inspired by a similar concept used for ASP justification graphs [Pontelli et al., 2009] and

Figure 1: Rules of the HT anti-sequent calculus

also Pearce's fix-point characterisation of equilibrium models [Pearce, 2006].

Definition 2 (Assumption Set). Given an interpretation I, a set of literals A is an assumption set w.r.t I if I |= ∧ ¬A.

An assumption set is minimal whenever it is a ⊆-minimal assumption set w.r.t I.

The intuition behind assumption sets will be more obvious after the following proposition.

Proposition 1. Given a theory Γ with equilibrium model I and some p ∈ Var(Γ), then there is a minimal assumption set A such that (i) Γ, ¬A ∣≈ p if p ∈ I, and (ii) Γ, ¬A ∣≈ ¬p if p ̸∈ I.

The basic idea is that the assumption set fixes the truth values of a necessary but minimal set of atoms to the truth value they have in the given model. Positive assumptions have to be added using double negation due to nonmonotonicity.

Example 1. Consider the theory consisting of the single formula a ∨ b. This theory has two equilibrium models {a} and {b}. For consider the former and suppose we want to answer why a is in the model. The minimal assumption sets for {a} are {¬a} and {b} and clearly Γ, ¬¬a ∣≈ a and Γ, ¬b ∣≈ a both hold. Intuitively, the assumption ¬¬a expresses that a is assumed to be true, whereas ¬b assumes that b is false.

Note that in the above example, simply assuming the truth of the atom we sought to justify was valid. It could be argued that for a proper explanation, only the latter, assuming b false, is preferable. However, we will leave such explanatory preferences for a different work.

We note the following observation, which is in the folklore and can be easily shown.

4 Sequent Calculus

We now introduce our notion of sequent, which will be the main building block for our proof system.

Definition 3. An equilibrium sequent is of the form Γ ∣∼ ∆, where Γ and ∆ are both sets of formulas.

An equilibrium sequent Γ ∣∼ ∆ is satisfied, if Γ ∣≈ ∆.

Our calculus has two axioms which will also be the allowed initial sequents in our derivations.

Definition 4. An initial sequent is either

Those initial sequents hold for any Γ and φ which follows from the Proposition 2 and from the fact that every equilibrium model is a classical model.

Proposition 3. The initial sequents given in Definition 4 are sound.

Now, as usual, a sequent proof is defined as follows.

Definition 5. A derivation of a sequent Γ ∣∼ ∆ is a tree that is rooted in the sequent, the leaves are initial sequents and parent nodes are generated by the application of some rule.

The initial sequents, as well as the basic rules, are all sound. Proposition 4. The basic rules given in Figure 2 are all sound, i.e., if the sequents in the premise are satisfied, then so is the

sequent in the conclusion.

The proof proceeds by showing the statement for each rule. Figure 2 shows the basic rules of our sequent calculus, which concern handling the logical connectives and weakening on the right. Note that most rules resemble their classical counterparts, except for (∨l) and (⊃l). The former allows us to directly exclude disjuncts which would not be part of an equilibriummodel as the following example shows.

Figure 2: Basic rules of the sequent calculus

Example 2. Consider the theory (a ∨ b) ∧ (b ⊃ a) which has one equilibrium model {a}. Hence, it holds that ¬b is equilibrium entailed.

The reason why the implication rule is different from the classical one is that by putting ¬φ on the right-hand side of the left premise, we can show that uneven negative cycles lead to instability.

Example 3. We will show that ¬p ⊃ p ∣≈ ⊥, i.e., has no equilibrium models.

The following restricted version of the classical cut rule stems from an axiomatisation of propositional circumscription [Olivetti, 1992].

As it turns out, (RCut) is also admissible in our case.

Proposition 5. The (RCut)-rule is sound for equilibrium entailment, i.e., if Γ ∣≈ ∆, φ and Γ, φ ∣≈ Σ, then Γ ∣≈ ∆, Σ.

Proof. Towards a contradiction, suppose Γ ̸∣≈ ∆,Σ, then there is some equilibrium model I of Γ such that I ̸|= ∆ and I ̸|= Σ. The former and Γ ∣≈ ∆, φ imply that I |= φ. Since Γ, φ ∣≈ Σ and I ̸|= Σ, there has to be some J ⊂ I such that ⟨J, I⟩ |= Γ ∪ {φ}. However, the latter implies ⟨J, I⟩ |= Γ contradicting I being an equilibrium model of Γ.

The rules mentioned so far are not enough to achieve a complete axiomatisation of equilibrium entailment, for example, we cannot show that a ⊃ b, b ⊃ a ∣≈ ¬a holds. Intuitively, the issue here is that a is not in any equilibriummodel, because it only has cyclic support, but our rules cannot capture this notion. The rule given in Figure 3 fills this gap and makes use of an anti-sequent calculus, cf., Section 2 for details.

Proposition 6. Given a theory Γ, S ⊆ Var(Γ) and S = Var(Γ) \ S. If (a) Γ ∣≈ ∧ S ∪ ¬S and (b) Γ, ¬¬S, ¬S ̸|=HT ∧p∈S p ∨ ¬p, then Γ ∣≈ ∆ for every ∆.

Proof. Towards a contradiction, suppose there is some equilibrium model I of Γ. Now, from (a) it follows that I = S and from (b) we obtain that there is some ⟨J ′ , I ′ ⟩ |= Γ where I ′ = S = I and ⟨J ′ , I ′ ⟩ ̸|= p ∨ ¬p for some p ∈ S. The latter implies p ̸∈ J ′ and thus J ′ ⊂ S which in turn implies that I cannot be an equilibrium model of Γ.

The intuition is that the left premises ensures that whenever Γ has an equilibriummodel that model is S. The refutation in the right-premise gives us that S is a classical model but unstable and Γ has thus no equilibrium models.

Proposition 6 is also closely related to the concept of safe beliefs [Osorio et al., 2005], which coincide with equilibrium models and are defined in a similar fashion.

Example 4. Consider the theory Γ1 = {a ⊃ b, b ⊃ a} which has the empty set as its sole equilibrium model. Clearly, Γ1 ∣≈ ¬a holds and Figure 4 shows the corresponding proof.

Definition 6. The sequent calculus ELK is defined by the initial sequents given in Definition 4, the basic rules in Figure 2, the (RCut)-rule, and the (⊣)-rule.

The introduced rules constitute our sequent calculus ELK.

Theorem 1. The sequent calculus ELK is sound, i.e., if Γ ∣∼ ∆ is derivable in ELK, then Γ ∣≈ ∆ holds.

Having established soundness, it remains to show that the calculus is complete. First, introduce the notion of consistency as well as some properties of the calculus.

Definition 7. Γ is equilibrium inconsistent whenever Γ ∣∼ ⊥ can be derived, in ELK and equilibrium consistent otherwise.

We drop "equilibrium" here whenever clear from context.

Proposition 7. Γ ∣∼ φ can be derived iff Γ ∪ {¬φ} is inconsistent.

Proof. Suppose Γ ∣∼ φ can be derived, by application of the rule (¬l) we can derive Γ, ¬φ ∣∼ and thus Γ, ¬φ ∣∼ ⊥ using (wr). With Γ, ¬φ ∣∼ ⊥ we can derive Γ ∣∼ φ as follows:

Figure 3: Refutation-based rule in the sequent calculus

Figure 4: Partial derivation of a ⊃ b, b ⊃ a ∣∼ ¬a

Proposition 8. If Γ ∣∼ φ can be derived and ¬φ ∈ Γ, then Γ is inconsistent.

Proof. Suppose Γ ∣∼ φ can be derived and ¬φ ∈ Γ, then by application of the rules (¬l) and (wr) we can derive Γ, ¬φ ∣∼ ⊥ and since by definition the sides of equilibrium sequents are sets, we obtain Γ ∣∼ ⊥.

Proposition 9. If φ ∈ Γ and ¬φ ∈ Γ, then Γ is inconsistent.

Proof. If φ ∈ Γ, then Γ ∣∼ φ is an initial sequent and Γ is thus inconsistent by Proposition 8.

Proposition 10. If Γ ∪ {φ} and Γ ∪ {¬φ} are inconsistent, then Γ is inconsistent as well.

Proof. If Γ, φ ∣∼ ⊥ and Γ, ¬φ ∣∼ ⊥ can be derived, we can derive Γ ∣∼ ⊥ as follows:

Our completeness proof will follow the well-known Lindenbaum approach also used in classical logic. Hence, we must define what we understand by a complete theory.

Definition 8. A theory Γ is complete iff for every formula φ, either ¬¬φ ∈ Γ or ¬φ ∈ Γ.

Different from classical logic, we do not require that each formula occurs either positively or negatively and rather that the negation or the double negation is contained. This is due to the fact that equilibrium logic is not cumulative, i.e., adding positive formulas can induce new equilibrium models. However, as the next results show, this is not the case for negated or double negated formulas.

Lemma 1. If I is an equilibrium model of Γ and I |= φ, then I is an equilibrium model of Γ ∪ {φ}.

Proof. Suppose I is not an equilibrium model of Γ ∪ {φ}. It is is clearly a classical model, as I |= Γ follows from it being an equilibrium model of Γ and I |= φ. Hence, there is some J ⊂ I such that ⟨J, I⟩ |= Γ ∪ {φ}. The latter implies ⟨J, I⟩ |= Γ, so I is not an equilibriummodel of Γ.

Lemma 2. If I |= ¬φ, then I is an equilibrium model of Γ iff it is an equilibrium model of Γ ∪ {¬φ}.

Proof. The left-to-right direction, follows from Lemma 1 and I |= ¬φ. Remains to show the other direction. Towards a contradiction, suppose I is not an equilibrium model of Γ. Since it is a classical model, there has to be some J ⊂ I such that ⟨J, I⟩ |= Γ. However, I |= ¬φ implies ⟨J, I⟩ |= ¬φ. Hence, ⟨J, I⟩ |= Γ ∪ {¬φ} holds contradicting that I is an equilibrium model of Γ ∪ {¬φ}.

Lemma 3. If I |= φ, then I is an equilibriummodel of Γ iff it is an equilibrium model of Γ ∪ {¬¬φ}.

Establishing that every complete theory has some classical model works similarly to the classical case and leads to the following lemma.

Lemma 4. Given a complete theory Γ, if Γ is consistent, then there is some interpretation I such that I |= Γ.

Furthermore, the classical model is unique.

Lemma 5. Given a complete theory Γ. Whenever ⟨J, I⟩ |= Γ and ⟨J ′ , I ′ ⟩ |= Γ, then I = I ′ .

Proof. Suppose ⟨J, I⟩ |= Γ and ⟨J ′ , I ′ ⟩ |= Γ. We show I ⊆ I ′ . Let p be an arbitrary element of I. Since Γ is complete, either ¬¬p ∈ Γ or ¬p ∈ Γ. Now, if ¬p ∈ Γ, then ⟨J, I⟩ |= ¬p holds, which implies I |= ¬p and thus p ̸∈ I. So, suppose ¬¬p ∈ Γ and thus ⟨J ′ , I ′ ⟩ |= ¬¬p which implies I ′ |= ¬¬p. Hence, p ∈ I ′ . The statement I ′ ⊆ I can be shown mutatis mutandis and thus I = I ′ .

Of course, having a classical model is not enough in our case. We also need the following lemma, which shows that our calculus enforces stability.

Lemma 6. Given a complete theory Γ. If ⟨J, I⟩ |= Γ where J ⊂ I, then Γ is inconsistent.

Proof. Let S = I and S = Var(Γ) \ S. Since Γ is complete, ¬p ∈ Γ for every p ∈ S and we can thus derive Γ ∣∼ ¬p as it is an initial sequent. Similarly, ¬¬p ∈ Γ for every p ∈ S and we can derive Γ ∣∼ p by applications of the (¬l) and (¬r) rules. Hence, Γ ∣∼ ∧ S ∪ ¬S can be derived through (∧r). Furthermore, S = I, ⟨J, I⟩ |= Γ, p ∈ I \ J and p ∈ S imply Γ, ¬¬S, ¬S ̸|=HT ∧p∈S p ∨ ¬p. Hence, Γ ∣∼ ⊥ follows from the (⊣)-rule and the completeness of the HT anti-sequent calculus.

Finally, we can state the following which follows immediately from the lemmas above.

Corollary 1. Given a complete theory Γ, if Γ is consistent, then it has an equilibrium model.

Now, having the tools in place, we come to the actual Lindenbaum-like construction. First, another helpful lemma.

Lemma 7. Given a consistent theory Γ, if Γ ∣∼ φ can be derived, then Γ ∪ {φ} is consistent.

Proof. Suppose Γ ∣∼ φ can be derived, then by Proposition 7, Γ∪{¬φ} is inconsistent. Towards a contradiction, assume Γ∪ {φ} is inconsistent. Then by Proposition 10, Γ is inconsistent.

Proposition 11. Given a consistent theory Γ there exists Γ∗ ⊇ Γ which is consistent and complete.

Proof. Let φ0, . . . , φn be an enumeration of all formulas in the language. We define Γ0 = Γ and

Γ0 is consistent by assumption. Suppose Γi+1 = Γi∪{¬¬φi}, then Γi+1 is consistent by construction. Now, if Γi+1 = Γi ∪ {¬φi} then Γi ∪ {¬¬φi} is inconsistent and therefore, by Proposition 7, Γ ∣∼ ¬φ can be derived. By Lemma 7, the latter and Γi being consistent imply Γi ∪ {¬φi} = Γi+1 is consistent. Hence, Γ∗ = ⋃1≤i≤n Γi is consistent.

By construction, Γ∗ is complete as every formula φi appears in the enumeration and either ¬¬φi of ¬φi gets added.

The completeness of the calculus now follows easily.

Theorem 2. If Γ ∣≈ φ, then Γ ∣∼ φ is derivable in ELK.

Proof. We proceed by contraposition. Suppose Γ ∣∼ φ cannot be derived. By Proposition 7 it holds that Γ ∪ {¬φ} is consistent. Hence, it has some complete extension which has an equilibrium model I such that I |= ¬φ. By Lemmas 2 and 3, I is also an equilibrium model of Γ and I |= ¬φ clearly implies I ̸|= φ. Hence, Γ ̸∣≈ φ holds by definition.

The sequent calculus ELK thus satisfies the following.

Corollary 2 (Main Result). The sequent calculus ELK is sound and complete.

5 Discussion

Alternative Characterisation. Naturally, one might wonder whether there is a way to replace the (⊣)-rule and ideally with a rule that does not rely on a separate refutation calculus.

The entailment in Example 4 is shown in the MLK sequent calculus for circumscription [Olivetti, 1992] using the weak monotonicity rule; the encoded property of inference is also known as cautious monotonicity (CM). It is well-known that answer set entailment does not satisfy it in general, but in a restricted syntactic fragment.

In the following, we call a theory nested if it contains nested implication, i.e., an implication φ ⊃ ψ where either φ or ψ contains an implication as a subformula, and negation ¬χ is interpreted as χ ⊃ ⊥ and thus counts as an implication as well.

With this in place, we can introduce the following rule.

This rule is sound for equilibrium entailment.

Proposition 12. Given a theory Γ that is not nested, if Γ ∣≈ ∆ and Γ ∣≈ φ hold, then so does Γ, φ ∣≈ ∆.

The proof follows from the fact that for non-nested theories, minimal models and equilibrium models coincide.

Furthermore, consider the following rule, where ⊢HT denotes an HT sequent calculus, e.g. the one given by Mints [2010], and let ↔ denote biimplication.

Intuitively, the rule states that HT-equivalent subformulas are interchangeable, which is a well-known property of equilibrium logic [Lifschitz et al., 2001].

Using the two rules, we obtain the following result.

Theorem 3. Let ELK′ denote the calculus of initial sequents fromDefinition 4, the rules in Figure 2, (RCut), (RCM), and (LLE). Then, Γ ∣≈ φ iff Γ ∣∼ φ is derivable in ELK′ .

The basic idea is that for each complete theory, there is an HT-equivalent theory which consists of a non-nested part and negated or double-negated atoms.

Hence, (RCM) and (LLE) replace the (⊣)-rule, but has rather drastic syntactic side conditions and we have to utilize an HT sequent calculus.

ASP Fragment. Given that part of our motivation for this work is to provide a proof system for ASP, it is natural to ask how our calculus behaves on this fragment of EL. Recall that programs are theories where every formula is an implication l1 ∧ · · · ∧ lm ⊃ lm+1 ∨ · · · ∨ ln and all li are literals.

We have already seen in Example 4 that even for programs, the (⊣) rule may be needed to derive certain consequences. However, as we show there is an important class of programs for which this is not the case. In fact, not even the (RCut) rule is needed for it. The class in question is the one of tight programs which are defined as follows. A program is tight [Erdem and Lifschitz, 2003] if there is no loop in its dependency graph, which is constructed over all atoms by adding an edge from p to q for each positive literals p and q in the antecedent and the consequent of a rule, respectively. 1

The intuition is that for tight programs, the (⊃l)-rule becomes invertible, as the next result shows, which is not the case in general.

Proposition 13. If Γ, φ ⊃ ψ ∣≈ ∆ is satisfied, where Γ is a tight program, then Γ, ψ ∣≈ ∆, ¬φ and Γ ∣≈ ∆, φ.

Using this proposition, the following can be shown.

Theorem 4. Given tight ASP program Γ and ∆ in negation normal form, then Γ ∣≈ ∆ holds iff Γ ∣∼ ∆ can be derived using the basic rules in Figure 2, and initial sequents from Definition 4.

Proof (Sketch). It can be seen that for programs only the (∧l), (∨l), (¬l) and (⊃l) rules are ever required for the left-hand side of the sequent. Furthermore, for tight programs, the (⊃l) rule is invertible by Proposition 13. The rules (∧l) and (¬l) are in invertible in general already. On the left-hand sides we now only have sets of clauses and the selection of the branches for the (∨)l rule is guided by which literal satisfies the most clauses. Furthermore, by deriving the rules only after their bodies have been added to the left, also the sometimes required (¬r)-rule becomes invertible.

We thus always have leaves Γ′ ∣∼ ∆′ where Γ′ is a set of atoms and ∆′ is a set of literals and if Γ ∣≈ ∆ holds then the sequents in the leaves have to be axioms due to invertibility.

Given that for tight programs, answer sets and so-called supported models coincide [Erdem and Lifschitz, 2003], Theorem 4 implies that the rules given in Figure 2 axiomatise the inference over such models. This further suggests that in the full calculus, the (⊣) rule is required to exclude supported models which include unfounded sets [Leone et al., 1997], i.e., atoms which are deemed true but only have cyclic support.

The observation above also gives rise to a general proof strategy when dealing with programs. First, one should apply the (⊃l)-rule on parts of the program which are locally tight, i.e., the dependency graph of that program module is non-cyclic, leaving the (⊣)-rule to potentially handle remaining loops. Due to space restrictions we cannot go into more details, but proof strategies also arise by utilisation of splitting sets [Lifschitz and Turner, 1994].

Explanations. We argued in Section 3 that equilibrium entailment provides a useful framework for explanations in equilibrium logic and thus ASP, and our calculus gives insight into why such an entailment is valid. We do not claim that proofs in the sequent calculus are already accessible explanations, but as we will discuss, they serve as an overarching theoretical framework from which explanations can be derived. To that end we can also introduce derived rules, which may be less general but help shorten proofs. For example, we use the following rule, which essentially encodes modus ponens and we will see later that this rule is very useful when one considers ASP programs.

1 Tight programs are usually considered to have no negative literals in rule heads. However, relevant concepts, like supporting rules, carry over to the more general case.

In Example 3, we have already seen how the calculus shows why a theory is inconsistent. In that proof, we see that since ¬p holds by default and p entails p, ¬p ⊃ p cannot have any equilibrium models.

Let us consider some more examples with theories that essentially represent ASP programs.

Example 5. Consider Γ1 = {¬c ⊃ (a ∨ b), ¬(a ∧ d), ¬b, d}. The atom d can be seen as the input data and the remaining formulas encode a choice between a and b given ¬c and some constraints. It holds that Γ1 ∣≈ ⊥, i.e., has no equilibrium models which we can prove as shown in Figure 5.

Let us verbalise the steps of the proof bottom up. First, we select ¬c ⊃ (a ∨ b) and detach the implication with the (⊃l)-rule. In the right branch, we now need to show that ¬c follows. After two applications of (¬l) we only have atoms on the left and have an axiom. On the left branch, we have added a ∨ b on the left and proceed by case distinction through the (∨l)-rule.

In the branch where a is now on the left, we also have d. We can apply (¬l) to ¬(a ∧ d) and get a ∧ d on the right. The latter can be split with the (∧r)-rule and since both a and d were already on the left, we have two axioms. Otherwise, if b holds, then this clashes with ¬b which is shown the same as for the other branch.

As we have seen in the example, a proof in the sequent calculus which is summarised and, put into natural language, can serve as an explanation.

Let us now turn to an example where we have a theory and one of its equilibriummodels.

Example 6. Let Γ2 = {¬a ⊃ b, ¬b ⊃ a, a ⊃ c} and consider its equilibrium model I = {a, c}. Suppose we seek to explain why c is in the model. A minimal assumption set w.r.t. I, cf. Section 3, is {b} and we give the following sequent proof:

The proof can be summarised as follows. We look at the implication ¬b ⊃ a. Since ¬b is in the theory, we can apply the modus ponens rule (MP) from above. With a in the theory, we can again use (MP) on a ⊃ c. Given that c is now on the left and right, we have an axiom.

So far we have only used the rules from ELK and (MP). However, one might introduce further derived rules and use them in explanations. A rule akin to Proposition 2 comes to mind. Furthermore, in a potential explanation system, lemmas might be reused using the (RCut)-rule, shortening the proofs.

6 RelatedWork

To the best of our knowledge, no sequent calculus for equilibrium logic has been given in the literature. Pearce et al. [2000] introduced a tableau system for equilibrium logic. Their approach works in several stages. In the first stage, a dedicated

Figure 5: Derivation for Example 5

calculus for total HT models is used to enumerate all models. With another dedicated calculus, those total models are then checked for stability in the second stage. Finally, in the last stage, it is checked via tableaux whether the given formula holds in the previously obtained total and stable models. Hence, due to the required enumeration and multi-stage concept, this calculus does not fully satisfy requirements (R1) and (R3) introduced in Section 1.

Several proof systems have been studied directly for ASP. Bonatti [2001] introduced a resolution calculus for answer set entailment and provided another calculus for brave entailment [Bonatti et al., 2008]. The latter is different from the notion of entailment we study in the sense that the consequence does not need to hold in all models but rather in at least one. The calculi differ from their classical counterparts and operate on pairs of sets of literals and suffer from some drawbacks: they support only normal logic programs and rely on a rather complicated notion of counter-supports which is not axiomatised by the calculus but computed externally. The calculi are thus weak on requirements (R1-R3).

Gebser and Schaub [2013] presented a tableau calculus which is aimed at axiomatising satisfiability and how solvers obtain their solutions and thus differs in motivation from our work. However, it can also be used for answer set entailment by translation of the entailment into an inconsistent program. While their calculus supports a large number of advanced ASP language features like disjunction and weight constraints, it does not cover arbitrary nested formulas like our calculus does. Furthermore, some rules in their calculus heavily rely on global syntactic notions which only work for programs, which clashes with our requirement (R1).

Proofs for ASP also appear in the context of proof logging that ASP solvers provide to justify whenever they report unsatisfiability [Alviano et al., 2019; Chew et al., 2024]. However, those proofs are generally not geared towards human interpretability but rather verification and are not very concise. Thus, they are violating requirement (R3).

Proof-like systems have been used to provide explanations as to why certain atoms are, or are not, in a given answer set [Pontelli et al., 2009; Alviano et al., 2024]. While the explanations given by those approaches share some similarity with a formal proof, they are not actual complete proof systems and cannot be applied without a model. Furthermore, they are limited to the basic ASP language.

Similarly, the fix-point characterisation for equilibrium logic [Pearce, 2006] does not axiomatise the inference relation over equilibrium models, but rather only provides a definition of stable models via HT entailment and model selection. The characterisation can be used in conjunction with an HT sequent calculus [Mints, 2010] to justify the atoms in an equilibrium model in a proof-theoretic manner. However, this is not the scope of our work.

Finally, we mention some inspiring related sequent calculi that axiomatise other nonmonotonic formalism, viz. the one by Olivetti [1992] for propositional circumscription, which is also two-sided, and those by Bonatti and Olivetti for Circumscription [Bonatti and Olivetti, 1997b] and Default Logic [Bonatti and Olivetti, 1997a], which also use an anti-sequent calculus.

7 Conclusion

In this work, we have introduced an axiomatisation of answer set entailment in the form of a sequent calculus for equilibrium logic. The calculus was then shown to be sound as well as complete. All rules, except one are natural and structurally simple, the remaining rule utilises an refutation calculus to ensure the stability condition necessary for equilibrium models.

We also discussed an alternative to this refutation rule which is based on cautious monotonicity. However, this property only holds for a syntactic fragment of the logic that includes positive ASP programs. However, it is unlikely that there is an axiomatisation which operates on purely standard rules. We further showed how answer set entailment can serve as a framework for explainability and how our calculus can in turn justify why an entailment holds.

For future work, we plan to further explore the use of proofbased explanations for ASP, for example, by studying translations of proofs into natural language including proof search and human-friendly presentation of proofs, or investigating contrastive explanations. Extensions of the calculus to cover more general versions of equilibrium logic, which encompass programs with variables [Pearce and Valverde, 2008] or linear constraints [Cabalar et al., 2016] are also of interest.

Acknowledgments

Tobias Geibinger is a recipient of a DOC Fellowship of the Austrian Academy of Sciences at the Institute of Logic and Computation at the TUWien.

This work has benefited from the European Union's Horizon 2020 research and innovation programme under grant agreement No 101034440 (LogiCS@TUWien).

In addition, this research was funded in part by the Austrian Science Fund (FWF) [10.55776/COE12].

Furthermore, we thank Agata Ciabattoni, Matteo Tesi, David Pearce and Hans Tompits for the helpful discussions on the topic.