Effective Synthesis of Strongly Equivalent Logic Programs via Craig Interpolation in First-Order Logic

The existence of a logic program R that is strongly equivalent to the combination of a given program P and another given program Q, under a restricted vocabulary, can be characterized as a first-order entailment. Moreover, such a program R can be effectively constructed from a Craig interpolant of the entailment.