FORTissimo — IWC 2018  

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.