Conference ProceedingsOPEN ACCESS

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

Lecture Notes in Computer Science (2020) 12079 LNCS 178-194
DOI: 10.1007/978-3-030-45237-7_11
2Citations
Citations of this article
2Readers
Mendeley users who have this article in their library.

This article is free to access.

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

APA

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 (Vol. 12079 LNCS, pp. 178–194). Springer Science and Business Media Deutschland GmbH. 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.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free