Inconsistency Proofs for ASP: The ASP-DRUPE Format

TL;DR

This paper introduces ASP-DRUPE, a new proof format for verifying inconsistency in Answer Set Programming, based on RUP, with correctness proof and implementation in the wasp solver.

Contribution

It develops ASP-DRUPE, a novel proof format for ASP inconsistency, adapting RUP for logic programs, and demonstrates its integration and correctness.

Findings

ASP-DRUPE is correct and sound.

Implemented in the wasp solver.

Facilitates formal verification of ASP inconsistency.

Abstract

Answer Set Programming (ASP) solvers are highly-tuned and complex procedures that implicitly solve the consistency problem, i.e., deciding whether a logic program admits an answer set. Verifying whether a claimed answer set is formally a correct answer set of the program can be decided in polynomial time for (normal) programs. However, it is far from immediate to verify whether a program that is claimed to be inconsistent, indeed does not admit any answer sets. In this paper, we address this problem and develop the new proof format ASP-DRUPE for propositional, disjunctive logic programs, including weight and choice rules. ASP-DRUPE is based on the Reverse Unit Propagation (RUP) format designed for Boolean satisfiability. We establish correctness of ASP-DRUPE and discuss how to integrate it into modern ASP solvers. Later, we provide an implementation of ASP-DRUPE into the wasp solver for normal logic programs. This work is under consideration for acceptance in TPLP.

Equations

$${\Delta }_P^{\text{Bdef}}:=$$

$${\Delta }_P^{\to }:=$$

$${\nabla }_0(\Pi )$$

$${\nabla }_i(\Pi )$$

$${\sigma }_1$$

$${\sigma }_2$$

$${\sigma }_3$$

$${\sigma }_4$$

$${\sigma }_5$$

$${\sigma }_6$$

$${\sigma }_7$$

$${\sigma }_8$$

$${\sigma }_9$$

$${\sigma }_{10}$$

$${\sigma }_{11}$$

$${\sigma }_{12}$$

$${\sigma }_{13}$$

$${\sigma }_{14}$$

$${\sigma }_{15}$$

$${\sigma }_{16}$$

$${\sigma }_{17}$$

$${\sigma }_{18}$$

$$\mathsf{tv}(l)$$

$$\mathsf{smod}({\sigma }_i)$$

Full text

1 Introduction

Answer Set Programming (ASP) [Brewka et al. (2011)] is a logic-based declarative modeling language and problem solving framework [Gebser et al. (2012)] for hard computational problems and an active research area in artificial intelligence (AI) and knowledge representation and reasoning. It has been applied both in academia [Balduccini et al. (2006), Gebser et al. (2010), Gebser et al. (2011)] and industry [Gebser et al. (2011), Guziolowski et al. (2013), Ricca et al. (2012)]. In propositional ASP questions are encoded by atoms combined into rules and constraints which form a logic program. Solutions to the program consist of sets of atoms called answer sets; if no solutions exist then the program is inconsistent.

Knowledge representation languages like ASP are usually considered explainable AI, as they are based on deduction, which is an explainable procedure. For example, we can easily explain answer sets of a normal logic program in terms of program reducts and fixpoint operators [Liu et al. (2010)]. In this case, we may argue that answer sets are self-explanatory, and therefore ASP systems providing answer sets are explainable AI systems. However, modern ASP systems do not provide any explanation for inconsistent programs; there is no witness that can be checked or evidence of the correctness of the refutation of the input program. Hence, even if inconsistency of logic programs is anyhow explainable with mathematical rigour, ASP systems are essentially black-boxes in this case, and just report the absence of answer sets. We believe that adding inconsistency proofs in ASP systems is important to make them explainable for inconsistent programs, but also provides auditability for consistent programs. Thanks to a duality result in the literature [Pearce (1999)], such inconsistency proofs for ASP can be also used as a certificate for the validity of some formulas of intuitionistic logic and other intermediate logics. A further application of these inconsistency proofs is query answering in ASP, which is usually achieved by inconsistency checks. There, the goal is to provide a witness for cautiously true answers of a given query.

Modern ASP solvers have been highly influenced by SAT solvers, which solve the Boolean satisfiability problem and are often based on conflict-driven clause learning [Silva and Sakallah (1999)]. Typically, ASP solvers aim for computing an answer set of a given program, and therefore solve the consistency problem that asks whether a given program has an answer set. This problem is on the second level of the polynomial hierarchy when allowing arbitrary propositional disjunctive programs as input and on the first level when restricting to disjunction-free programs [Truszczyński (2011)]. As already stated, while consistency of a program can be easily verified given such a computed answer set, verifying whether a solver correctly outputted that a program is inconsistent, is not immediate. Given that ASP solvers are also used for critical applications [Gebser et al. (2018), Haubelt et al. (2018)], their correctness is of utter importance.

When looking at SAT solvers, various techniques have been developed to ensure correctness of unsatisfiability, such as clausal proof variants [Gelder (2008), Goldberg and Novikov (2003)] based on clauses that have RUP (reverse unit propagation) and RAT (Resolution Asymmetric Tautology) property. These proof formats share verifiability in polynomial time in the size of the proof and input formula and can be tightly coupled with modern solving techniques. A solver outputs such a proof during solving. Thereby, the correctness of solving can be verified by a relatively simple method for every input instance. While there are variants of these proofs for various problems, such as extensions to verify the validity of quantified Boolean formulas [Heule et al. (2013), Wetzler et al. (2014)] (QRAT [Heule et al. (2014)] and QRAT+ [Lonsing and Egly (2018)]), to our knowledge such a format is not yet available for verifying ASP solvers.

One approach to certify inconsistency of a given normal program is to translate the program into a SAT formula in polynomial time [Lin and Zhao (2003), Janhunen (2006)] and obtain a proof from a SAT solver, e.g., via a RAT-based proof format, to verify that indeed the program is inconsistent. Unfortunately, this approach does not take the techniques into account that are employed by state-of-the-art ASP solvers and therefore seem to lack efficiency and scalability. Further, this is still not a suitable technique for disjunctive programs, nor to verify whether internally the ASP solver is able to correctly explain the obtained result.

We follow this line of research and establish the following novel results for ASP:

We present the proof format ASP-DRUPE based on RUP for logic programs given in SModels [Syrjänen (2000)] or ASPIF [Gebser et al. (2016)] (restricted to ASP without theory reasoning) input format including disjunctive programs and show its correctness. 2. 2.

We provide an algorithm for verifying that a given solving trace in the ASP-DRUPE format is indeed a valid proof for inconsistency of the input program. This algorithm works in polynomial time in the size of the given solving trace. 3. 3.

We illustrate on an abstract ASP solving algorithm how one can integrate ASP-DRUPE into state-of-the-art ASP solvers like clasp [Gebser et al. (2012)] and wasp [Alviano et al. (2015)]. 4. 4.

We provide an implementation in a variant of wasp, where ASP-DRUPE is integrated for normal ASP. This variant of wasp is able to not only explain inconsistency for inconsistent logic programs, but also provides auditability in case of consistency for verifying whether the provided answer set was indeed correctly obtained.

Related Work.

