Formalized Confluence of Quasi-Decreasing, Strongly Deterministic Conditional TRSs
Thomas Sternagel, Christian Sternagel
TL;DR
This paper formalizes a characterization of confluence in a specific class of conditional term rewrite systems using Isabelle/HOL, providing a rigorous proof framework for these properties.
Contribution
It provides the first formalization of the confluence criteria for quasi-reductive strongly deterministic conditional TRSs in Isabelle/HOL.
Findings
Formal proof of confluence characterization
Implementation in Isabelle/HOL
Enhanced rigor in confluence analysis
Abstract
We present an Isabelle/HOL formalization of a characterization of confluence for quasi-reductive strongly deterministic conditional term rewrite systems, due to Avenhaus and Lor\'ia-S\'aenz.
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 · Formal Methods in Verification · Logic, Reasoning, and Knowledge