Inconsistency Proofs for ASP: The ASP-DRUPE Format

Carmine Dodaro; Jakob Rath; Johannes K. Fichte; Mario Alviano; Markus Hecher; Tobias Philipp

arxiv: 1907.10389 · v1 · pith:OJKE2YAOnew · submitted 2019-07-24 · 💻 cs.LO · cs.AI

Inconsistency Proofs for ASP: The ASP-DRUPE Format

Mario Alviano , Carmine Dodaro , Johannes K. Fichte , Markus Hecher , Tobias Philipp , Jakob Rath This is my paper

Pith reviewed 2026-05-24 16:44 UTC · model grok-4.3

classification 💻 cs.LO cs.AI

keywords Answer Set ProgrammingProof formatsInconsistency proofsReverse Unit PropagationDisjunctive logic programsDRUPEASP solversLogic programming

0 comments

The pith

ASP-DRUPE is a proof format that certifies disjunctive logic programs have no answer sets.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

Verifying that a claimed answer set is correct can be done quickly, but confirming that a program has none at all requires a different kind of evidence. The paper introduces ASP-DRUPE, which adapts the reverse unit propagation technique from SAT proofs to the setting of answer set programming. The format covers propositional disjunctive programs and extends to weight rules and choice rules. Correctness of the format is shown, and the authors describe how current solvers can be modified to emit these proofs. An implementation inside the wasp solver demonstrates the approach for normal programs.

Core claim

The paper establishes that ASP-DRUPE correctly certifies the absence of answer sets for propositional disjunctive logic programs that include weight rules and choice rules, by extending the reverse unit propagation mechanism from Boolean satisfiability while preserving soundness under ASP semantics.

What carries the argument

The ASP-DRUPE format, which records a sequence of reverse unit propagation steps adapted to ASP semantics that derive a contradiction from the program rules.

If this is right

Modern ASP solvers can be extended to output ASP-DRUPE proofs when they conclude a program is inconsistent.
The format applies uniformly to normal programs, disjunctive programs, weight rules, and choice rules.
An implementation inside the wasp solver shows that the format can be produced for normal logic programs without changing the core solving algorithm.
Independent checkers can verify the proofs in polynomial time relative to the size of the derivation.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

Verified inconsistency proofs could support the use of ASP in domains where the absence of solutions must be demonstrated to a third party.
The same RUP-style approach might be adapted to produce proofs for other non-monotonic formalisms that decide consistency.
Tool chains that already handle DRUP proofs for SAT could be reused or lightly extended to handle ASP-DRUPE files.

Load-bearing premise

Extending the RUP derivation rules from SAT to the answer-set semantics of disjunctive programs with weights and choices keeps the proofs sound.

What would settle it

A concrete program that possesses an answer set together with a purported ASP-DRUPE proof claiming inconsistency, or an ASP-DRUPE derivation that cannot be checked by the stated propagation rules.

read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

ASP-DRUPE extends RUP to certify inconsistency for disjunctive ASP programs with weights and choices, plus a wasp implementation, but the abstract leaves the soundness derivation for the new rules undetailed.

read the letter

The paper introduces ASP-DRUPE as a proof format that adapts reverse unit propagation from SAT to propositional disjunctive logic programs, including weight and choice rules, so that a solver's claim of no answer sets can be checked. They also describe how to plug the format into existing solvers and give a concrete implementation for the wasp solver on normal programs. That implementation is the most immediately usable part, since verifying inconsistency has been harder than verifying a claimed answer set. The approach stays close to established RUP work and does not introduce circular definitions or free parameters. The central claim is that the authors establish correctness of the extended rules. The abstract states this but supplies no explicit inference rules for weight or choice constructs and no walk-through showing they preserve the minimality and unfounded-set properties that matter in ASP. The stress-test concern therefore lands on the provided text: without those details it is not possible to confirm the extension cannot admit spurious inconsistency proofs. The work is scoped to propositional programs, which fits the verification goal. This is the sort of paper that solver developers and people using ASP in planning or AI applications would want to see. It deserves a serious referee because the practical verification need is real and the implementation shows the authors have moved beyond a sketch, even though the soundness argument will need close checking during review.

