Abstract

An interpolant for a pair (A, B) of inconsistent formulas is a formula C such that: A implies C; B is inconsistent with C; and C only contains common symbols between A and B. Modern techniques for interpolant generation rely on special deductive calculus and unsatisfiability proofs. In this talk, we will discuss a new algorithm to compute the interpolation formula for the theory of Equality with Uninterpreted Functions (EUF) that does not require unsatisfiability proofs. We will discuss an observation made during the implementation of the algorithm, introducing a new Horn-unsatisfiability algorithm that uses a congruence closure with explanations as the mechanism for equality propagation.