LIPIcs.RTA.2015.269.pdf
- Filesize: 0.63 MB
- 16 pages
Document
Certified Rule Labeling
Authors
-
Part of:
Volume:
26th International Conference on Rewriting Techniques and Applications (RTA 2015)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Conference on Rewriting Techniques and Applications (RTA) - License:
Creative Commons Attribution 3.0 Unported license
- Publication Date: 2015-06-18
Cite AsGet BibTex
Julian Nagele and Harald Zankl. Certified Rule Labeling. In 26th International Conference on Rewriting Techniques and Applications (RTA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 36, pp. 269-284, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
https://doi.org/10.4230/LIPIcs.RTA.2015.269
https://doi.org/10.4230/LIPIcs.RTA.2015.269
Abstract
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 for the first time. The power of the method is illustrated by an experimental evaluation on a (standard) collection of confluence problems.
Keywords
- term rewriting
- confluence
- decreasing diagrams
- certification
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads