cl-banner

Property Invariant Embedding for Automated Reasoning

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

8th ACM SIGPLAN International Conference on Certified Programs and Proofs, pp. 132 – 143, 2019.

Abstract

It is well known that (ground) confluence is a decidable property of ground term rewrite systems, and that this extends to larger classes. Here we present a formally verified ground confluence checker for linear, variable-separated rewrite systems. To this end, we formalize procedures for ground tree transducers and so-called RRn relations. The ground confluence checker is an important milestone on the way to formalizing the decidability of the first-order theory of ground rewriting for linear, variable-separated rewrite systems. It forms the basis for a formalized confluence checker for left-linear, right-ground systems.

 

  PDF |    doi:10.1145/3293880.3294098  

BibTeX 

@inproceedings{BFAMPRFR-CPP19,
author = "Bertram Felgenhauer and Aart Middeldorp and
T.V.H. Prathamesh and Franziska Rapp",
title = "A Verified Ground Confluence Tool for Linear
Variable-Separated Rewrite Systems in {Isabelle/HOL}",
booktitle = "Proceedings of the 8th International {ACM SIGPLAN}
International Conference on Certified Programs and
Proofs",
pages = "132--143",
publisher = "ACM",
doi = "10.1145/3293880.3294098",
year = 2019
}
Nach oben scrollen