cl-banner

A Verified Decision Procedure for the First-Order Theory of Rewriting for Linear Variable-Separated Rewrite Systems

Alexander Lochmann, Aart Middeldorp, Fabian Mitterwallner, Bertram Felgenhauer

10th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2021), pp. 250 – 263, 2021.

Abstract

The first-order theory of rewriting is a decidable theory for finite left-linear right-ground rewrite systems, implemented in FORT. We present a formally verified variant of the decision procedure for the class of linear variable-separated rewrite systems. This variant supports a more expressive theory and is based on the concept of anchored ground tree transducers. The correctness of the decision procedure is verified by a formalization in Isabelle/HOL on top of the Isabelle Formalization of Rewriting (IsaFoR)

 

  PDF |    doi:10.1145/3437992.3439918

BibTeX 

@inproceedings{ALAMFMBF-CPP21,
author = "Alexander Lochmann and Aart Middeldorp and Fabian
Mitterwallner and Bertram Felgenhauer",
title = "A Verified Decision Procedure for the First-Order Theory of
Rewriting for Linear Variable-Separated Rewrite Systems",
booktitle = "Proceedings of the 10th International {ACM} {SIGPLAN}
International Conference on Certified Programs and Proofs",
publisher = "ACM",
editors = "Cătălin Hriţcu and Andrei Popescu",
pages = "250--263",
doi = "10.1145/3437992.3439918",
year = 2021
}
Nach oben scrollen