Confluence by Decreasing Diagrams -- Formalized

TL;DR

This paper formalizes decreasing diagrams in Isabelle, proving that locally decreasing abstract rewrite systems are confluent, and explores both valley and conversion versions of decreasing diagrams.

Contribution

It provides a formalized proof framework for decreasing diagrams in Isabelle, enhancing the rigor of confluence proofs in rewriting systems.

Findings

Mechanical proofs confirm confluence for locally decreasing systems

Formalization covers valley and conversion versions

Enhances rigor of confluence proofs in rewriting systems

Abstract

This paper presents a formalization of decreasing diagrams in the theorem prover Isabelle. It discusses mechanical proofs showing that any locally decreasing abstract rewrite system is confluent. The valley and the conversion version of decreasing diagrams are considered.