On the existence of polynomial time algorithms for interpolation problems in propositional logic (Q1118581)

An interpolant of two formulae G and H, such that H is a consequence of G, is a formula I which is a consequence of G, implies H, and has as variables only the common variables of G and H. For technical reasons we consider instead of the case that H is a consequence of G, the case that G and H are inconsistent, and ask for a formula I which is a consequence of G, inconsistent with H, and has as variables only the common variables of G and H. The paper considers the problem of the complexity for the computation of such an interpolant for several subclasses of propositional formulae. It is shown that the interpolation problem is of the same degree of difficulty as the corresponding satisfiability problem.