Level-Confluence of 3-CTRSs in Isabelle/HOL
Christian Sternagel, Thomas Sternagel
TL;DR
This paper formalizes in Isabelle/HOL a proof that a specific class of conditional rewrite systems exhibits level-confluence, enhancing the rigor and clarity of the original proof by Suzuki, Middeldorp, and Ida.
Contribution
It provides a formal Isabelle/HOL proof of level-confluence for a class of conditional rewrite systems, with detailed formalization and clarified definitions.
Findings
Formal proof of level-confluence in Isabelle/HOL
Enhanced understanding of conditional rewrite systems
Alignment with original proof structure
Abstract
We present an Isabelle/HOL formalization of an earlier result by Suzuki, Middeldorp, and Ida; namely that a certain class of conditional rewrite systems is level-confluent. Our formalization is basically along the lines of the original proof, from which we deviate mostly in the level of detail as well as concerning some basic definitions.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · semigroups and automata theory · Logic, Reasoning, and Knowledge