Publicações
Publicações
Work in progress
A. L. Galdino. Formalizing Properties of Group Theory: From Isomorphism Theorems to Sylow's Theorems. PVS files.
2024
T. A. de Lima, A. L. Galdino, B. B. O. Resende and M. Ayala-Rincón. A Formalization of the General Theory of Quaternions. In: International Conference on Interactive Theorem Proving, 2024, Tblisi. LiPIcs Proc. 15th International Conference on Interactive Theorem Proving (ITP). Dagstuhl: LiPIcs, 2024. p. 1-18. doi.
2023
M. Ayala-Rincón, T. A. de Lima, A. B. Avelar and A. L. Galdino. Formalization of Algebraic Theorems in PVS (Invited Talk). In: Proceedings of 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning. EPiC Series in Computing, Pages 1-10, 2023. doi.
T. A. de Lima, A. L. Galdino, A. B. Avelar and M. Ayala-Rincón. Formalizing Factorization on Euclidean Domains and Abstract Euclidean Algorithms. In: 18th International Workshop on Logical and Semantic Frameworks, with Applications (LSFA 2023), Pages 6-21, 2023.
2021
T. A. de Lima, A. L. Galdino, A. B. Avelar and M. Ayala-Rincón. Formalization of Ring Theory in PVS: Isomorphism Theorems, Principal, Prime and Maximal Ideals, Chinese Remainder Theorem. Journal of Automated Reasoning, 2021. doi.
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
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.
Tese de Doutorado, 2008. PDF file, in Portuguese.
2007
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.