Ground interpolation for the theory of equality

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...

Full description

Bibliographic Details
Main Authors: Alexander Fuchs, Amit Goel, Jim Grundy, Sava Krstić, Cesare Tinelli
Format: Article
Language:English
Published: Logical Methods in Computer Science e.V. 2012-02-01
Series:Logical Methods in Computer Science
Subjects:
Online Access:https://lmcs.episciences.org/709/pdf