Heule et al. [Heule et al. (2013)] presented a proof format based on the RAT property and subsequently a program to validate solving traces in this format [Wetzler et al. (2014)]. Extended resolution allows to polynomially simulate the DRAT format [Kiesl et al. (2018)] and vice-versa [Wetzler et al. (2014)]. Many advanced techniques, such as XOR reasoning [Philipp and Rebola-Pardo (2016)] as well as symmetry breaking [Heule et al. (2015)] can be expressed in DRAT and efficient, verified checkers based on RAT have been developed [Cruz-Filipe et al. (2017)]. Further, RAT is also available for QBF [Heule et al. (2014)] and has been extended to cover a more powerful redundancy property [Lonsing and Egly (2018)].

2 Preliminaries

2.1 Answer Set Programming (ASP)

We follow standard definitions of propositional ASP [Brewka et al. (2011)] and use rules defined by the SModels [Syrjänen (2000)] or ASPIF [Gebser et al. (2016)] (restricted to ASP without theory reasoning) input format, which is widely supported by modern ASP solvers. In particular, let $\ell$, $m$, $n$ be non-negative integers such that $1\leq\ell\leq m\leq n$, $a_{1}$, $\ldots$, $a_{n}$ propositional atoms, $w$, $w_{1}$, $\ldots$, $w_{n}$ non-negative integers. A choice rule is an expression of the form $\{a_{1};\ldots;a_{\ell}\}\leftarrow\,a_{\ell+1},\ldots,a_{m},{\sim}a_{m+1},\ldots,{\sim}a_{n}$, a disjunctive rule is of the form $a_{1}\vee\cdots\vee a_{\ell}\leftarrow\,a_{\ell+1},\ldots,a_{m},{\sim}a_{m+1},$ $\ldots,{\sim}a_{n}$, and a weight rule is of the form $a_{\ell}\leftarrow\,w\leqslant\{a_{\ell+1}=w_{\ell+1},\ldots,a_{m}=w_{m},\,{\sim}a_{m+1}=w_{m+1},\ldots,{\sim}a_{n}=w_{n}\}$, where $\ell=1$. A rule is either a disjunctive, a choice, or a weight rule. A (disjunctive logic) program $P$ is a finite set of rules. For a rule $r$, we let $H_{r}\,\mathrel{\mathop{:}}=\{a_{1},\ldots,a_{\ell}\}$, $B^{+}_{r}\,\mathrel{\mathop{:}}=\{a_{\ell+1},\ldots,a_{m}\}$, $B^{-}_{r}\,\mathrel{\mathop{:}}=\{a_{m+1},\ldots,a_{n}\}$, and $B_{r}\,\mathrel{\mathop{:}}=B^{+}_{r}\cup\{{\sim}a\mid a\in B^{-}_{r}\}$ is a set of literals, i.e., an atom or the negation thereof. We denote the sets of atoms occurring in a rule $r$ or in a program $P$ by $\and(r)\,\mathrel{\mathop{:}}=H_{r}\cup B^{+}_{r}\cup B^{-}_{r}$ and $\and(P)\,\mathrel{\mathop{:}}=\bigcup_{r\in P}\and(r)$. For a weight rule $r$, let $\operatorname{wght}(r,l)$ map literal $l$ to its weight $w_{i}$ in rule $r$ if $l=a_{i}$ for $\ell+1\leq i\leq m$, or if $l={\sim}a_{i}$ for $m+1\leq i\leq n$, and to [math] otherwise. Further, let $\operatorname{wght}(r,L)\,\mathrel{\mathop{:}}=\Sigma_{l\in L}\operatorname{wght}(r,l)$ for a set $L$ of literals and let $\operatorname{bnd}(r)\,\mathrel{\mathop{:}}=w$ be its bound. A normal (logic) program $P$ is a disjunctive program $P$ with $\left|H_{r}\right|\leq 1$ for every $r\in P$. The positive dependency digraph $D_{P}$ of $P$ is the digraph defined on the set $\{a\mid a\in H_{r}\cup B^{+}_{r},r\in P\}$ of atoms, where for every rule $r\in P$ two atoms $a\in B^{+}_{r}$ and $b\in H_{r}$ are joined by an edge $(a,b)$. We denote the set of all cycles (loops) in $D_{P}$ by $\mathsf{loop}(P)$. A program $P$ is called tight, if $\mathsf{loop}(P)=\emptyset$. While we allow programs with loops that might also involve atoms of weight rules, we consider weight rules only as a compact representation of a set of normal rules, similar to the definition of stable models in related work [Bomanson et al. (2016)]. In other words, we do not consider advanced semantics concerning recursive weight rules (recursive aggregates). In case of solvers with different semantics, one can restrict the input language to disregard recursive weight rules, which is also in accordance with the latest ASP-Core-2.03c standard [Calimeri et al. (2015)]. This restriction is motivated by a lack of consensus on the interpretation of recursive weight rules [Ferraris (2011), Faber et al. (2011), Gelfond and Zhang (2014), Pelov et al. (2007), Son and Pontelli (2007)].

2.2 Solving Logic Programs

