Academic Journals Database
Disseminating quality controlled scientific knowledge

A Formalization of Newman's and Yokouchi's Lemmas in a Higher-Order Language

ADD TO MY LIST
 
Author(s): Andre Luiz Galdino | Mauricio Ayala-Rincón

Journal: Journal of Formalized Reasoning
ISSN 1972-5787

Volume: 1;
Issue: 1;
Start page: 39;
Date: 2008;
Original page

ABSTRACT
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.

Tango Rapperswil
Tango Rapperswil

    
RPA Switzerland

RPA Switzerland

Robotic process automation