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 sub-theory for illustrating the verification of unification algorithms à la Robinson is available as well as sub-theories with a formalization of Rosen's confluence for orthogonal TRS's and verification of the dependency_pairs criterion for innermost reduction.

Download

• The theory trs is available for:
  • PVS TRS theory is available within NASA Langley PVS Libraries.
  • Also available here: TRS PVS 6.0 and 7.0 (snapshot 1218)
    The TRS theoryincludes sub-theories orthogonality, and dependency_pairs.
  • PVS 5.0: trs-pvs50.tgz.
  • PVS 4.2: trs-pvs42.tgz.

Previous versions of the TRS theory are available for: PVS 4.2. 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.

Related work

• A.A. Almeida, and M. Ayala-Rincón Formalizing the Dependency Pairs Criterion for Innermost Termination. Revised paper presented at SBMF 2019 Science of Computer Programming 195:102474, 2020.
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. 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 PVS. 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 M. Ayala-Rincón A Formalization of the Knuth-Bendix(-Huet) Critical Pair Theorem (doi). Available 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.


• A.L. Galdino and M. Ayala-Rincó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 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 M. Ayala-Rincón A Formalization of Newman's and Yokouchi Lemmas in a Higher-Order Language, 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 M. Ayala-Rincó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 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.

Contact

The main authors are A.L. Galdino, A.B. Avelar, A.C. Rocha-Oliveira, A.A. Almeida, M. Ayala-Rincón.