Let $P$ be a given program, $r\in P$ be a rule, and $a\in\and(P)$. We define the set $\mathsf{IB}(r,a)$ of induced bodies with $a$ in the head by the singleton $\{B_{r}\mid a\in H_{r}\}$ if $r$ is a choice rule, by $\{B_{r}\cup\{{\sim}b\mid b\in H_{r}\setminus\{a\}\}\mid a\in H_{r}\}$ if $r$ is a disjunctive rule, and by the union over $\{\{A\cap B^{+}_{r}\}\cup\{{\sim}b\mid b\in A\cap B_{r}^{-}\}\mid a\in H_{r}\}$ for every (subset-minimal) set $L$ of literals such that $\operatorname{wght}(r,L)\geq\operatorname{bnd}(r)$, if $r$ is a weight rule. This allows us to define $\mathsf{IB}(P,a)\,\mathrel{\mathop{:}}=\bigcup_{r\in P,a\in H_{r}}\mathsf{IB}(r,a)$, and $\mathtt{Bod}(P)\,\mathrel{\mathop{:}}=\bigcup_{a\in\and(P)}\mathsf{IB}(P,a)$. A variable assignment is either $\mathbf{T}X$ or $\mathbf{F}X$, where variable $X$ is either an atom, or an induced body, or a fresh atom that does not occur in $\and(P)$. For a variable assignment $l$, $\overline{l}$ is the complementary variable assignment of $l$, i.e., $\overline{l}\,\mathrel{\mathop{:}}=\mathbf{F}X$ if $l=\mathbf{T}X$ and $\overline{l}\,\mathrel{\mathop{:}}=\mathbf{T}X$ if $l=\mathbf{F}X$. An assignment $A$ is a set of variable assignments, where $A^{\mathbf{T}}\,\mathrel{\mathop{:}}=\{X\mid\mathbf{T}X\in A\}$, $A^{\mathbf{F}}\,\mathrel{\mathop{:}}=\{X\mid\mathbf{F}X\in A\}$, and $\overline{A}\,\mathrel{\mathop{:}}=\{\overline{l}\mid l\in A\}$ such that $A^{\mathbf{T}}\cap A^{\mathbf{F}}=\emptyset$. For a set $B$ of literals, we define the induced assignment $\mathsf{IAss}(P,B)\,\mathrel{\mathop{:}}=\{\mathbf{T}a\mid a\in\and(P)\cap B\}\cup\{\mathbf{F}a\mid{\sim}a\in B\}$. A nogood $\delta$ is an assignment, which is not allowed, where $\Box\,\mathrel{\mathop{:}}=\emptyset$ refers to the empty nogood. Given a set $\Delta$ of nogoods. We define the least fixpoint $\Delta_{\mathrel{|}\joinrel\mkern-0.5mu\mathrel{-}_{1}}$ of unit propagated nogoods by the fixpoint computation $\Delta_{\mathrel{|}\joinrel\mkern-0.5mu\mathrel{-}_{1}}^{0}\,\mathrel{\mathop{:}}=\Delta$, and $\Delta_{\mathrel{|}\joinrel\mkern-0.5mu\mathrel{-}_{1}}^{i}\,\mathrel{\mathop{:}}=\Delta_{\mathrel{|}\joinrel\mkern-0.5mu\mathrel{-}_{1}}^{i-1}\cup\{\delta\setminus\{l\}\mid\delta\in\Delta_{\mathrel{|}\joinrel\mkern-0.5mu\mathrel{-}_{1}}^{i-1},l\in\delta,\{\overline{l}\}\in\Delta_{\mathrel{|}\joinrel\mkern-0.5mu\mathrel{-}_{1}}^{i-1}\}$ for $i\geq 1$. Nogood $\delta$ is a consequence using unit propagation (UP) of set $\Delta$, denoted by $\Delta\mathrel{|}\joinrel\mkern-0.5mu\mathrel{-}_{1}\delta$, if $\delta\in\Delta_{\mathrel{|}\joinrel\mkern-0.5mu\mathrel{-}_{1}}$. An assignment $A$ satisfies a set $\Delta$ of nogoods (written $A\models\Delta$) if for every $\delta\in\Delta$, we have ${\delta}\not\subseteq A$. Set $\Gamma$ of nogoods is a consequence of a set $\Delta$ of nogoods (denoted by $\Delta\models\Gamma$) if every assignment, which contains a variable assignment for all variables in $\Delta\cup\Gamma$, that satisfies $\Delta$ also satisfies $\Gamma$. The set $\Delta_{P}$ of completion nogoods [Clark (1977), Gebser et al. (2012)] is defined by $\Delta_{P}\,\mathrel{\mathop{:}}=\Delta_{P}^{\text{Bdef}}\cup\Delta_{P}^{\rightarrow}\cup\Delta_{P}^{\leftarrow}$, where

[TABLE]

Note that in practice, current ASP solvers do not fully compute $\Delta_{P}$. Instead, these solvers partially compute $\Delta_{P}$ and add relevant nogoods lazily during solving [Alviano et al. (2018)].

Then, if $P$ is tight the set $A^{\mathbf{T}}\cap\and(P)$ is an answer-set if and only if there is a satisfying assignment $A$ for $\Delta_{P}$ [Fages (1994), Gebser et al. (2012)]. The set $\mathsf{EB}(P,U)$ of external bodies of program $P$ and set $U\subseteq\and(P)$ of atoms are given by $\mathsf{EB}(P,U)\,\mathrel{\mathop{:}}=\{B\mid B\in\mathsf{IB}(P,a),B\cap U=\emptyset,a\in U\}$ [Gebser et al. (2012)]. We define the loop nogood $\lambda(a,U)$ for an atom $a\in U$ on a loop $U\in\mathsf{loop}(P)$ by $\lambda(a,U)\,\mathrel{\mathop{:}}=\{\mathbf{T}a\}\cup\{\mathbf{F}B\mid B\in\mathsf{EB}(P,U)\}$. For a logic program $P$, the set $A^{\mathbf{T}}\cap\and(P)$ is an answer set if and only if there is a satisfying assignment $A$ for $\Delta_{P}\cup\Lambda_{P}$, where $\Lambda_{P}\,\mathrel{\mathop{:}}=\{\lambda(a,U)\mid a\in U,U\in\mathsf{loop}(P)\}$ [Lin and Zhao (2003), Faber (2005)].

3 ASP-DRUPE: RUP-like Format for Proof Logging

Inspired by RUP-style unsatisfiability proofs in the field of Boolean satisfiability solving [Goldberg and Novikov (2003)], we aim for a proof of inconsistency of a program. Since modern ASP solvers use Clark’s completion [Clark (1977)] to transform a program into a set of nogoods, we do so as well. Our aimed proof then has the following features:

Existence of a simple verification algorithm. In order to increase confidence in the correctness of results, the algorithm that verifies the proof has to be fairly easy to understand and to implement. 2. 2.

Low complexity. The proof is verifiable in polynomial time in its length and the size of the completion nogoods. 3. 3.

Integrability into solvers that employ Conflict-Driven Nogood Learning (CDNL). The proof can stepwise be outputted during solving with minimal impact on the solving algorithm and hence the solver.

The method works as follows: We run the solver on the set $\Delta_{P}$ of completion nogoods for given input program $P$. The solver outputs either an answer set or that $P$ has no answer set and a proof $\Pi$. We pass $P$ together with $\Pi$ to the verifier in order to validate whether the solver’s assessment is in accordance with its outputted proof.

3.1 The Proof Format for Logic Programs

The basic idea of clausal proofs for SAT is the following: One starts with the input formula in CNF (given as a set of clauses). Every step of the proof denotes an addition or deletion of a clause to/from the set of clauses. For additions, the condition is to only add clauses that are a logical consequence of the current set of clauses and that it can be checked easily, e.g., use only unit propagation.

For our format ASP-DRUPE, we consider Clark’s completion $\Delta_{P}$ as the initial set of nogoods corresponding to the input program $P$. Besides addition and deletion of nogoods, we need proof steps that model how the solver excludes unfounded sets (loops).

Example 1

Consider program $P=\{a\leftarrow b,d;\;b\leftarrow a,d;\;a\leftarrow c;\;b\leftarrow c,d;\;c\leftarrow{\sim}d;\;d\leftarrow{\sim}c;\;e\leftarrow c,{\sim}e;\;e\leftarrow{\sim}a,{\sim}e\}$, which is inconsistent. $P$ contains only the positive loop $L=\{a,b\}$, whose external support is given by the set $\{a\leftarrow c;\;b\leftarrow c,d\}$ of rules, and thus $\mathsf{EB}(P,L)=\{\{c\},\{c,d\}\}$. Set $L$ induces two possible loop nogoods, $\lambda(a,L)=\{\mathbf{T}a,\mathbf{F}\{c\},\mathbf{F}\{c,d\}\}$ and $\lambda(b,L)=\{\mathbf{T}b,\mathbf{F}\{c\},\mathbf{F}\{c,d\}\}$.

We describe the proof format ASP-DRUPE for logic programs and adapt the RUP property [Goldberg and Novikov (2003)] to nogoods as follows.

