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
Paper Information
| 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 |
| Proceedings: | IWC Final papers |
| Editors: | Jakob Grue Simonsen and Bertram Felgenhauer |
| Keywords: | confluence, term rewriting, formalization, ground systems |
| Abstract: | 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. |
| Pages: | 5 |
| Talk: | Jul 07 14:30 (Session 28F: Term Rewriting) |
| Paper: |  |