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

@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
}