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 as
subtheories with a formalization of Rosen's confluence for
orthogonal TRS's and verification of the
dependency_paris criterion for
innermost reduction.
Download

The theory trs is available for:
Previous versions of the TRS theory are available for:
PVS 4.2.

The theory Nominal Unification is available for:
To expand the file type, for example, "tar zxvf trspvs60.tgz" in a terminal. It will create the directory "trspvs60" that contains the file
README containing all details about the
theory trs.
Related work
 A.A. Almeida, and M. AyalaRincón
Formalizing the Dependency Pairs Criterion for Innermost
Termination.
pdf in ArXiv, accepted
for presentation at SBMF 2019.
This work describes the formalization of theorems of necessity and
sufficiency of the Dependency Pairs Criterion: A TRS is innermost
noetherian if and only if there are no infinite chains of innermost
Dependency Pairs.
 A. C. RochaOliveira, A. L. Galdino and
M. AyalaRincón. Confluence of Orthogonal Term
Rewriting Systems in the Prototype Verification System.
Journal of Automated Reasoning,
Pages 121, First online: 07 June 2016.
This work describes a complete formalization in PVS of the theorem of
confluence of orthogonal term rewriting systems. The formalization
includes definitions and results on parallel reduction, in particular
Rosen's Parallel Moves Lemma. It is made available as a PVS theory
orthogonality inside the directory TRS of the NASA Langley PVS
Library. Like all of TRS, orthogonality is intended to stay close to
textbook proofs. The present proof uses the Parallel Moves Lemma at
dominating positions of a parallel context. In this manner, all
parallel forks filling the holes of the context are joined and, as
result, a term of joinability for the whole fork is constructed.
 A. B. Avelar, A. L. Galdino, F. L. C. de
Moura, and M. AyalaRincón. Firstorder unification
in the PVS proof assistant.
Logic Journal of the IGPL,
Volume 22(5), Pages 758789, 2014.
This work presents formalizations of properties and algorithms for the
firstorder unification theory in the proof assistant PVS. In previous
works a formalization of the theorem of existence of most general
unifiers (mgu's) for firstorder unifiable problems was presented and
then, it was illustrated how the formalizations of correctness and
completeness used for the proof of the theorem of existence, can be
adapted in order to verify greedy unification algorithms à la
Robinson. That work consists of two elaborated PVS theories
having been the one related with the theorem of existence of mgu's
applied for obtaining a full formalization of the KnuthBendix(Huet)
critical pair theorem. In addition to these two developments, this
work describes a formalization of the correction and completeness of a
more elaborated firstorder unification algorithm. In contrast with
the greedy algorithm, the current one is more efficient.
 A. C. RochaOliveira, A. L. Galdino and
M. AyalaRincón. Synchronizing Applications of the
Parallel Moves Lemma to Formalize Confluence of Orthogonal TRSs in
PVS.
In Proc. International Workshop on Confluence 2013,
Pages 4752, Eindhoven, Netherlands, 2013.
A complete formalization in PVS of the theorem of confluence of
orthogonal term rewriting systems is presented. The formalized proof
uses the PVS theory trs maintaining its distinguishing feature of
remaining close to textbook's proofs. The proof is based on a
formalization of the Parallel Moves Lemma. Auxiliary lemmas are given
which use an inductive construction of the crucial positions of a term
originating a parallel divergence. Classifying all these positions,
by application of the parallel moves lemma to the crucial divergence
subterms, the desired common term of joinability is built.
 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,
A.C. RochaOliveira,
A.A. Almeida,
M. AyalaRincón.