Formalized Proofs of the Infinity and Normal Form Predicates in the First-Order Theory of Rewriting
Alexander Lochmann and Aart Middeldorp
Proceedings of the 26th International Conference on Tools and Algorithms
for the Construction and Analysis of Systems (TACAS 2020), Lecture Notes in
Computer Science 12079, pp. 178 – 194, 2020
Abstract
We present a formalized proof of the regularity of the infinity predicate on ground terms. This predicate plays an important role in the first-order theory of rewriting because it allows to express the termination property. The paper also contains a formalized proof of a direct tree automaton construction of the normal form predicate, due to Comon.BibTeX Entry
@inproceedings{LM-TACAS20,
author = "Alexander Lochmann and Aart Middeldorp",
title = "Formalized Proofs of the Infinity and Normal Form Predicates
in the First-Order Theory of Rewriting",
booktitle = "Proceedings of the 26th International Conference on Tools
and Algorithms for the Construction and Analysis of Systems",
editor = "Armin Biere and Dave Parker",
series = "Lecture Notes in Computer Science",
volume = 12079,
pages = "178--194",
year = 2020,
doi = "10.1007/978-3-030-45237-7_11"
}