Definition 1** (nogood RUP)**

Let $\Delta$ be a set of nogoods. Then, a nogood $\delta$ is RUP (reverse unit propagable) for $\Delta$ if $\Delta\cup\{\{\overline{l}\}\mid l\in\delta\}\mathrel{|}\joinrel\mkern-0.5mu\mathrel{-}_{1}\Box$, i.e., we can derive $\Box$ using only unit propagation.

A proof step is a triple $(t,\delta,a)$, where $t\in\{\mathsf{a},\mathsf{c},\mathsf{s},\mathsf{e},\mathsf{d},\mathsf{l}\}$ denotes the type of the step, $\delta$ is an assignment, and $a$ is an atom or $\epsilon$. The type $t\in\{\mathsf{a},\mathsf{c},\mathsf{s},\mathsf{e},\mathsf{d},\mathsf{l}\}$ indicates whether the step is an addition ($\mathsf{a}$), a completion rule addition ($\mathsf{c}$), a completion support addition ($\mathsf{s}$), an extension ($\mathsf{e}$), a deletion ($\mathsf{d}$), or a loop addition ($\mathsf{l}$). A proof sequence for a logic program $P$ is a finite sequence $\Pi\,\mathrel{\mathop{:}}=\langle\sigma_{1},\ldots,\sigma_{n}\rangle$ of proof steps. Initially, a proof sequence gets associated with a set $\nabla_{0}(\Pi)\,\mathrel{\mathop{:}}=\Delta_{P}^{\text{Bdef}}$ of nogoods. Note that although the set $\Delta_{P}^{\text{Bdef}}$ might be exponential in the size of the program $P$, body definitions for body variables $B\in\mathtt{Bod}(P)$ that do not occur in the proof are never materialized. Then, each proof step $\sigma_{i}$ for $1\leq i\leq n$ subsequently transforms $\nabla_{i-1}(\Pi)$ into the induced set $\nabla_{i}(\Pi)$ of nogoods, formally defined below. An ASP-DRUPE derivation is a proof sequence that allows for RUP-like rules for ASP and includes both deletion and extension. In an ASP-DRUPE derivation each step $\sigma=(t,\delta,a)$ has to satisfy a condition depending on its type as follows:

An addition $\sigma=(\mathsf{a},\delta,\epsilon)$ inserts a nogood $\delta$ that is RUP for $\nabla_{i-1}(\Pi)$. 2. 2.

A completion rule addition $\sigma=(\mathsf{c},\delta,\epsilon)$ inserts a nogood $\delta\in\Delta_{P}^{\leftarrow}$. 3. 3.

A completion support addition $\sigma=(\mathsf{s},\{\mathbf{F}B_{1},\ldots,\mathbf{F}B_{k}\},a)$ inserts a nogood $\{\mathbf{T}a,\mathbf{F}B_{1},\ldots,$ $\mathbf{F}B_{k}\}\in\Delta_{P}^{\rightarrow}$ if $\{B_{1},\ldots,B_{k}\}=\mathsf{IB}(P,a)$. 4. 4.

An extension $\sigma=(\mathsf{e},\delta,a)$ introduces a definition that renders nogood $\delta$ equivalent to a fresh atom $a$, i.e., $a$ does not appear in $\bigcup_{j=0}^{j=i-1}\nabla_{j}(\Pi)\cup\Delta_{P}$. Formally, this rule represents the set \mathsf{ext}(a,\delta)\,\mathrel{\mathop{:}}=\big{\{}\delta\cup\{\mathbf{F}a\}\big{\}}\cup\big{\{}\{\mathbf{T}a,\overline{l}\}\mid l\in\delta\big{\}} of extension nogoods. 5. 5.

A deletion $\sigma=(\mathsf{d},\delta,\epsilon)$ represents the deletion of $\delta$ from $\nabla_{i-1}(\Pi)$. 6. 6.

A loop addition111There could be an exponential number of external bodies involving weight rules. However, both clasp and wasp treat weight rules differently [Alviano et al. (2015)]. Alternatively, one could easily modify the loop addition type to list also involved external bodies (as in the completion support addition type), which we did not for the sake of readability. $\sigma=(\mathsf{l},\{\mathbf{T}a_{1},\ldots,\mathbf{T}a_{k}\},a_{1})$ inserts a loop nogood $\lambda(a_{1},L)$ for a loop $L=\{a_{1},\ldots,a_{k}\}\in\mathsf{loop}(P)$.

Given an ASP-DRUPE derivation $\Pi=\langle\sigma_{1},\ldots,\sigma_{n}\rangle$, we define the set $\nabla_{i}(\Pi)$ of nogoods induced by step $i$ as the result of applying proof steps $\langle\sigma_{1},\ldots,\sigma_{i}\rangle$ to the initial completion body definitions $\Delta_{P}^{\text{Bdef}}$ for $0\leq i\leq n$. For our inductive definition in the following, we use multiset semantics for additions and deletions of nogoods, and write $\uplus$ for the multiset sum.

[TABLE]

Then, we say that an ASP-DRUPE derivation $\Pi$ is an ASP-DRUPE proof for the inconsistency of $P$ if it actually derives inconsistency for $P$, formally, $\Box\in\nabla_{n}(\Pi)$. Note that $\Delta_{P}^{\text{Bdef}}$ might be exponential in the input program size, in the worst case. However, there is no need to materialize the set $\Delta_{P}^{\text{Bdef}}$, as, intuitively, this set of body definitions only ensures that every induced body has a reserved auxiliary atom that can be used to “address” the body in a compact way. In an actual implementation of a solver that uses ASP-DRUPE, one needs to specify these used auxiliary atoms anyway, cf. Section 5, where implementational specifications of ASP-DRUPE are described.

Example 2

Consider program $P$ from Example 1 and loop $L=\{a,b\}$, which induces loop nogood $\lambda(a,L)=\{\mathbf{T}a,\mathbf{F}\{c\},\mathbf{F}\{c,d\}\}$. Then, the proof sequence $\Pi=\langle\sigma_{1},\ldots,\sigma_{18}\rangle$ is an ASP-DRUPE proof for the inconsistency of $P$ with

[TABLE]

We show that the proof step $\sigma_{7}$ is correct, i.e., that $\{\mathbf{F}\{c\},\mathbf{T}a\}$ is RUP for $\nabla_{6}(\Pi)$. To this end, we need to derive $\Box$ from $\nabla_{6}(\Pi)\cup\{\{\mathbf{T}\{c\}\},\{\mathbf{F}a\}\}$ by unit propagation. With the nogood $\{\mathbf{F}\{c\},\mathbf{T}c\}\in\Delta_{P}^{\text{Bdef}}$, we derive the unit nogood $\{\mathbf{T}c\}$. With $\{\mathbf{T}\{c,d\},\mathbf{F}c\}\in\Delta_{P}^{\text{Bdef}}$ we now get $\{\mathbf{T}\{c,d\}\}$. With these unit nogoods, $\lambda(a,L)$ reduces to $\Box$.

3.2 Correctness of ASP-DRUPE

Next, we establish soundness and completeness of the ASP-DRUPE format.

