First-Order Interpolation and Interpolating Proof Systems
Laura Kovács, Андрей Воронков · EPiC series in computing · 2018
It is known that one can extract Craig interpolants from so-called local proofs. An interpolant extracted from such a proof is a boolean combination of formulas occurring in the proof. However, standard complete proof systems, such as superposition, for theories having the interpolation property are not necessarily complete for local proofs: there are formulas having non-local proofs but no local proof. In this paper we investigate interpolant extraction from non-local refutations (proofs of contradiction) in the superposition calculus and prove a number of general results about interpolant extraction and complexity of extracted interpolants. In particular, we prove that the number of quantifier alternations in first-order interpolants of formulas without quantifier alternations is unbounded. This result has far-reaching consequences for using local proofs as a foundation for interpolating proof systems: any such proof system should deal with formulas of arbitrary quantifier complexity. To search for alternatives for interpolating proof systems, we consider several variations on interpolation and local proofs. Namely, we give an algorithm for building interpolants from resolution refutations in logic without equality and discuss additional constraints when this approach can be also used for logic with equality. We finally propose a new direction related to interpolation via local proofs in first-order theories.