Skip to main content
Conference ProceedingsOPEN ACCESS

Certifying confluence of quasi-decreasing strongly deterministic conditional term rewrite systems

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (2017) 10395 LNAI 413-431
DOI: 10.1007/978-3-319-63046-5_26
0Citations
Citations of this article
1Readers
Mendeley users who have this article in their library.

This article is free to access.

Abstract

We formalize a confluence criterion for the class of quasi-decreasing strongly deterministic conditional term rewrite systems in Isabelle/HOL: confluence follows if all conditional critical pairs are join-able. However, quasi-decreasingness, strong determinism, and joinability of conditional critical pairs are all undecidable in general. Therefore, we also formalize sufficient criteria for those properties, which we incorporate into the general purpose certifier CeTA as well as the confluence checker ConCon for conditional term rewrite systems.

Cite

CITATION STYLE

APA

Sternagel, C., & Sternagel, T. (2017). Certifying confluence of quasi-decreasing strongly deterministic conditional term rewrite systems. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 10395 LNAI, pp. 413–431). Springer Verlag. https://doi.org/10.1007/978-3-319-63046-5_26

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free