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 equalityinterpolating 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).

• Type: Conference
• Year: 2005
• Where: CADE
• Authors: Greta Yorsh, Madanlal Musuvathi
• Keywords: Automated Reasoning, CADE 2005, Combination Method, Combination Method Applies, Nelson-Oppen-style Decision Procedures