Lemma 1** (Invariants)**

Let $P$ be a logic program and $\Pi=\langle\sigma_{1},\ldots,\sigma_{n}\rangle$ be a finite ASP-DRUPE derivation for program $P$. Moreover, let $D_{i}$ be the accumulated set of nogoods introduced by the extension rules in $\sigma_{k}$ for all $k\in\{1,\ldots,i\}$. Then, the following holds: $\Delta_{P}\cup\Lambda_{P}\cup D_{i}\models\nabla_{i}(\Pi)\text{ for all }i\in\{0,\ldots,n\}$.

Proof 3.1** (Proof (Sketch).).**

We proceed by induction over the length $n$ of the derivation. For the base case, we have $\nabla_{0}(\Pi)=\Delta_{P}^{\text{Bdef}}$. Hence, $\nabla_{0}(\Pi)\subseteq\Delta_{P}\cup\Lambda_{P}\cup D_{0}$ and the claim holds trivially. For the induction step, we assume that the statement holds for length $i$ and consider step $\sigma_{i+1}$. It remains to do a case distinction for the type:

Deletion with $\sigma_{i+1}=(\mathsf{d},\delta,\epsilon)$: Immediately, we have $\nabla_{i}(\Pi)\models\nabla_{i+1}(\Pi)$. Thus, transitivity of $\models$ and the induction hypothesis establishes this case. 2. 2.

Addition with $\sigma_{i+1}=(\mathsf{a},\delta,\epsilon)$: Since $\delta$ is RUP for $\nabla_{i}(\Pi)$, we know that $\{\delta\}$ is a logical consequence of $\Delta_{i}$. The remaining steps to draw the conclusion are similar to the deletion step case. 3. 3.

Completion Rule Addition with $\sigma_{i+1}=(\mathsf{c},\delta,\epsilon)$: Since the resulting nogood $\delta\in\Delta_{P}^{\leftarrow}$ is contained in $\Delta_{P}$, the result follows. 4. 4.

Completion Support Addition with $\sigma_{i+1}=(\mathsf{s},\delta,a)$: Since the resulting nogood $\{\mathbf{T}a\}\cup\delta$ is contained in $\Delta_{P}^{\rightarrow}$, the result follows. 5. 5.

Extension with $\sigma_{i+1}=(\mathsf{e},\delta,a)$: According to the induction hypothesis we have $\Delta_{P}\cup\Lambda_{P}\cup D_{i}\models\nabla_{i}(\Pi)$. Then, $D_{i}\subset D_{i+1}$, since $a$ is a fresh variable and $\mathsf{ext}(a,\delta)\in D_{i+1}\setminus D_{i}$. As $\models$ is monotone, and $D_{i}\subset D_{i+1}$, we know that $\Delta_{P}\cup\Lambda_{P}\cup D_{i+1}\models\nabla_{i}(\Pi)$. It then follows that $\Delta_{P}\cup\Lambda_{P}\cup D_{i+1}\models\nabla_{i+1}(\Pi)$. 6. 6.

Loop addition with $\sigma_{i+1}=(\mathsf{l},L,a_{1})$: By definition nogood $\delta\,\mathrel{\mathop{:}}=\lambda(a_{1},L)$ is already contained in $\Delta_{P}\cup\Lambda_{P}\cup D_{i}$, which immediately establishes this case.  ∎

Theorem 3.2** (Soundness and Completeness).**

Let $P$ be a logic program. Then, $P$ is inconsistent if and only if there is an ASP-DRUPE proof for $P$.

Proof 3.3** (Proof (Sketch).).**

Let $P$ be a logic program. “$\Leftarrow$”: Assume there is an ASP-DRUPE proof of $P$. By definition, there is a finite sequence of proof steps $\langle\sigma_{i},\ldots,\sigma_{n}\rangle$ such that $\Box\in\nabla_{n}(\Pi)$ and $\nabla_{n}(\Pi)$ is inconsistent. From Lemma 1, we obtain that $\Delta_{P}\cup\Lambda_{P}\cup D_{n}$ is inconsistent. As $D$ consists of extension nogoods with disjoint variables, we know that $\Delta_{P}\cup\Lambda_{P}$ is inconsistent. We conclude from an earlier result [Gebser et al. (2012), Theorem 5.4] that $P$ is inconsistent. “$\Rightarrow$”: Suppose $P$ is inconsistent. According to earlier work [Gebser et al. (2012), Theorem 5.4], we know that $\Delta_{P}\cup\Lambda_{P}$ is inconsistent. RUP is complete [Gelder (2008), Goldberg and Novikov (2003)], which means that for every propositional, unsatisfiable formula $F$ there is a RUP proof for $F$. Hence, we can construct an ASP-DRUPE proof for $P$ as follows: (i) Output all completion rule additions for $\Delta_{P}^{\leftarrow}$ and completion support additions for $\Delta_{P}^{\rightarrow}$. (ii) Generate loop addition steps for all loops $L\in\mathsf{loop}(P)$. (iii) Transform $\Delta_{P}\cup\Lambda_{P}$ into a propositional formula $F=\overline{\Delta_{P}\cup\Lambda_{P}}$ by inverting all nogoods. (iv) Construct and use a RUP proof for $F$. Then, output addition rules accordingly, where again all clauses need to be inverted to obtain addition proof steps using nogoods.

Note that in the only-if direction of the proof, one can also use RAT [Wetzler et al. (2014)] proofs without deletion information and afterwards translate RAT steps into extended resolution steps [Kiesl et al. (2018)].

Listing 1 presents the ASP-DRUPE checker, that decides whether a given ASP-DRUPE proof is correct. The input to the checker is both the original program $P$ and the proof $\Pi$. To check the proof, we encode $P$ into nogoods $\Delta_{P}$ and then check each statement $\sigma\in\Pi$ sequentially.

Lemma 3.4**.**

For a given logic program $P$ and an ASP-DRUPE derivation $\Pi$, the ASP-DRUPE-Checker runs in time at most $\left|\Pi\right|^{{\mathcal{O}}(1)}$.

Corollary 3.5**.**

Given a logic program $P$ and an ASP-DRUPE derivation $\Pi$. Then, the ASP-DRUPE-Checker is correct, i.e., it outputs Success if and only if $\Pi$ is an ASP-DRUPE proof for the inconsistency of $P$.

3.3 Extension to Optimization

Next, we briefly mention how to verify cost optimization. To this end, an optimization rule is an expression of the form \operatorname{\mathrel{\mathchoice{\reflectbox{\displaystyle\rightsquigarrow}}{\reflectbox{\textstyle\rightsquigarrow}}{\reflectbox{\scriptstyle\rightsquigarrow}}{\reflectbox{\scriptscriptstyle\rightsquigarrow}}}}l_{1}[w_{1}], where $l_{1}$ is a literal. Intuitively this indicates that if an assignment satisfies $\mathsf{IAss}(P,\{l_{1}\})$, then this results in costs $w_{1}$. Overall, one aims to minimize the total costs, i.e., the goal is to deliver an answer set of minimal total costs. Therefore, if one wants to verify, whether a given answer set candidate is indeed an answer set of minimal costs, we foresee the following extension to ASP-DRUPE, where such a proof consists of the following two parts. (i) An answer set that shows a solution with costs $c$ exists. (ii) An ASP-DRUPE proof that shows that the program restricted to costs $c-1$ is inconsistent. Note that for disjunctive programs already the first part also needed to contain a second proof showing that indeed there cannot be an unfounded set for the provided answer set. Further, it is not immediate, how this extends to unsatisfiable cores. Hence, so far it only applies to progression based approaches.

