A Theory for Abstract Reduction Systems in PVS

Authors

  • Andre Luiz Galdino Departamento de Matematica, Universidade Federal de Goias
  • Mauricio Ayala Rincon Instituto de Ciencias Exatas, Universidade de Brasılia

DOI:

https://doi.org/10.19153/cleiej.11.2.4

Abstract

A theory for Abstract Reduction Systems (ARS) in the proof assistant PVS (Prototype Verification System) called ars is described. Adequate specifications of basic definitions and notions of the theory of ARSs such as reduction, confluence and normal form are given and well-known results formalized. The formalizations include non trivial results of the theory of ARSs such as the correctness of the principle of Noetherian Induction, Newman’s Lemma and its generalizations, and Commutation Lemmas, among others. Although term rewriting proving technologies have been provided in several specification languages and proof assistants, to our knowledge, before the development presented in this paper there was no complete formalization of an abstract reduction theory in PVS. This makes relevant the presented ars specification as the basis of a PVStheory called trs for the general treatment of Term Rewriting Systems.

Downloads

Published

2008-12-01

Issue

Vol. 11 No. 2 (2008): Special Issue of Best Papers presented at CLEI 2007, San Jose, Costa Rica

Section

Articles

License

CLEIej is supported by its home institution, CLEI, and by the contribution of the Latin American and international researchers community, and it does not apply any author charges whatsoever for submitting and publishing. Since its creation in 1998, all contents are made publicly accesibly. The current license being applied is a (CC)-BY license (effective October 2015; between 2011 and 2015 a (CC)-BY-NC license was used).