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.
Author supplied keywords
Cite
CITATION STYLE
Lochmann, A., & Middeldorp, A. (2020). Formalized Proofs of the Infinity and Normal Form Predicates in the First-Order Theory of Rewriting. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 12079 LNCS, pp. 178–194). Springer. https://doi.org/10.1007/978-3-030-45237-7_11
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
