A Parametric Interpolation Framework for First-Order Theories

Craig interpolation is successfully used in both hardware and softwaremodel checking. Generating good interpolants, and hence automatic understanding of the quality of interpolants is however a very hard problem,requiring non-trivial reasoning in first-order theories.An important class of state-of-the-art interpolation algorithmsis based on recursive procedures that generate interpolantsfrom refutations of unsatisfiable conjunctions of formulas.We analyze this type of algorithms and develop a theoretical framework,called a parametric interpolationframework, for arbitrary first-order theories and inference systems.As interpolation-based verification approaches depend on the quality of interpolants,our method can be used to deriveinterpolants of different structure and strength, withor without quantifiers, from the same proof.We show that some well-known interpolation algorithms are instantiations of our framework