A Combination Method for Generating Interpolants
Greta Yorsh and Madan Musuvathi
To appear in Proc. Conf. on Automated Deduction, 2005 (CADE-20,
Microsoft Research Technical Report, MSR-TR-2004-108, October 2004
We present a combination method for generating interpolants for a class of
first-order theories. Using interpolant-generation procedures for individual
theories as black-boxes, our method generates interpolants for the combined
theory. Our method extends that of McMillan to a class of first-order theories,
which we characterize as equality-interpolating Nelson-Oppen theories.
We show that this class includes many useful theories such as the
quantifier-free theories of uninterpreted functions, linear inequalities over
reals, and Lisp structures. Our method provides a way to integrate interpolant
generation within existing Nelson-Oppen-style decision procedures (such as
Simplify, Verifun, ICS, and CVC-Lite).
We have implemented this method in Zap, a symbolic reasoning engine in
development at Microsoft Research.
Click here to access the short version of the paper (CADE-20, 2005):
Click here to access the technical report with proofs (October 2004):
Unfortunately, the technical report published by MSR is no longer available.
The proofs (dated October 2004) can be found in the appendix of this document