A. L. Galdino. Formalizing Properties of Group Theory: From Isomorphism Theorems to Sylow's Theorems. PVS files.
2018
A. B. Avelar, T. A. de Lima, A. L. Galdino. Formalizing Ring Theory in PVS. In: Avigad J., Mahboubi A. (eds) Interactive Theorem Proving. ITP 2018. Lecture Notes in Computer Science, Volume 10895, Pages 40-47, 2018. doi.
2017
A. C. Rocha-Oliveira, A. L. Galdino and M. Ayala-Rincón. Confluence of Orthogonal Term Rewriting Systems in the Prototype Verification System. Journal of Automated Reasoning, Volume 58, Pages 231-251, 2017. doi.
2014
A. B. Avelar, A. L. Galdino, F. L. C. de Moura, and M. Ayala-Rincón. First-Order Unification in the Proof Assistant PVS. In press Logic Journal of the IGPL, 2014. doi.
2013
A. C. R. Oliveira, A. L. Galdino, and M. Ayala-Rincón. Synchronizing Applications of the Parallel Moves Lemma to Formalize Confluence of Orthogonal TRSs in PVS. In Proc. 2nd International Workshop on Confluence - IWC 2013. Eindhoven: RDP, Pages 47-51, 2013. PDF file.
2012
A. B. Avelar, A. L. Galdino, F. L. C. de Moura, and M. Ayala-Rincón. A Formalization of the Theorem of Existence of First-Order Most General Unifiers. Electronic Proceedings in Theoretical Computer Science, Volume 81, Pages 63-78, 2012. doi.
2010
A. L. Galdino and M. Ayala-Rincón. A Formalization of the Knuth-Bendix(-Huet) Critical Pair Theorem. Journal of Automated Reasoning, Volume 45, Number 3, Pages 301-325, 2010. doi, PVS files.
A. B. Avelar, F. L. C. de Moura, A. L. Galdino, and M. Ayala-Rincón. Verification of the Completeness of Unification Algoritms à la Robinson. In Proc. WoLLIC 2010, Springer-Verlag LNCS Vol. 6188, Pages 110-124, 2010. doi, PDF file.
2009
A. L. Galdino and M. Ayala-Rincón. A PVS theory for Term Rewriting Systems. In Proc. Third Workshop on Logical and Semantic Frameworks with Applications (LSFA 2008), Elsevier ENTCS Vol. 247, Pages 67-83, 2009. doi, PDF file, PVS files.
2008
A. L. Galdino and M. Ayala-Rincón. A Formalization of Newman's and Yokouchi Lemmas in a Higher-Order Language. Journal of Formalized Reasoning, 1(1):39-50, 2008. PDF file.
A. L. Galdino and M. Ayala-Rincón. A Theory for Abstract Reduction Systems in PVS. CLEI electronic journal, 11(2), Paper 4, 12 pages, Special Issue of Best Papers presented at CLEI'07, San José, 2008. PDF file.
A. L. Galdino and M. Ayala-Rincón. Verification of Newman's and Yokouchi Lemmas in PVS. Presentation at Computability in Europe (CiE 2008), 2008. PDF file, PVS files.
A. L. Galdino and M. Ayala-Rincón. A PVS Theory for Abstract Rewriting Systems. In Proc. XXXIII Conferencia Latinoamericana de Informática - CLEI'07, 2007. PDF file, PVS files.
A. L. Galdino, C. A. Muñoz and M. Ayala- Rincón. Formal Verification of an Optimal Air Traffic Conflict Detection and Recovery Algorithm. In Proc. WoLLIC 2007, Springer-Verlag LNCS Vol. 4576, pages 177-188, 2007. doi, PDF file, PVS files.
2000
Dissertação de Mestrado, 2000. PDF file, in Portuguese.
1999
O. C. de Oliveira Filho and A. L. Galdino. Análise de Equações Diferencias Funcionais via Equações Diferença. In: 50 Seminário Brasileiro de Análise - SBA, 1999, São Paulo - SP. v. I, p. 523-537.
1997
M. H. Stoppa and A. L. Galdino. A representação única das Funções Schanuel. In: 46 Seminário Brasileiro de Análise - SBA, 1997, Niterói - RJ. v. único, p. 407-417.
