Cargando…

Formalized Proofs of the Infinity and Normal Form Predicates in the First-Order Theory of Rewriting

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 constr...

Descripción completa

Detalles Bibliográficos
Autores principales: Lochmann, Alexander, Middeldorp, Aart
Formato: Online Artículo Texto
Lenguaje:English
Publicado: 2020
Materias:
Acceso en línea:https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7480710/
http://dx.doi.org/10.1007/978-3-030-45237-7_11