A Combination Method for Generating Interpolants

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 modularly generates interpolants for the combined theory. Our combination method applies for a broad class of first-order theories, which we characterize as equality-interpolating Nelson-Oppen theories. This class includes many useful theories such as the quantifier-free theories of uninterpreted functions, linear inequalities over reals, and Lisp structures. The combination method can be implemented within existing Nelson-Oppen-style decision procedures (such as Simplify, Verifun, ICS, CVC-Lite, and Zap).

cade05-interpolants.pdf
PDF file

In  in CADE 2005: Twentieth International Conference on Automated Deduction.

Publisher  Springer-Verlag
All copyrights reserved by Springer 2004.

Details

TypeInproceedings
URLhttp://www.springer-ny.com/
Pages18
NumberMSR-TR-2004-108
InstitutionMicrosoft Research
> Publications > A Combination Method for Generating Interpolants