4 Integrating ASP-DRUPE Proofs into a Solver

In the following, we describe the CDNL-ASP algorithm for logic programs $P$ that we use as a basis for our theoretical model. Afterwards, we describe how proof logging can be integrated. In other words, during the run of an ASP solver, we immediately print the corresponding ASP-DRUPE rules that are needed later for verification in case the ASP solver concludes that the program is inconsistent. A typical CDNL-based ASP solver (cf., Listing 2) relies on unit propagation, since this is a rather simple and efficient way of concluding consequences. Thereby it keeps a set $\nabla$ of nogoods, a current assignment $A$, and a decision level $\mathit{dl}$. In a loop it applies NogoodPropagation [Gebser et al. (2012), page 101] consisting of unit propagation and loop propagation (using UnfoundedSet [Gebser et al. (2012), page 104]) whenever suited. Then, if there is some nogood that is not satisfied, either the program is inconsistent (at decision level 0) or ConflictAnalysis [Gebser et al. (2012), page 108] triggers backtracking to an earlier decision level, followed by the learning of a conflict nogood $\delta$. Otherwise, if all nogoods in $\Delta_{P}\cup\nabla$ are satisfied and all the variables are assigned, an answer set is found, and otherwise some free variable is selected (Select).

Listings 2 and 3 contain a prototypical CDNL-based ASP solver that is extended by proof logging, where the changes for proof logging are highlighted in red. We use the element operator ($\in$) to determine whether an element is in a sequence, and denote the concatenation of two proofs by the $\cdot$ operator as follows: $\langle\sigma_{1},\ldots,\sigma_{i}\rangle\cdot\langle\sigma_{i+1},\ldots,\sigma_{n}\rangle\,\mathrel{\mathop{:}}=\langle\sigma_{1},\ldots,\sigma_{i},\sigma_{i+1},\ldots,\sigma_{n}\rangle$. The idea is to start with an empty ASP-DRUPE derivation. Whenever a new nogood, or loop nogood is learned and added to $\nabla$ accordingly, this results in an added addition or loop addition proof step, respectively. Note that in Listing 3 we add completion rule addition steps and completion support addition steps, whenever unit propagation (or conflicts) involve rules in $\Delta_{P}^{\leftarrow}$ or $\Delta_{P}^{\rightarrow}$, respectively. In particular, Lines 3 and 3 take care of adding involved parts of the completion to the proof (if needed) accordingly. At the end, when the ASP solver concludes inconsistency, the proof is returned including the empty nogood as last nogood. Note that advanced techniques (see, e.g., [Gebser et al. (2012)]) like forgetting of learned clauses and restarting of the ASP solver can also be implemented using deletion rules with ASP-DRUPE.

As it turns out, preprocessing in ASP is less sophisticated as for SAT. In the literature, CDNL-based ASP solvers often use preprocessing techniques [Gebser et al. (2008)] similar to SAT solvers, i.e., SatElite-like [Eén and Biere (2005)] operations as variable and nogood elimination. For simple preprocessing operations restricted to variable and nogood elimination ASP-DRUPE suffices. Note that if Clark’s completion is exponential in the program size due to weight rules, also propagators [Alviano et al. (2018)] are supported. For details we refer to the implementation in Section 4.1.

Example 4.6** (CDNL-ASP-DRUPE).**

We continue the previous Example 2 and indicate a possible CDNL-ASP-DRUPE run on $P$ that leads to the exemplary ASP-DRUPE proof given above. We use the notation $\mathbf{T}X@\mathit{dl}$ ($\mathbf{F}X@\mathit{dl})$ to indicate that $X$ was assigned true (false) at decision level $\mathit{dl}$.

Initially, nothing can be propagated. 2. 2.

After the decision $\mathbf{T}a@1$, unit propagation derives only $\mathbf{F}\{{\sim}a,{\sim}e\}@1$. 3. 3.

After the second decision $\mathbf{F}\{c\}@2$, we eventually derive $\mathbf{T}a@2$ and $\mathbf{T}b@2$ by unit propagation. Thus we discover the unfounded set $U=\{a,b\}\in\operatorname{\mathsf{loop}}(P)$, and add the loop nogood $\lambda(a,U)$. 4. 4.

The loop nogood immediately leads to a conflict, and conflict analysis learns the nogood $\{\mathbf{F}\{c\},\mathbf{T}a\}$. 5. 5.

We backtrack to decision level 1, and after propagation, make the decision $\mathbf{T}e@2$. We arrive at another conflict, and learn $\{\mathbf{T}e,\mathbf{F}\{{\sim}a,{\sim}e\}\}$. 6. 6.

After backtracking, a conflict appears at decision level 1, and we learn $\{\mathbf{T}a\}$. 7. 7.

We backtrack to decision level 0, and decide on $\mathbf{T}e@1$. After arriving at a conflict almost immediately, we learn $\{\mathbf{T}e\}$. 8. 8.

We backtrack once more, and finally arrive at a conflict at decision level 0, returning INCONSISTENT along with an ASP*-*DRUPE proof. Note that the proof given in Example 2 is slightly simplified in that we only include those steps of types $\mathsf{c}$ and $\mathsf{s}$ that are actually used.

4.1 Implementation of ASP-DRUPE in wasp solver

We provide an implementation of ASP-DRUPE within the wasp [Alviano et al. (2015)] solver that is available on github222The repository can be found at https://github.com/alviano/wasp/tree/unsatproof.. The solver prints a proof for inconsistency in the file proof.log if the solver gets passed the program options - -disable-simplifications - -proof-log=proof.log. Actually wasp prints an ASP-DRUPE derivation also in the positive case of consistency. This derivation can still be used to verify whether the nogoods learned by the solver are correct. Currently, proof logging is restricted to normal programs and we do not yet support recursive weight rules due to discrepancy among different semantics as discussed in the preliminaries. Moreover, we had to introduce a normalized form because of several (in-processing) simplifications that would otherwise require major refactoring to isolate. Just to mention one of these simplifications, a rule of the form $a\leftarrow\,\ell_{1},\ldots,\ell_{n},{\sim}a$ is replaced by the integrity constraint $\leftarrow\,\ell_{1},\ldots,\ell_{n},{\sim}a$. While these simplifications are required to achieve efficient computation, they alter the completion of the input program. Therefore, wasp cannot log in the proof the auxiliary atoms required to keep the completion compact. The problem is circumvented by introducing a normalized form such that the completion can be compactly computed without introducing any auxiliary atoms.

