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).

BibTeX Entry

@inproceedings{LMMF-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",
 editors   = "Cătălin Hriţcu and Andrei Popescu",
 pages     = "250--263",
 doi       = "10.1145/3437992.3439918",
 year      = 2021
}