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 joinable. 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.

BibTeX

@inproceedings{CSTS-CADE17,
 author    = "Christian Sternagel and Thomas Sternagel",
 title     = "Certifying Confluence of Quasi-Decreasing Strongly
Deterministic Conditional Term Rewrite Systems",
 booktitle = "Proceedings of the 26th International Confluence on
Automated Deduction (CADE-26)",
 editor    = "de Moura L.",
 series    = "Lecture Notes in Computer Science",
 volume    = 10395,
 pages     = "413-431",
 year      = 2017,
 doi       = "10.1007/978-3-319-63046-5_26"
}