Computability in Europe 2008
Logic and Theory of Algorithms

Print current page  Print this page

Regular Talk:
Verification of Newman's and Yokouchi's Lemmas in PVS

Edit abstract data

Author(s): André Luiz Galdino and Mauricio Ayala-Rincon
Slot: Mon, 12:00-12:20, Propylaia (col. 2)

Abstract

This paper shows how a theory for Abstract Reduction Systems (ARSs)
in which noetherianity was defined by the notion of well-foundness
over binary relations is used in order to prove results such as the
well-known Newman's Lemma and the Yokouchi's Lemma. The former one
known
as the diamond lemma and the later which states a property
of commutation between ARSs. The ars theory was specified in the
Prototype Verification System (PVS) for which to the best of our
knowledge there are no available theory for dealing with rewriting
techniques in general.
In addition to proof techniques available in PVS the verification
of these lemmas implies an elaborated use of natural as well as
noetherian induction.

websites: Arnold Beckmann 2008-05-19 Valid HTML 4.01! Valid CSS!