%0 Journal Article
%T A Formalization of Newman's and Yokouchi's Lemmas in a Higher-Order Language
%A Andre Luiz Galdino
%A Mauricio Ayala-Rinc¨Žn
%J Journal of Formalized Reasoning
%D 2008
%I University of Bologna
%X This 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.
%U http://jfr.cib.unibo.it/article/view/1347/744