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.


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


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