Description
trs (acronymous for
Term
Rewriting
Systems)
is a complete library specified in the language of the proof
assistant PVS. The
PVS
theory trs contains a
collection of formalizations of theorems related with termination and
confluence properties of abstract reduction and term rewriting
systems. In addition, inside this
theory a
PVS
subtheory for illustrating the verification of
unification
algorithms
à la Robinson is available as well.
Download

The theory trs is available for:
To expand the file type, for example, "tar zxvf trspvs50.tgz" in a terminal. It will create the directory "trspvs50" that contains the file
README containing all details about the
theory trs.
Related work
 A. B. Avelar, A. L. Galdino, F. L. C. de Moura, and M. AyalaRincón. A Formalization of the Theorem of Existence of FirstOrder Most General Unifiers (doi). Electronic Proceedings in Theoretical Computer Science, Volume 81, Pages 6378, 2012.
This work presents a formalization of the theorem of existence of
most general unifiers in firstorder signatures in the higherorder
proof assistant PVS. The distinguishing feature of this
formalization is that it remains close to the textbook proofs that
are based on proving the correctness of the wellknown Robinson's
firstorder unification algorithm. The formalization was applied
inside a PVS development for term rewriting systems that provides a
complete formalization of the KnuthBendix Critical Pair theorem,
among other relevant theorems of the theory of rewriting. In
addition, the formalization methodology has been proved of practical
use in order to verify the correctness of unification algorithms in
the style of the original Robinson's unification algorithm.
 A. B. Avelar, F. L. C. de Moura, A. L. Galdino, and M. AyalaRincón. Verification of the Completeness of Unification Algoritms à la Robinson (doi). In Proc. WoLLIC 2010, SpringerVerlag LNCS Vol. 6188, pag. 110124, 2010.
This work presents a general methodology for verification of the
completeness of firstorder unification algorithms à la
Robinson developed in the higherorder proof assistant PVS. The
methodology is based on a previously developed formalization of the
theorem of existence of most general unifiers for unifiable terms over
firstorder signatures. Termination and soundness proofs of any
unification algorithm are proved by reusing the formalization of this
theorem and completeness should be proved according to the specific
way in that non unifiable inputs are treated by the algorithm.
 A.L. Galdino and
M. AyalaRincón
A Formalization of the KnuthBendix(Huet) Critical Pair
Theorem
(doi). Available
online (Online First), Journal of Automated Reasonning, 2010.
A mechanical proof of the KnuthBendix Critical Pair Theorem in the
higherorder language of the theorem prover PVS is described. This
wellknown theorem states that a Term Rewriting System is locally
confluent if and only if all its critical pairs are joinable. The
formalization of this theorem follows Huet's wellknown structure of
proof in which the restriction on strong normalization or Noetherian
was dropped and the result presented as a lemma.

A.L. Galdino
and
M. AyalaRincón . A PVS theory for Term
Rewriting Systems
(doi).
In Proc. Third Workshop on Logical and Semantic Frameworks with
Applications (LSFA 2008), Elsevier ENTCS Vol. 247, Pages 6783, 2009 .
The theory trs is described. This theory is built on the PVS
libraries for finite sequences and sets and a previously developed PVS
theory named ars for Abstract Reduction Systems which
was built on the PVS libraries for sets. Theories fordealing with the
structure of terms, for replacements and substitutions jointly
with ars allow for
adequate specifications of notions of term rewriting such as critical
pairs and formalization of elaborated criteria from the theory of Term
Rewriting Systems such as the KnuthBendix Critical Pair Theorem.
 A.L. Galdino and
M. AyalaRincón
A Formalization of Newman's and Yokouchi Lemmas in a
HigherOrder Language,
Journal of Formalized
Reasoning, 1(1):3950, 2008.
This paper shows how a formalization for the theory of Abstract
Reduction Systems (ars) in which noetherianity was specified by the
notion of wellfoundness over binary relations is used in order to
prove results such as the wellknown Newman's and Yokouchi's
Lemmas. The former is known as the diamond lemma and the latter states
a property of commutation between ARSs. In addition to proof
techniques available in the higherorder specification language of
PVS, the verification of these lemmas implies an elaborated use of
natural and noetherian induction.
 A.L. Galdino and
M. AyalaRincón
A Theory for Abstract Reduction Systems in PVS,
CLEI electronic
journal 11(2), Paper 4, 12 pages, Special Issue of Best Papers
presented at CLEI'07, San José, 2008.
Adequate specifications of basic definitions and notions of the theory
of Abstract Reduction Systems (ars) such as reduction, confluence and normal form are given and
wellknown results formalized. The formalizations include non trivial
results of the theory of Abstract Reduction Systems such as the correctness of the principle
of Noetherian Induction, Newman's Lemma and its generalizations, and
Commutation Lemmas, among others.
Contact
The main authors are
A.L. Galdino,
A.B. Avelar and
M. AyalaRincón.