Ground Interpolation for the Theory of Equality

Cesare Tinelli (University of Iowa)

Info

Date	3rd July 2009 (week -, Trinity Term 2009)
Time	11:30
Place	Room 478, Oxford University Computing Laboratory

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 A and B, (ii) it is entailed by A in T, and (iii) it is unsatisfiable with B in T . Theory interpolants are used in model checking, among other things, to accelerate the computation of reachability relations. This talks presents a novel method for computing ground interpolants for ground formulas in the theory of equality.

The method computes 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, the method is able to derive interpolants that are simpler (being always conjunctions of Horn clauses) and smaller than those generated by other tools.

This is joint work with Alexander Fuchs, Amit Goel, Jim Grundy, and Sava Krstic.