Referee Report

1 major / 0 minor

Summary. The paper introduces the ASP-DRUPE proof format, extending the Reverse Unit Propagation (RUP) format from SAT to certify inconsistency (absence of answer sets) for propositional disjunctive logic programs that may include weight and choice rules. It claims to establish the correctness of ASP-DRUPE, discusses integration into modern ASP solvers, and reports an implementation for normal logic programs inside the wasp solver.

Significance. If the soundness argument holds, the format supplies the first practical mechanism for producing and checking certificates of unsatisfiability in ASP, addressing a verification gap that is harder than checking individual answer sets. The work builds directly on the mature DRUP/RUP literature and supplies an implementation, which are concrete strengths.

major comments (1)

[Sections describing the proof rules and the correctness argument] The manuscript asserts that correctness of the ASP-DRUPE rules is established for disjunctive programs and for weight/choice rules, yet supplies neither the explicit statement of the adapted inference rules for those constructs nor a derivation showing that they preserve the necessary properties (unfounded-set detection and minimality) that distinguish ASP semantics from SAT. This derivation is load-bearing for the central claim.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the careful reading and for highlighting the need for greater explicitness in the correctness argument. We address the major comment below and will revise the manuscript accordingly.

read point-by-point responses

Referee: [Sections describing the proof rules and the correctness argument] The manuscript asserts that correctness of the ASP-DRUPE rules is established for disjunctive programs and for weight/choice rules, yet supplies neither the explicit statement of the adapted inference rules for those constructs nor a derivation showing that they preserve the necessary properties (unfounded-set detection and minimality) that distinguish ASP semantics from SAT. This derivation is load-bearing for the central claim.

Authors: We agree that the manuscript does not supply the explicit adapted inference rules for disjunctive programs and for weight/choice rules, nor a derivation showing preservation of unfounded-set detection and minimality. While the core RUP-style rules are stated for the normal case and correctness is claimed for the extensions, the adaptation details and the required semantic preservation argument are missing. In the revision we will insert (i) the explicit inference rules for the disjunctive, weight, and choice cases and (ii) a derivation (or detailed proof sketch) establishing that these rules continue to detect unfounded sets and enforce minimality. The new material will be placed in the sections on proof rules and correctness. revision: yes

Circularity Check

0 steps flagged

ASP-DRUPE extends independent RUP without circular reduction

full rationale

The paper develops ASP-DRUPE by adapting the established Reverse Unit Propagation format from SAT literature to disjunctive ASP programs with weight and choice rules. It claims to establish correctness of the format but the provided abstract and description contain no equations, definitions, or steps that reduce by construction to fitted parameters, self-citations, or renamed inputs. The core extension references external SAT RUP work as its foundation, with no load-bearing self-citation chain or ansatz smuggling visible. This qualifies as a self-contained derivation against external benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

Based solely on abstract: relies on standard ASP semantics for disjunctive programs and the established correctness of RUP for SAT; no free parameters or invented entities described.

axioms (2)

domain assumption Standard answer set semantics for propositional disjunctive logic programs with weight and choice rules
The format targets these programs as stated in the abstract.
standard math Soundness of Reverse Unit Propagation (RUP) for SAT inconsistency proofs
ASP-DRUPE is explicitly based on RUP.

pith-pipeline@v0.9.0 · 5711 in / 1035 out tokens · 30453 ms · 2026-05-24T16:44:54.222131+00:00 · methodology

Inconsistency Proofs for ASP: The ASP-DRUPE Format

Core claim

What carries the argument

If this is right

Where Pith is reading between the lines

Load-bearing premise

What would settle it

discussion (0)