Synthesizing Strongly Equivalent Logic Programs: Beth Definability for Answer Set Programs via Craig Interpolation in First-Order Logic

TL;DR

The paper presents an effective, programmatic approach to Beth definability for answer set programs by reducing the existence of a strongly equivalent, vocabulary‑restricted reformulation to first‑order FO entailment. It encodes logic programs in FO using a 0/1‑superscripted representation and translates strong equivalence into FO equivalence via the γ translation and $\mathsf{S}_P$ formulas, enabling Craig interpolation to produce explicit definients. By developing an LP‑interpolation framework (a strengthened Craig‑Lyndon interpolation) and an extraction procedure, the authors show how to obtain a concrete program R from the interpolant, ensuring $P\cup R$ is strongly equivalent to $P\cup Q$ while respecting the allowed vocabulary. The work further provides a practical prototype, implemented with CMProver and Prover9 in the PIE environment, demonstrating the potential to transform and synthesize ASPs from first‑order proofs, with applications in program transformation and knowledge representation.

Abstract

We show a projective Beth definability theorem for logic programs under the stable model semantics: For given programs $P$ and $Q$ and vocabulary $V$ (set of predicates) the existence of a program $R$ in $V$ such that $P \cup R$ and $P \cup Q$ are strongly equivalent can be expressed as a first-order entailment. Moreover, our result is effective: A program $R$ can be constructed from a Craig interpolant for this entailment, using a known first-order encoding for testing strong equivalence, which we apply in reverse to extract programs from formulas. As a further perspective, this allows transforming logic programs via transforming their first-order encodings. In a prototypical implementation, the Craig interpolation is performed by first-order provers based on clausal tableaux or resolution calculi. Our work shows how definability and interpolation, which underlie modern logic-based approaches to advanced tasks in knowledge representation, transfer to answer set programming.