Certifying Confluence Proofs via Relative Termination and Rule Labeling
The rule labeling heuristic aims to establish confluence of (left-)linear term rewrite systems via decreasing diagrams. We present a formalization of a confluence criterion based on the interplay of relative termination and the rule labeling in the theorem prover Isabelle. Moreover, we report on the...
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2017-05-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/3654/pdf |
| _version_ | 1798018250196385792 |
|---|---|
| author | Julian Nagele Bertram Felgenhauer Harald Zankl |
| author_facet | Julian Nagele Bertram Felgenhauer Harald Zankl |
| author_sort | Julian Nagele |
| collection | DOAJ |
| description | The rule labeling heuristic aims to establish confluence of (left-)linear
term rewrite systems via decreasing diagrams. We present a formalization of a
confluence criterion based on the interplay of relative termination and the
rule labeling in the theorem prover Isabelle. Moreover, we report on the
integration of this result into the certifier CeTA, facilitating the checking
of confluence certificates based on decreasing diagrams. The power of the
method is illustrated by an experimental evaluation on a (standard) collection
of confluence problems. |
| first_indexed | 2024-04-11T16:20:42Z |
| format | Article |
| id | doaj.art-423e266ddf3145588287603e7a288b3f |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-11T16:20:42Z |
| publishDate | 2017-05-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-423e266ddf3145588287603e7a288b3f2022-12-22T04:14:22ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742017-05-01Volume 13, Issue 210.23638/LMCS-13(2:4)20173654Certifying Confluence Proofs via Relative Termination and Rule LabelingJulian NageleBertram FelgenhauerHarald ZanklThe rule labeling heuristic aims to establish confluence of (left-)linear term rewrite systems via decreasing diagrams. We present a formalization of a confluence criterion based on the interplay of relative termination and the rule labeling in the theorem prover Isabelle. Moreover, we report on the integration of this result into the certifier CeTA, facilitating the checking of confluence certificates based on decreasing diagrams. The power of the method is illustrated by an experimental evaluation on a (standard) collection of confluence problems.https://lmcs.episciences.org/3654/pdfcomputer science - logic in computer sciencef.2f.4 |
| spellingShingle | Julian Nagele Bertram Felgenhauer Harald Zankl Certifying Confluence Proofs via Relative Termination and Rule Labeling Logical Methods in Computer Science computer science - logic in computer science f.2 f.4 |
| title | Certifying Confluence Proofs via Relative Termination and Rule Labeling |
| title_full | Certifying Confluence Proofs via Relative Termination and Rule Labeling |
| title_fullStr | Certifying Confluence Proofs via Relative Termination and Rule Labeling |
| title_full_unstemmed | Certifying Confluence Proofs via Relative Termination and Rule Labeling |
| title_short | Certifying Confluence Proofs via Relative Termination and Rule Labeling |
| title_sort | certifying confluence proofs via relative termination and rule labeling |
| topic | computer science - logic in computer science f.2 f.4 |
| url | https://lmcs.episciences.org/3654/pdf |
| work_keys_str_mv | AT juliannagele certifyingconfluenceproofsviarelativeterminationandrulelabeling AT bertramfelgenhauer certifyingconfluenceproofsviarelativeterminationandrulelabeling AT haraldzankl certifyingconfluenceproofsviarelativeterminationandrulelabeling |