Book chapter
Ground Interpolation for Combined Theories
Automated Deduction – CADE-22, pp.183-198
Lecture Notes in Computer Science, Springer Berlin Heidelberg
2009
DOI: 10.1007/978-3-642-02959-2_16
Abstract
We give a method for modular generation of ground interpolants in modern SMT solvers supporting multiple theories. Our method uses a novel algorithm to modify the proof tree obtained from an unsatifiability run of the solver into a proof tree without occurrences of troublesome “uncolorable” literals. An interpolant can then be readily generated using existing procedures. The principal advantage of our method is that it places few restrictions (none for convex theories) on the search strategy of the solver. Consequently, it is straightforward to implement and enables more efficient interpolating SMT solvers. In the presence of non-convex theories our method is incomplete, but still more general than previous methods.
Details
- Title: Subtitle
- Ground Interpolation for Combined Theories
- Creators
- Amit Goel - IntelSava Krstić - IntelCesare Tinelli - University of Iowa
- Resource Type
- Book chapter
- Publication Details
- Automated Deduction – CADE-22, pp.183-198
- Publisher
- Springer Berlin Heidelberg; Berlin, Heidelberg
- Series
- Lecture Notes in Computer Science
- DOI
- 10.1007/978-3-642-02959-2_16
- eISSN
- 1611-3349
- ISSN
- 0302-9743
- Language
- English
- Date published
- 2009
- Academic Unit
- Computer Science
- Record Identifier
- 9984259420502771
Metrics
18 Record Views