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.


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


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