A Formalization of Newman's and Yokouchi's Lemmas in a Higher-Order Language
AbstractThis paper shows how a formalization for the theory of Abstract Reduction Systems (ARSs) in which noetherianity was specified by the notion of well-foundness over binary relations is used in order to prove results such as the well-known Newman's and Yokouchi's Lemmas. The former is known as the diamond lemma and the latter states a property of commutation between ARSs. The theory ars was specified in the Prototype Verification System (PVS) for which to the best of our knowledge there was no available theory for dealing with rewriting techniques in general before this development. In addition to proof techniques available in the higher-order specification language of PVS, the verification of these lemmas implies an elaborated use of natural and noetherian induction.
How to Cite
Galdino, A. L., & Ayala-Rincón, M. (2008). A Formalization of Newman’s and Yokouchi’s Lemmas in a Higher-Order Language. Journal of Formalized Reasoning, 1(1), 39–50. https://doi.org/10.6092/issn.1972-5787/1347
Copyright (c) 2008 Andre Luiz Galdino, Mauricio Ayala-Rincón
Copyrights and publishing rights of all the texts on this journal belong to the respective authors without restrictions.