Formalized Confluence of Quasi-Decreasing, Strongly Deterministic Conditional TRSs

2016/09/12 by Thomas Sternagel, Sternagel, Thomas, Christian Sternagel +1
Computer Science · #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems

paper · pdf · doi:10.48550/arxiv.1609.03341

openalex publication_date 2016/09/12 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

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ía-Sáenz.

Related

• Confluence by Critical Pair Analysis Revisited (Extended Version)
• Confluence of conditional rewriting modulo
• Level-Confluence of 3-CTRSs in Isabelle/HOL
• Confluence by Decreasing Diagrams -- Formalized
• The Orientation Boundary for Step-Duplicating Recursors: Mechanized Impossibility, Escape, and Certification