Abstract
In Decreasing-Diagrams it was formally proved that the decreasing diagrams method is sound for proving confluence: if a binary relation $r$ has $LD$ property defined in Decreasing-Diagrams, then it has $CR$ property defined in Abstract-Rewriting.
In this formal theory it is proved that if the cardinality of $r$ does not exceed the first uncountable cardinal, then $r$ has $CR$ property if and only if $r$ has $LD$ property. As a consequence, the decreasing diagrams method is complete for proving confluence of relations of the least uncountable cardinality.
A paper that describes details of this proof has been submitted to the FSCD 2025 conference.
License
Topics
Related publications
- Ivanov, I. (2024). Formal proof of completeness of the decreasing diagrams method for proving confluence of relations of the least uncountable cardinality. Zenodo. https://doi.org/10.5281/ZENODO.14254256
- Ivanov, I. (2025). Modified version of a formal proof of completeness of the decreasing diagrams method for proving confluence of relations of the least uncountable cardinality. Zenodo. https://doi.org/10.5281/ZENODO.15190469
- Ivanov, I. (2025). Formalization of a confluent abstract rewriting system of the least uncountable cardinality outside of the class DCR2. Zenodo. https://doi.org/10.5281/ZENODO.14740062
- Ivanov, I. (2024). Formalization of an abstract rewriting system in the class DCR3\DCR2. Zenodo. https://doi.org/10.5281/ZENODO.11571490
- V. van Oostrom. Confluence by decreasing diagrams. Theoretical computer science, Vol. 126, P. 259-280, 1994.
- I. Ivanov. On Non-triviality of the Hierarchy of Decreasing Church-Rosser Abstract Rewriting Systems. Proceedings of the 13th International Workshop on Confluence, P. 30-35, 2024.