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.

BibTeX

@inproceedings{FMPR-IWC18,
  author    = "Bertram Felgenhauer and Aart Middeldorp and
               T.V.H. Prathamesh and Franziska Rapp",
  title     = "Towards a Verified Decision Procedure for Confluence of
               Ground Term Rewrite Systems in Isabelle/HOL",
  booktitle = "Proceedings of the 7th International Workshop on Confluence",
  editor    = "Bertram Felgenhauer and Jakob Grue Simonsen",
  pages     = "46--50",
  year      = 2018
}