Ground interpolation for the theory of equality

Details Ground interpolation for the theory of equality Ground interpolation for the theory of equality

2011-11-23

arxiv.org/abs/1111.5652v2

LMCS 8 (1:6) 2012

Computer Science

Logic in Computer Science

Scientific paper

10.2168/LMCS-8(1:6)2012

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.

Affiliated with

Also associated with

No associations

Rating

Ground interpolation for the theory of equality does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with Ground interpolation for the theory of equality, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Ground interpolation for the theory of equality will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-156375