A program $P$ is in short-body normalized form if for each atom $a\in\and(P)$ either $\left|\mathsf{IB}(P,a)\right|\leq 1$, or for any body $B\in\mathsf{IB}(P,a)$, we have $\left|B\right|\leq 1$. Any normal program can be transformed into short-body normalized form in linear time by introducing a linear number of auxiliary atoms (in the program size). This normalized form allows us to get rid of auxiliary variables for bodies $B\in\mathtt{Bod}(P)$, i.e., we can set $\Delta_{P}^{\text{Bdef}}=\emptyset$, and replace $\mathbf{T}B$ in $\Delta_{P}^{\leftarrow}$ by $\mathsf{IAss}(P,B)$, and $\mathbf{F}B$ in $\Delta_{P}^{\rightarrow}$ by $\overline{\mathsf{IAss}(P,B)}$. For simplification and increased readability of a compact resulting proof log, we further do not use neither completion rule addition, nor completion support addition types. Instead, we assume that the checker is aware of the completion from the beginning. In this respect, we have to observe that for weight rules, completion might be exponential in the program size. Therefore, we require that the checker is equipped with a propagator [Alviano et al. (2018)] for drawing conclusions by unit-propagation on parts of the completion associated with weight rules. We provide an implementation of such a checker tool as well333Both the checker tool and a tool for bringing normal logic programs in short-body normalized form can be found at https://github.com/alviano/python/tree/master/asp-proof..

5 ASP-DRUPE Implementational Specifications

Next, we discuss the specific format description of ASP-DRUPE that we think can be commonly used in ASP solvers. To this end, we assume a program $P$ and a set $\{\hat{B}\mid B\in\mathtt{Bod}(P)\}$ of fresh atoms, where we have one fresh atom for each induced body in $P$. Further, let $\mathsf{vm}:(\and(P)\cup\{\hat{B}\mid B\in\mathtt{Bod}(P)\})\rightarrow\mathbb{N}$ be an injective mapping of atoms $a\in\and(P)\cup\{\hat{B}\mid B\in\mathtt{Bod}(P)\}$ to a unique positive integer $n\geq 1$ such that $\mathsf{vm}(a)\,\mathrel{\mathop{:}}=n$, and $a=\mathsf{vm}^{-1}(n)$. Note that for atoms $a\in\and(P)$ this can be (partly) already provided by the input format. However, for technical reasons, we assume such a mapping also for atom $\hat{B}$, where $B\in\mathtt{Bod}(P)$, as these integers will then correspond to fresh atoms. We define in the following an SModels-like [Syrjänen (2000)] output format of strings for a given program $P$, which is ready for the checker to parse. Actually, the output format is “line-based”, i.e., it is even ASPIF-like [Gebser et al. (2016)]. However, ASP-DRUPE still supports ASP only, and not ASP solving with theory reasoning. To this end, let the truth value mapping $\mathsf{tv}$ map a variable assignment $l$ to an integer different from 0, where a positive integer represents an atom and a negative integer a negated atom.

[TABLE]

Then, the ASP-DRUPE output format is a sequence $\zeta=\langle s_{1},\ldots,s_{j}\rangle$ of strings, where each element in the sequence corresponds to one rule in an ASP-DRUPE derivation and is terminated by character “0”. Each part of an element in the sequence is separated by a white space (␣). We indicate other strings constants by ${}^{\prime}string^{\prime}$. Then, element $s_{i}$ of the sequence $\zeta$ for $1\leq i\leq j$ is of the following form.

• •

A body definition string is of the form ${}^{\prime}\mathsf{b}^{\prime}\text{\textvisiblespace}{}b_{1}\text{\textvisiblespace}{}n_{1}\text{\textvisiblespace}{}\ldots\text{\textvisiblespace}{}n_{k}\text{\textvisiblespace}{}^{\prime}0^{\prime}$ such that $b_{1}$, $n_{1}$, $\ldots$, $n_{k}\in\mathbb{N}$. Further, we require that $\{\mathsf{tv}^{-1}(n_{1}),\ldots,\mathsf{tv}^{-1}(n_{k})\}=\mathsf{IAss}(P,B)$ for some $B\in\mathtt{Bod}(P)$. Finally, for $s_{i}$ the string corresponds to the proof step $(\mathsf{e},\{\mathbf{T}B\},{\hat{B}})$, where ${\hat{B}}=\mathsf{vm}^{-1}(b_{1})$. The technical purpose of $s_{i}$ is to specify the fresh body variable $\hat{B}$ for a body $B\in\mathtt{Bod}(P)$.

• •

An addition string is of the form ${}^{\prime}\mathsf{a}^{\prime}\text{\textvisiblespace}{}n_{1}\text{\textvisiblespace}{}\ldots\text{\textvisiblespace}{}n_{k}\text{\textvisiblespace}{}^{\prime}0^{\prime}$ such that $n_{1},\ldots,n_{k}\in\mathbb{N}$, which corresponds to proof step $(\mathsf{a},\{\mathsf{tv}^{-1}(n_{1}),\ldots,\mathsf{tv}^{-1}(n_{k})\},\epsilon)$.

• •

A completion rule addition string is of the form ${}^{\prime}\mathsf{c}^{\prime}\text{\textvisiblespace}{}b_{1}\text{\textvisiblespace}{}n_{1}\text{\textvisiblespace}{}\ldots\text{\textvisiblespace}{}n_{k}\text{\textvisiblespace}{}^{\prime}0^{\prime}$ such that $b_{1},n_{1},\ldots,n_{k}\in\mathbb{N}$ and ${\hat{B}}=\mathsf{vm}^{-1}(b_{1})$, which relates to proof step $(\mathsf{c},\{\mathbf{F}\mathsf{vm}^{-1}(n_{1}),\ldots,\mathbf{F}\mathsf{vm}^{-1}(n_{k}),\mathbf{T}B\},\epsilon)$.

• •

A completion support addition string is of the form ${}^{\prime}\mathsf{s}^{\prime}\text{\textvisiblespace}{}n_{1}\text{\textvisiblespace}{}b_{1}\text{\textvisiblespace}{}\ldots\text{\textvisiblespace}{}b_{k}\text{\textvisiblespace}{}^{\prime}0^{\prime}$ such that $n_{0},b_{1},\ldots,$ $b_{k}\in\mathbb{N}$ and $\hat{B}_{i}=\mathsf{vm}^{-1}(b_{i})$ for $i\in\{1,\ldots,k\}$, which corresponds to proof step $(\mathsf{s},\{\mathbf{F}B_{1},\ldots,$ $\mathbf{F}B_{k}\},\mathsf{vm}^{-1}(n_{0}))$.

• •

An extension string is of the form ${}^{\prime}\mathsf{e}^{\prime}\text{\textvisiblespace}{}n_{0}\text{\textvisiblespace}{}n_{1}\text{\textvisiblespace}{}\ldots\text{\textvisiblespace}{}n_{k}\text{\textvisiblespace}{}^{\prime}0^{\prime}$ such that $n_{0}$, $n_{1}$, $\ldots$, $n_{k}\in\mathbb{N}$, which corresponds to proof step $(\mathsf{e},\{\mathsf{tv}^{-1}(n_{1}),\ldots,\mathsf{tv}^{-1}(n_{k})\},\mathsf{vm}^{-1}(n_{0}))$.

