| dc.contributor.author | Nagele, J | en_US |
| dc.contributor.author | Zankl, H | en_US |
| dc.contributor.author | 26th International Conference on Rewriting Techniques and Applications | en_US |
| dc.date.accessioned | 2018-05-10T13:21:37Z | |
| dc.date.available | 2015-04-08 | en_US |
| dc.date.issued | 2015-06-01 | en_US |
| dc.date.submitted | 2018-05-02T16:52:43.390Z | |
| dc.identifier.isbn | 9783939897859 | en_US |
| dc.identifier.issn | 1868-8969 | en_US |
| dc.identifier.uri | http://qmro.qmul.ac.uk/xmlui/handle/123456789/37344 | |
| dc.description.abstract | © Julian Nagele and Harald Zankl. 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. | en_US |
| dc.format.extent | 269 - 284 | en_US |
| dc.rights | This article is distributed under the terms of the Creative Commons Attribution License (CC-BY 4.0), which permits any use, distribution and reproduction in any medium, provided the original author(s) and source are credited. | |
| dc.title | Certified rule labeling | en_US |
| dc.type | Conference Proceeding | |
| dc.rights.holder | © The Author(s) 2015 | |
| dc.identifier.doi | 10.4230/LIPIcs.RTA.2015.269 | en_US |
| pubs.notes | No embargo | en_US |
| pubs.publication-status | Published | en_US |
| pubs.volume | 36 | en_US |
| dcterms.dateAccepted | 2015-04-08 | en_US |
