@techreport{yorsh2005a,
author = {Yorsh, Greta and Musuvathi, Madan},
title = {A Combination Method for Generating Interpolants},
year = {2005},
month = {July},
abstract = {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).},
publisher = {Springer-Verlag},
url = {http://approjects.co.za/?big=en-us/research/publication/a-combination-method-for-generating-interpolants/},
pages = {18},
edition = {in CADE 2005: Twentieth International Conference on Automated Deduction.},
number = {MSR-TR-2004-108},
note = {in CADE 2005: Twentieth International Conference on Automated Deduction.},
}