scholarly journals A Theory for Abstract Reduction Systems in PVS

2008 ◽  
Vol 11 (2) ◽  
Author(s):  
Andre Luiz Galdino ◽  
Mauricio Ayala Rincon
Keyword(s):  
Normal Form ◽  
Term Rewriting ◽  
General Treatment ◽  
Reduction Theory ◽  
Proof Assistant ◽  
Proof Assistants ◽  
Specification Languages ◽  
Term Rewriting Systems ◽  
Rewriting Systems ◽  
Prototype Verification

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.

Confluence of Orthogonal Term Rewriting Systems in the Prototype Verification System

2016 ◽  
Vol 58 (2) ◽  
pp. 231-251 ◽  
Author(s):  
Ana Cristina Rocha-Oliveira ◽  
André Luiz Galdino ◽  
Mauricio Ayala-Rincón
Keyword(s):  
Term Rewriting ◽  
Term Rewriting Systems ◽  
Rewriting Systems ◽  
Verification System ◽  
Prototype Verification

PATTERN MATCHING CODE MINIMIZATION IN REWRITING-BASED PROGRAMMING LANGUAGES

2002 ◽  
Vol 13 (06) ◽  
pp. 873-887
Author(s):  
NADIA NEDJAH ◽  
LUIZA DE MACEDO MOURELLE
Keyword(s):  
Programming Languages ◽  
Pattern Matching ◽  
Term Rewriting ◽  
Directed Acyclic Graphs ◽  
Tree Automaton ◽  
Minimal Tree ◽  
Term Rewriting Systems ◽  
Rewriting Systems ◽  
Acyclic Graphs ◽  
Space Requirements

We compile pattern matching for overlapping patterns in term rewriting systems into a minimal, tree matching automata. The use of directed acyclic graphs that shares all the isomorphic subautomata allows us to reduce space requirements. These are duplicated in the tree automaton. We design an efficient method to identify such subautomata and avoid duplicating their construction while generating the dag automaton. We compute some bounds on the size of the automata, thereby improving on previously known equivalent bounds for the tree automaton.

scholarly journals CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates

2011 ◽  
Vol 21 (4) ◽  
pp. 827-859 ◽  
Author(s):  
FRÉDÉRIC BLANQUI ◽  
ADAM KOPROWSKI
Keyword(s):  
Term Rewriting ◽  
Automated Verification ◽  
Proof Assistant ◽  
Proof Assistants ◽  
Active Subject ◽  
Turing Complete

Termination is an important property of programs, and is notably required for programs formulated in proof assistants. It is a very active subject of research in the Turing-complete formalism of term rewriting. Over the years, many methods and tools have been developed to address the problem of deciding termination for specific problems (since it is undecidable in general). Ensuring the reliability of those tools is therefore an important issue.In this paper we present a library formalising important results of the theory of well-founded (rewrite) relations in the proof assistant Coq. We also present its application to the automated verification of termination certificates, as produced by termination tools.The sources are freely available athttp://color.inria.fr/.

Sign in / Sign up

Export Citation Format

Share Document