Description
This page accompanies a paper that was presented at TACAS 2020.
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. The contributions of the paper are the formalization of the infinity and normal form predicates.