Logo image
Back
Ground Interpolation for the Theory of Equality
Book chapter   Open access   Peer reviewed

Ground Interpolation for the Theory of Equality

Alexander Fuchs, Amit Goel, Jim Grundy, Sava Krstić and Cesare Tinelli
Tools and Algorithms for the Construction and Analysis of Systems, pp.413-427
Lecture Notes in Computer Science, Springer Berlin Heidelberg
2009
DOI: 10.1007/978-3-642-00768-2_34
url
https://doi.org/10.1007/978-3-642-00768-2_34View
Published (Version of record) Open Access

Abstract

Given a theory \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$\mathcal{T}$\end{document} and two formulas A and B jointly unsatisfiable in \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$\mathcal{T}$\end{document}, 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 \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$\mathcal{T}$\end{document}, and (iii) it is unsatisfiable with B in \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$\mathcal{T}$\end{document}. Theory interpolants are used in model checking to accelerate the computation of reachability relations. We present a novel method for computing ground interpolants for ground formulas in the theory of equality. Our algorithm computes interpolants from colored congruence graphs representing derivations in the theory of equality. 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.
 Horn Clause Interpolation Property Model Check Parent Path Resolution Proof

Details

Metrics

15 Record Views
Logo image