Towards a Verified Decision Procedure for Confluence of Ground Term Rewrite Systems in Isabelle/HOL
Bertram Felgenhauer, Aart Middeldorp, T. V. H. Prathamesh, and Franziska
Rapp
Proceedings of the 7th International Workshop on Confluence (IWC 2018),
pp. 46 – 50, 2018
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 Entry
@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
}