Volume 11 : Number 2 : Paper 4
December 2008 Special Issue of Best Papers presented at CLEI 2007, San Jose, Costa Rica
Title:
A Theory for Abstract Reduction Systems in PVS

Authors and Affiliations:
Andre Luiz Galdino, Departamento de Matematica, Universidade Federal de Goias, Brazil
Mauricio Ayala-Rincon, Instituto de Ciencias Exatas, Universidade de Brasilia Brasilia D.F., Brazil

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


Received April, 2007, Revised Dec, 2008 , Editor: Manuel Bermudez, Marcelo Jenkins
Full paper, 12 pages [ PDF, 233 Kb ]