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).
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Barrett, C., Berezin, S.: CVC lite: A new implementation of the cooperating validity checker category B. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 515–518. Springer, Heidelberg (2004)
Craig, W.: Linear reasoning. a new form of the herbrand-gentzen theorem. J. Symbolic Logic 22, 250–268 (1957)
Detlefs, D., Nelson, G., Saxe, J.: Simplify theorem prover, http://research.compaq.com/SRC/esc/Simplify.html
Filliâtre, J.-C., Owre, S., Rueß, H., Shankar, N.: ICS: Integrated canonizer and solver. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 246–249. Springer, Heidelberg (2001)
Flanagan, C., Joshi, R., Ou, X., Saxe, J.B.: Theorem proving using lazy proof explication. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 355–367. Springer, Heidelberg (2003)
Gallier, J.H.: Logic for Computer Science: Foundations of Automatic Theorem Proving. John Wiley & Sons, New York (1987)
Ganesh, V., Berezin, S., Tinelli, C., Dill, D.L.: Combination results for many-sorted theories with overlapping signatures. Technical report, Department of Computer Science, Stanford University (2004)
Gerhardy, P.: Refined complexity analysis of cut elimination. In: Baaz, M., Makowsky, J.A. (eds.) CSL 2003. LNCS, vol. 2803, pp. 212–225. Springer, Heidelberg (2003)
Takeuti, G.: Studies in Logic, vol. 81. Elsevier/North Holland, Amsterdam (1975)
Gulwani, S., Tiwari, A.: Unpublished manuscript
Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from proofs. In: POPL, pp. 232–244 (2004)
McMillan, K.L.: Interpolation and SAT-based model checking. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 1–13. Springer, Heidelberg (2003)
McMillan, K.L.: An interpolating theorem prover. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 16–30. Springer, Heidelberg (2004)
Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM Transactions on Programming Languages and Systems 1(2), 245–257 (1979)
Nelson, G., Oppen, D.C.: Fast decision procedures based on congruence closure. J. ACM 27(2), 356–364 (1980)
Oppen, D.C.: Complexity, convexity and combinations of theories. Theoretical Computer Science 12, 291–302 (1980)
Pudlák, P.: Lower bounds for resolution and cutting planes proofs and monotone computations. J. of Symbolic Logic 62(3), 981–998 (1995)
Kleene, S.C.: Mathematical Logic. Wiley Interscience, New York (1967)
Yorsh, G., Musuvathi, M.: A combination method for generating interpolants. Technical Report MSR-TR-2004-108, Microsoft Research (October 2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Yorsh, G., Musuvathi, M. (2005). A Combination Method for Generating Interpolants. In: Nieuwenhuis, R. (eds) Automated Deduction – CADE-20. CADE 2005. Lecture Notes in Computer Science(), vol 3632. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11532231_26
Download citation
DOI: https://doi.org/10.1007/11532231_26
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-28005-7
Online ISBN: 978-3-540-31864-4
eBook Packages: Computer ScienceComputer Science (R0)