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

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