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.

Download

• The theory trs is available for:
  • PVS 6.0: TRS files available within NASA Langley PVS Libraries.
  • PVS 5.0: trs-pvs50.tgz.
  • PVS 4.2: trs-pvs42.tgz.

To expand the file type, for example, "tar zxvf trs-pvs50.tgz" in a terminal. It will create the directory "trs-pvs50" 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. 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 and M. Ayala-Rincón.