Synthesizing Strongly Equivalent Logic Programs: Beth Definability for Answer Set Programs via Craig Interpolation in First-Order Logic
<|reference_start|>Synthesizing Strongly Equivalent Logic Programs: Beth Definability for Answer Set Programs via Craig Interpolation in First-Order Logic: 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.<|reference_end|>
@article{heuer2024synthesizing,
    title={Synthesizing Strongly Equivalent Logic Programs: Beth Definability for
  Answer Set Programs via Craig Interpolation in First-Order Logic},
    author={Jan Heuer and Christoph Wernhard},
    journal={arXiv preprint arXiv:2402.07696},
    year={2024},
    doi={10.1007/978-3-031-63498-7_11},
    archivePrefix={arXiv},
    eprint={2402.07696},
    primaryClass={cs.LO}
}