Confluence Criteria for Logically Constrained Rewrite Systems (Full Version)

TL;DR

This paper extends known confluence criteria to logically constrained rewrite systems, introduces a new tool called crest for automated confluence checking, and provides experimental results demonstrating its effectiveness.

Contribution

It adapts strongly-closed and parallel-closed critical pair criteria to logically constrained rewriting and develops crest, a tool for automated confluence analysis.

Findings

Successful implementation of confluence criteria in crest

Experimental validation shows effectiveness of the approach

Extension of classical criteria to new logical setting

Abstract

Numerous confluence criteria for plain term rewrite systems are known. For logically constrained rewrite system, an attractive extension of term rewriting in which rules are equipped with logical constraints, much less is known. In this paper we extend the strongly-closed and (almost) parallel-closed critical pair criteria of Huet and Toyama to the logically constrained setting. We discuss the challenges for automation and present crest, a new tool for logically constrained rewriting in which the confluence criteria are implemented, together with experimental data.