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

Jan Heuer, Christoph Wernhard

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 existe…