Confluence Framework: Proving Confluence with CONFident

Abstract This paper describes CONFident, a tool which is able to automatically prove and disprove confluence of variants of rewrite systems: term rewriting systems, conditional term rewriting systems (using join, oriented, or semi-equational semantics), and context-sensitive term rewriting systems. We introduce a new proof framework to generate proof trees by combining different techniques for proving confluence (including modular decompositions, checking joinability of (conditional) critical pairs, transformations, etc.). We also use external tools for proving termination and operational termination ( mu-term ), or feasibility ( infChecker ) and deducibility ( Prover9 ).

Authors

• Raúl Gutiérrez
• Miguel Vítores
• Salvador Lucas

Keywords

No keywords are indexed for this paper.