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...
| Main Authors: | , , , , |
|---|---|
| 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 |
| _version_ | 1827322963475562496 |
|---|---|
| author | Alexander Fuchs Amit Goel Jim Grundy Sava Krstić Cesare Tinelli |
| author_facet | Alexander Fuchs Amit Goel Jim Grundy Sava Krstić Cesare Tinelli |
| author_sort | Alexander Fuchs |
| collection | DOAJ |
| description | 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. |
| first_indexed | 2024-04-25T01:37:09Z |
| format | Article |
| id | doaj.art-e88e7fcf97d74d07b14c8da93311f30d |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:37:09Z |
| publishDate | 2012-02-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-e88e7fcf97d74d07b14c8da93311f30d2024-03-08T09:27:54ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742012-02-01Volume 8, Issue 110.2168/LMCS-8(1:6)2012709Ground interpolation for the theory of equalityAlexander FuchsAmit GoelJim GrundySava KrstićCesare Tinellihttps://orcid.org/0000-0002-6726-775XTheory 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.https://lmcs.episciences.org/709/pdfcomputer science - logic in computer scienced.2.4, f.3.1, f.4.1, i.2.3 |
| spellingShingle | Alexander Fuchs Amit Goel Jim Grundy Sava Krstić Cesare Tinelli Ground interpolation for the theory of equality Logical Methods in Computer Science computer science - logic in computer science d.2.4, f.3.1, f.4.1, i.2.3 |
| title | Ground interpolation for the theory of equality |
| title_full | Ground interpolation for the theory of equality |
| title_fullStr | Ground interpolation for the theory of equality |
| title_full_unstemmed | Ground interpolation for the theory of equality |
| title_short | Ground interpolation for the theory of equality |
| title_sort | ground interpolation for the theory of equality |
| topic | computer science - logic in computer science d.2.4, f.3.1, f.4.1, i.2.3 |
| url | https://lmcs.episciences.org/709/pdf |
| work_keys_str_mv | AT alexanderfuchs groundinterpolationforthetheoryofequality AT amitgoel groundinterpolationforthetheoryofequality AT jimgrundy groundinterpolationforthetheoryofequality AT savakrstic groundinterpolationforthetheoryofequality AT cesaretinelli groundinterpolationforthetheoryofequality |