is a complete library specified in the language of the proof
assistant PVS. The
PVS theory trs
collection of formalizations of theorems related with termination and
confluence properties of abstract reduction and term rewriting
systems. In addition, inside this theory
for illustrating the verification of
algorithms à la
Robinson is available as well as a
with a formalization of confluence for orthogonal
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 trs-pvs60.tgz" in a terminal. It will create the directory "trs-pvs60" that contains the file README
containing all details about the theory trs
- A. C. Rocha-Oliveira, A. L. Galdino and
M. Ayala-Rincón. Confluence of Orthogonal Term
Rewriting Systems in the Prototype Verification System.
Journal of Automated Reasoning,
Pages 1-21, 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. Ayala-Rincón. First-order unification
in the PVS proof assistant.
Logic Journal of the IGPL,
Volume 22(5), Pages 758-789, 2014.
This work presents formalizations of properties and algorithms for the
first-order unification theory in the proof assistant PVS. In previous
works a formalization of the theorem of existence of most general
unifiers (mgu's) for first-order 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 Knuth-Bendix(-Huet)
critical pair theorem. In addition to these two developments, this
work describes a formalization of the correction and completeness of a
more elaborated first-order unification algorithm. In contrast with
the greedy algorithm, the current one is more efficient.
- A. C. Rocha-Oliveira, A. L. Galdino and
M. Ayala-Rincón. Synchronizing Applications of the
Parallel Moves Lemma to Formalize Confluence of Orthogonal TRSs in
In Proc. International Workshop on Confluence 2013,
Pages 47-52, 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. Ayala-Rincón. A Formalization of the Theorem of Existence of First-Order Most General Unifiers (doi). Electronic Proceedings in Theoretical Computer Science, Volume 81, Pages 63-78, 2012.
This work presents a formalization of the theorem of existence of
most general unifiers in first-order signatures in the higher-order
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 well-known Robinson's
first-order unification algorithm. The formalization was applied
inside a PVS development for term rewriting systems that provides a
complete formalization of the Knuth-Bendix 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. Ayala-Rincón. Verification of the Completeness of Unification Algoritms à la Robinson (doi). In Proc. WoLLIC 2010, Springer-Verlag LNCS Vol. 6188, pag. 110-124, 2010.
This work presents a general methodology for verification of the
completeness of first-order unification algorithms à la
Robinson developed in the higher-order 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
first-order 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
A Formalization of the Knuth-Bendix(-Huet) Critical Pair
on-line (Online First), Journal of Automated Reasonning, 2010.
A mechanical proof of the Knuth-Bendix Critical Pair Theorem in the
higher-order language of the theorem prover PVS is described. This
well-known 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 well-known structure of
proof in which the restriction on strong normalization or Noetherian
was dropped and the result presented as a lemma.
M. Ayala-Rincón . A PVS theory for Term
In Proc. Third Workshop on Logical and Semantic Frameworks with
Applications (LSFA 2008), Elsevier ENTCS Vol. 247, Pages 67-83, 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 Knuth-Bendix Critical Pair Theorem.
- A.L. Galdino and
A Formalization of Newman's and Yokouchi Lemmas in a
Journal of Formalized
Reasoning, 1(1):39-50, 2008.
This paper shows how a formalization for the theory of Abstract
Reduction Systems (ars) in which noetherianity was specified by the
notion of well-foundness over binary relations is used in order to
prove results such as the well-known 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 higher-order specification language of
PVS, the verification of these lemmas implies an elaborated use of
natural and noetherian induction.
- A.L. Galdino and
A Theory for Abstract Reduction Systems in PVS,
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
well-known 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.
The main authors are