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

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.

Preprint version of the IJCAR 2024 contribution

References in corpus (6)

• Abstract Gringo
• Verifying Tight Logic Programs with anthem and Vampire
• Characterising equilibrium logic and nested logic programs: Reductions and complexity
• Facets of the PIE Environment for Proving, Interpolating and Eliminating on the Basis of First-Order Logic
• Craig Interpolation with Clausal First-Order Tableaux
• Range-Restricted Interpolation through Clausal Tableaux