Formalising Confluence in PVS

Por Mauricio Ayala-Rincón
Publicado em 2016-03-01

Explicit substitions and all that

Por Mauricio Ayala Rincón, César Muñoz
Publicado em 2000-12-01

A Formalization of Newman's and Yokouchi's Lemmas in a Higher-Order Language

Por Andre Luiz Galdino, Mauricio Ayala-Rincón
Publicado em 2008-12-01

Unification modulo presburger arithmetic and other decidable theories

Por Mauricio Ayala Rincón, Ivan E. Tavares Araújo
Publicado em 2001-12-01

A Formalization of the Theorem of Existence of First-Order Most General Unifiers

Por Andréia B Avelar, André L Galdino, Flávio LC de Moura, Mauricio Ayala-Rincón
Publicado em 2012-03-01