You are here

Formalisation in PVS of Rewriting Properties


Lecturer: Mauricio Ayala-Rincón, Universidade de Brasília, Brazil

The capabilities of the proof assistant PVS to specify and proof, in a natural manner, that is very close to the one found in papers and textbooks, notions and properties of rewriting theory will be taught. The short course will be based on formalizations that range from simple properties of abstract reduction systems  such as Newman’s lemma, until those much more sophisticated of term rewriting systems such as the Knuth-Bendix-Huet Critical Pairs criterion and the confluence of orthogonal systems, all them available as part of the PVS theory "trs".


This course is directed to students with basic knowledge in rewriting and some familiarity with computational logic and formal deduction.

Tutorial for PVS rewriting can be download from here.