First-order Interpolation

Laura Kovacs

Craig Interpolation is an important technique in applications of software verification. Interpolants extracted from proofs of software correctness can, for example, be used to generate loop invariants. In this talk, I will discuss how interpolants from so-called local proofs can be efficiently constructed, using for example a first order prover. I will also describe a technique of generating and optimizing interpolants based on transformations over the so-called “grey area” of local proofs. While local proofs admit efficient interpolation algorithms, standard complete proof systems, such as superposition, for theories having the interpolation property are not necessarily complete for local proofs. In this talk, I will therefore also investigate interpolant extraction from non-local proofs in the superposition calculus and prove a number of general results about interpolant extraction and complexity of extracted interpolants.