• •

A deletion string is of the form ${}^{\prime}\mathsf{d}^{\prime}\text{\textvisiblespace}{}n_{1}\text{\textvisiblespace}{}\ldots\text{\textvisiblespace}{}n_{k}\text{\textvisiblespace}{}^{\prime}0^{\prime}$ such that $n_{1},\ldots,n_{k}\in\mathbb{N}$, which corresponds to proof step $(\mathsf{d},\{\mathsf{tv}^{-1}(n_{1}),\ldots,\mathsf{tv}^{-1}(n_{k})\},\epsilon)$.

• •

A loop addition string is of the form ${}^{\prime}\mathsf{l}^{\prime}\text{\textvisiblespace}{}n_{1}\text{\textvisiblespace}{}\ldots\text{\textvisiblespace}{}n_{k}\text{\textvisiblespace}{}^{\prime}0^{\prime}$ such that $n_{1}$, $\ldots$, $n_{k}\in\mathbb{N}$, which corresponds to proof step $(\mathsf{l},\{\mathbf{T}\mathsf{vm}^{-1}(n_{1}),\ldots,\mathbf{T}\mathsf{vm}^{-1}(n_{k})\},\mathsf{vm}^{-1}(n_{1}))$.

• •

An unfounded set addition string is of the form ${}^{\prime}\mathsf{u}^{\prime}\text{\textvisiblespace}{}k\text{\textvisiblespace}{}n_{1}\text{\textvisiblespace}{}\ldots\text{\textvisiblespace}{}n_{k}\text{\textvisiblespace}{}o_{1}\text{\textvisiblespace}{}\ldots\text{\textvisiblespace}{}o_{m}\text{\textvisiblespace}{}^{\prime}0^{\prime}$ such that $n_{1},$ $\ldots,n_{k},o_{1},\ldots,o_{m}\in\mathbb{N}$, which then corresponds to proof step $(\mathsf{u},\{\mathbf{T}\mathsf{vm}^{-1}(n_{1}),\ldots,\mathbf{T}\mathsf{vm}^{-1}(n_{k})$ $\},\epsilon,\{\mathsf{tv}^{-1}(o_{1}),\ldots,\mathsf{tv}^{-1}(o_{m})\})$.

Next, we define how to obtain the ASP-DRUPE output format $\zeta=\mathsf{smod}(\Pi)$ of a given ASP-DRUPE derivation $\Pi=\langle\sigma_{1},\ldots,\sigma_{n}\rangle$. To this end, we define $s=\mathsf{smod}(\sigma_{i})$, which transforms a proof step $\sigma_{i}$ into a string $s$ for $1\leq i\leq n$, by slight abuse of notation.

[TABLE]

Since fresh body atoms require introduction using extension proof steps in advance, we assume $\mathtt{Bod}(P)=\{B_{1},\ldots,B_{q}\}$, where $B_{i}=\{l_{i,1},\ldots l_{i,\left|B_{i}\right|}\}$ for $1\leq i\leq q$. Finally, let $\mathsf{smod}(\Pi)\,\mathrel{\mathop{:}}=\langle^{\prime}\mathsf{b}^{\prime}\text{\textvisiblespace}{}\mathsf{vm}(\hat{B}_{1})\text{\textvisiblespace}{}\mathsf{tv}(l_{1,1})\text{\textvisiblespace}{}\ldots\text{\textvisiblespace}{}\mathsf{tv}(l_{1,\left|B_{1}\right|})\text{\textvisiblespace}{}^{\prime}0^{\prime}\rangle\cdot\ldots\cdot\langle^{\prime}\mathsf{b}^{\prime}\text{\textvisiblespace}{}\mathsf{vm}(\hat{B}_{q})\text{\textvisiblespace}{}\mathsf{tv}(l_{q,1})\text{\textvisiblespace}{}\ldots\text{\textvisiblespace}{}\mathsf{tv}(l_{q,\left|B_{q}\right|})\text{\textvisiblespace}{}^{\prime}0^{\prime}\rangle\cdot\mathsf{smod}(\sigma_{1})\cdot\ldots\cdot\mathsf{smod}(\sigma_{n})$. As a simplification, one can leave out additional, unused body definition strings.

Example 5.7**.**

Consider the ASP-DRUPE proof $\Pi$ for inconsistency of $P$ from Example 2 and assume the dictionary in the program input assigns $\mathsf{vm}(a)=1$, $\mathsf{vm}(b)=2$, $\mathsf{vm}(c)=3$, $\mathsf{vm}(d)=4$, and $\mathsf{vm}(e)=5$. We extend this to the necessary bodies: $\mathsf{vm}(\{c\})=6$, $\mathsf{vm}(\{{\sim}c\})=7$, $\mathsf{vm}(\{{\sim}d\})=8$, $\mathsf{vm}(\{a,d\})=9$, $\mathsf{vm}(\{b,d\})=10$, $\mathsf{vm}(\{c,d\})=11$, $\mathsf{vm}(\{{\sim}a,{\sim}e\})=12$, and $\mathsf{vm}(\{c,{\sim}e\})=13$. Figure 1 corresponds to $\mathsf{smod}(\Pi)$. Note that we use body definitions for required body variables.

6 Conclusion & Future Work

ASP solvers are highly-tuned decision procedures that are widely applied in academia and industry. In this paper, we considered how to ensure that if an ASP solver outputs that a program has no answer set then the solver is indeed right. Similar to unsat certificates in SAT solvers, we propose an approach that augments the inconsistency answer of an ASP solver with a certificate of inconsistency. This approach allows the use of unverified, efficient ASP solvers while guaranteeing that a particular run of an ASP solver has been correct.

To this end, we developed a new proof format called ASP-DRUPE. It allows several types of proof steps: (RUP) addition that models nogood learning, completion rule addition and completion support addition for adding completion rules on demand, deletion that models nogood forgetting, extension that allows to infer new definitions and loop addition that adds nogoods to forbid assignments that do not correspond to answer sets. ASP-DRUPE supports formula simplification methods that can be obtained by learning entailed nogoods, nogood deletion as well as extended resolution. We established that ASP-DRUPE is sound and complete for logic programs and can be used effectively, i.e., a program $P$ is inconsistent if and only if a ASP-DRUPE proof of $P$ exists and that we can check an ASP-DRUPE proof in polynomial time of the proof length. Further, we demonstrated how to augment CDNL-based solvers with proof logging. It is in our interest for future work to continue this line of research. Potential next steps include the study of theory reasoning towards covering the full ASPIF intermediate format.

Finally, we would like to say a few words about RAT-style proofs. The combination of nogood deletion, loop, and RAT addition results in an inconsistent proof system in which we can infer a conflict although a non-tight program is consistent. This stems from the situation that clauses that are RAT with respect to $\nabla$ are not necessarily RAT with respect to $\Delta_{P}\cup\Lambda_{P}$. Although it was recently shown that extended resolution simulates DRAT [Kiesl et al. (2018)], we are unaware whether ASP-DRUPE can be extended to RAT such that each rule application can be checked in polynomial time, which we believe is an interesting question for future work.