Towards a Verified Decision Procedure for Confluence of Ground Term Rewrite Systems in Isabelle/HOL

Title:Towards a Verified Decision Procedure for Confluence of Ground Term Rewrite Systems in Isabelle/HOL

Authors:Bertram Felgenhauer, Aart Middeldorp, T. V. H. Prathamesh and Franziska Rapp

Conference:IWC 2018

Tags:confluence, formalization, ground systems and term rewriting

Abstract:

Confluence is a decidable property of ground rewrite systems. We present a formalization effort in Isabelle/HOL of the decision procedure based on ground tree transducers.