cl-banner

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

Alexander Lochmann, Aart Middeldorp

26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, LCNS 12079, pp. 25 – 40, 2020.

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.

 

  PDF |    doi:10.1007/978-3-030-45237-7_11  |  © The Author(s) 2020

BibTeX 

@inproceedings{LM-TACAS20,
author = "Alexander Lochmann and Aart Middeldorp",
title = "Formalized Proofs of the Infinity and Normal Form Predicates in the First-Order Theory of Rewriting",
booktitle = "Proceedings of the 26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems",
editor = "Armin Biere and Dave Parker",
series = "Lecture Notes in Computer Science",
volume = 12079,
pages = "178--194",
year = 2020,
doi = "10.1007/978-3-030-45237-7_11"
}
Nach oben scrollen