First-Order Theory of Rewriting for Linear Variable-Separated Rewrite Systems: Automation, Formalization, Certification
Aart Middeldorp, Alexander Lochmann, Fabian MitterwallnerJournal of Automated Reasoning 67, 2023.
Abstract
The first-order theory of rewriting is decidable for linear variable-separated rewrite systems. We present a new decision procedure which is the basis of FORT, a decision and synthesis tool for properties expressible in the theory. The decision procedure is based on tree automata techniques and verified in Isabelle. Several extensions make the theory more expressive and FORT more versatile. We present a certificate language that enables the output of FORT to be certified by the certifier FORTify generated from the formalization, and we provide extensive experiments.
BibTeX
@article{AMALFM-JAR23,
author = "Aart Middeldorp and Alexander Lochmann and Fabian
Mitterwallner",
title = "First-Order Theory of Rewriting for Linear Variable-Separated
Rewrite Systems: Automation, Formalization, Certification",
journal = "Journal of Automated Reasoning",
volume = 67,
number = 14,
pages = "1--76",
year = 2023,
doi = "10.1007/s10817-023-09661-7"
}