Certifying Proofs in the First-Order Theory of Rewriting
Fabian Mitterwallner, Alexander Lochmann, Aart Middeldorp, and Bertram
Felgenhauer
Proceedings of the 27th International Conference on Tools and Algorithms
for the Construction and Analysis of Systems (TACAS 2021), Lecture Notes in
Computer Science 12652, pp. 127 – 144, 2021
Abstract
The first-order theory of rewriting is a decidable theory for linear variable-separated rewrite systems. The decision procedure is based on tree automata techniques and recently we completed a formalization in the Isabelle proof assistant. In this paper we present a certificate language that enables the output of software tools implementing the decision procedure to be formally verified. To show the feasibility of this approach, we present FORT-h, a reincarnation of the decision tool FORT with certifiable output, and the formally verified certifier FORTify.BibTeX Entry
@inproceedings{MLMF-TACAS21,
author = "Fabian Mitterwallner and Alexander Lochmann and Aart
Middeldorp and Bertram Felgenhauer",
title = "Certifying Proofs in the First-Order Theory of Rewriting",
booktitle = "Proceedings of the 27th International Conference on Tools
and Algorithms for the Construction and Analysis of Systems",
editor = "Jan Friso Groote and Kim Guldstrand Larsen",
series = "Lecture Notes in Computer Science",
volume = 12652,
pages = "127--144",
year = 2021,
doi = "10.1007/978-3-030-72013-1_7"
}