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:
Article
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
_version_ 1783580464635707392
author Lochmann, Alexander
Middeldorp, Aart
author_facet Lochmann, Alexander
Middeldorp, Aart
author_sort Lochmann, Alexander
collection PubMed
description 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.
format Online
Article
Text
id pubmed-7480710
institution National Center for Biotechnology Information
language English
publishDate 2020
record_format MEDLINE/PubMed
spelling pubmed-74807102020-09-10 Formalized Proofs of the Infinity and Normal Form Predicates in the First-Order Theory of Rewriting Lochmann, Alexander Middeldorp, Aart Tools and Algorithms for the Construction and Analysis of Systems Article 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. 2020-03-13 /pmc/articles/PMC7480710/ http://dx.doi.org/10.1007/978-3-030-45237-7_11 Text en © The Author(s) 2020 Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made. The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
spellingShingle Article
Lochmann, Alexander
Middeldorp, Aart
Formalized Proofs of the Infinity and Normal Form Predicates in the First-Order Theory of Rewriting
title Formalized Proofs of the Infinity and Normal Form Predicates in the First-Order Theory of Rewriting
title_full Formalized Proofs of the Infinity and Normal Form Predicates in the First-Order Theory of Rewriting
title_fullStr Formalized Proofs of the Infinity and Normal Form Predicates in the First-Order Theory of Rewriting
title_full_unstemmed Formalized Proofs of the Infinity and Normal Form Predicates in the First-Order Theory of Rewriting
title_short Formalized Proofs of the Infinity and Normal Form Predicates in the First-Order Theory of Rewriting
title_sort formalized proofs of the infinity and normal form predicates in the first-order theory of rewriting
topic Article
url https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7480710/
http://dx.doi.org/10.1007/978-3-030-45237-7_11
work_keys_str_mv AT lochmannalexander formalizedproofsoftheinfinityandnormalformpredicatesinthefirstordertheoryofrewriting
AT middeldorpaart formalizedproofsoftheinfinityandnormalformpredicatesinthefirstordertheoryofrewriting

Ejemplares similares