FORT 0.2: Confluence Properties on Open Terms in the First-Order Theory of Rewriting

• Aart Middeldorp
• University of Innsbruck
• Homepage

The first-order theory of rewriting is decidable for finite left-linear right-ground rewrite systems. The decision procedure for this theory is based on tree automata techniques and implemented in FORT. FORT offers the possibility to synthesize rewrite systems that satisfy properties that are expressible in the first-order theory of rewriting.

Tree automata operate on ground terms. Consequently, variables in formulas range over ground terms and hence the properties that FORT is able to decide are restricted to ground terms. Whereas for termination and normalization this makes no difference, for other properties it does, even for left-linear right-ground rewrite systems. This raises the question how one can use FORT to decide properties on open terms. We show that for properties related to confluence it suffices to add one or two fresh constants. We furthermore provide sufficient conditions which obviate the need for additional constants. These results have been implemented in FORT 0.2.

In the talk, which is based on joint work with Franziska Rapp, I will explain the decision and synthesis algorithms implemented in FORT, before discussing the new results for deciding properties on open terms. The talk is concluded with a comparison with AGCP, a tool developed by Aoto and Toyama for checking ground-confluence of many-sorted rewrite systems.