Interpolation with Automated First-Order Reasoning
For researchers in automated reasoning and knowledge processing, this is a survey that consolidates known techniques without presenting new results or empirical improvements.
This paper surveys automated first-order reasoning methods for Craig and uniform interpolation, focusing on two-stage approaches using clausal tableaux and resolution, and discusses preprocessing techniques, equality encodings, and variations for databases and logic programming.
We consider interpolation from the viewpoint of fully automated theorem proving in first-order logic as a general core technique for mechanized knowledge processing. For Craig interpolation, our focus is on the two-stage approach, where first an essentially propositional ground interpolant is calculated that is then lifted to a quantified first-order formula. We discuss two possibilities to obtain a ground interpolant from a proof: with clausal tableaux, and with resolution. Established preprocessing techniques for first-order proving can also be applied for Craig interpolation if they are restricted in specific ways. Equality encodings from automated reasoning justify strengthened variations of Craig interpolation. Contributions to Craig interpolation that emerged from automated reasoning include variations for logics used in databases and logic programming. As an approach to uniform interpolation we introduce second-order quantifier elimination with examples and describe the basic algorithms DLS and SCAN.