Proving Confluence in the Confluence Framework with CONFident

What is it about?

This article describes the *Confluence Framework*, a novel framework for proving and disproving confluence using a divide-and-conquer modular strategy, and its implementation in CONFident. Using this approach, we are able to automatically prove and disprove confluence of *Generalized Term Rewriting Systems*. This includes, as particular cases, several variants of rewrite systems such as (context-sensitive) *term rewriting systems*, *string rewriting systems*, and (context-sensitive) *conditional term rewriting systems*.

Featured Image

Why is it important?

It is a step forward in the definition of practical techniques for program analysis. The framework is implemented in the tool CONFident, which is publicly available on the web (http://zenon.dsic.upv.es/confident/)