| First-order unification in the PVS proof assistant AB Avelar, AL Galdino, FLC de Moura, M Ayala-Rincón Logic Journal of the IGPL 22 (5), 758-789, 2014 | 13 | 2014 |
| Formalization of ring theory in PVS: isomorphism theorems, principal, prime and maximal ideals, Chinese remainder theorem TA de Lima, AL Galdino, AB Avelar, M Ayala-Rincón Journal of Automated Reasoning 65 (8), 1231-1263, 2021 | 9 | 2021 |
| Formalização da automação da terminação através de grafos com matrizes de medida AB Avelar | 9 | 2015 |
| Verification of the Completeness of Unification Algorithms à la Robinson AB Avelar, FLC de Moura, AL Galdino, M Ayala-Rincón Logic, Language, Information and Computation: 17th International Workshop …, 2010 | 7 | 2010 |
| Formalizing ring theory in PVS AB Avelar da Silva, TA de Lima, AL Galdino Interactive Theorem Proving: 9th International Conference, ITP 2018, Held as …, 2018 | 5 | 2018 |
| A formalization of the theorem of existence of first-order most general unifiers AB Avelar, AL Galdino, FLC de Moura, M Ayala-Rincón arXiv preprint arXiv:1203.6160, 2012 | 3 | 2012 |
| Formal Verification of Termination Criteria for First-Order Recursive Functions CA Muñoz, M Ayala-Rincón, MM Moscato, AM Dutle, AJ Narkawicz, ... Journal of Automated Reasoning 67 (4), 40, 2023 | 2 | 2023 |
| Formalizing Factorization on Euclidean Domains and Abstract Euclidean Algorithms TA de Lima, AB Avelar, AL Galdino, M Ayala-Rincón arXiv preprint arXiv:2404.14920, 2024 | 1 | 2024 |
| Formalization of Algebraic Theorems in PVS (Invited Talk) M Ayala-Rincón, TA de Lima, AB Avelar, AL Galdino Proceedings of 24th International Conference on Logic 94, 1-10, 2023 | 1 | 2023 |
| 12th International Conference on Interactive Theorem Proving (ITP 2021) MO Myreen, N Polikarpova, A Popescu, T Bauereiss, P Lammich, ... Schloss Dagstuhl-Leibniz-Zentrum für Informatik GmbH, 2021 | | 2021 |
| Automation of Termination: Abstracting Calling Contexts through Matrix-Weighted Graphs AB Avelar, M Ayala-Rincón, CA Munoz | | 2013 |
| Formalização da prova do teorema de existência de unificadores mais gerais em teorias de primeira-ordem AB Avelar | | 2011 |
| LSFA 2010-2011 Guest Editors: Elaine Pimentel and Simona Ronchi della Rocca B Lopes, M Benevides, EH Haeusler, PAS Veloso, SRM Veloso, ... | | |
| LOGIC JOURNAL of the IGPL B Lopes, M Benevides, EH Haeusler, PAS Veloso, SRM Veloso, ... | | |
