cl-banner

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

Bertram Felgenhauer, Aart Middeldorp, T. V. H. Prathamesh, 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.

 

  PDF

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
}
Nach oben scrollen