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...
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 |
Ejemplares similares
-
Certifying Proofs in the First-Order Theory of Rewriting
por: Mitterwallner, Fabian, et al.
Publicado: (2021) -
First-Order Theory of Rewriting for Linear Variable-Separated Rewrite Systems: Automation, Formalization, Certification
por: Middeldorp, Aart, et al.
Publicado: (2023) -
Truth, proof and infinity: a theory of constructions and constructive reasoning
por: Hintikka, Jaakko, et al.
Publicado: (2010) -
Roads to infinity: the mathematics of truth and proof
por: Stillwell, John C
Publicado: (2010) -
Theorem proving with first-order predicate logic, 3
por: Humpert, Benedikt
Publicado: (1987)