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 a sub-theory with a formalization of confluence for orthogonal TRS's.

Download

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

Contact

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