Journal article
GROUND INTERPOLATION FOR THE THEORY OF EQUALITY
Logical methods in computer science, Vol.8(1), 6
01/01/2012
DOI: 10.2168/LMCS-8(1:06)2012
Abstract
Given a theory T and two formulas A and B jointly unsatisfiable in T, a theory interpolant of A and B is a formula I such that (i) its non-theory symbols are shared by both A and B, (ii) it is entailed by A in T, and (iii) it is unsatisfiable with B in T. Theory interpolation has found several successful applications in model checking. We present a novel method for computing interpolants for ground formulas in the theory of equality. The method produces interpolants from colored congruence graphs representing derivations in that theory. These graphs can be produced by conventional congruence closure algorithms in a straightforward manner. By working with graphs, rather than at the level of individual proof steps, we are able to derive interpolants that are pleasingly simple (conjunctions of Horn clauses) and smaller than those generated by other tools. Our interpolation method can be seen as a theory-specific implementation of a cooperative interpolation game between two provers. We present a generic version of the interpolation game, parametrized by the theory T, and define a general method to extract runs of the game from proofs in T and then generate interpolants from these runs.
Details
- Title: Subtitle
- GROUND INTERPOLATION FOR THE THEORY OF EQUALITY
- Creators
- Alexander Fuchs - Univ Iowa, Dept Comp Sci, Iowa City, IA 52242 USAAmit Goel - Intel Corp, Strateg CAD Labs, Santa Clara, CA 95051 USAJim Grundy - Intel Corp, Strateg CAD Labs, Santa Clara, CA 95051 USASava Krstic - Intel Corp, Strateg CAD Labs, Santa Clara, CA 95051 USACesare Tinelli - Univ Iowa, Dept Comp Sci, Iowa City, IA 52242 USA
- Resource Type
- Journal article
- Publication Details
- Logical methods in computer science, Vol.8(1), 6
- Publisher
- Logical Methods Computer Science E V
- DOI
- 10.2168/LMCS-8(1:06)2012
- ISSN
- 1860-5974
- eISSN
- 1860-5974
- Number of pages
- 23
- Grant note
- FA9550-09-1-0517 / AFOSR; United States Department of Defense; Air Force Office of Scientific Research (AFOSR)
- Language
- English
- Date published
- 01/01/2012
- Academic Unit
- Computer Science
- Record Identifier
- 9984259490702771
Metrics
8 Record Views