Description

This page accompanies a short paper that was presented at IWC 2018. We present an ongoing formalization effort (in Isabelle/HOL, on top of IsaFoR) aimed at formalizing the decidability of the first-order logic of left-linear, right-ground term rewrite systems. At this point, we have constructions that suffice for confluence, but work on executable code for them is still in progress.

Links

• browse theory files online
• download FORTissimo theory files (last updated: 2018-05-25)
• get IsaFoR 2.33