Publications

Published works

M. Ayala-Rincón, T.A. de Lima, G. Ehling, T. Kutsia. Graded Quantitative Narrowing, In 18th International Conference on Intelligent Computer Mathematics (CICM 2025). Lecture Notes in Computer Science, Volume 16136, pp.113-132, Springer, Cham(2025).doi.
B. B. de Oliveira Ribeiro, M. M. Moscato, T.A. de Lima, M. Ayala-Rincón. A PVS Library on the Infinitude of Primes, In 18th International Conference on Intelligent Computer Mathematics (CICM 2025). Lecture Notes in Computer Science, Volume 16136, pp. 412 - 430, , Springer, Cham(2025).doi.
M. Ayala-Rincón, T. A. de Lima, M. J. Dias Lima, M. M. Moscato, and T. Kutsia. Verification of an Anti-Unification Algorithm in PVS, In The 17th NASA Formal Methods Symposium (NFM2025). Lecture Notes in Computer Science, Volume 15682, pp. 54 - 71, Springer, Cham (2025).doi.
(Honorable Mention Award)

T.A. de Lima, A.L. Galdino, B.B. O. Ribeiro, M. Ayala-Rincón. A Formalization of the General Theory of Quaternions, In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 11:1-11:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024).doi.
L. A. da Silveira, T. A. de Lima, M. Ayala-Rincón. On Reconfiguring Heterogeneous Parallel Island Models, Swarm and Evolutionary Computation.doi.
T.A. de Lima, A.B. Avelar, A.L. Galdino, M. Ayala-Rincón. Formalizing Factorization on Euclidean Domains and Abstract Euclidean Algorithms, In Proceedings LSFA 2023. EPTCS 402, 2024, pp. 18-33. doi.

L. A. da Silveira, T. A. de Lima, J. de Barros, J. L. Soncco-Álvarez, C. H. Llanos, and M. Ayala-Rincón. On The Behaviour of Parallel Island Models Genetic Algorithms, Applied Soft Computing Journal.doi. See pdf and source at genoma site.
F.F. Serrano Suárez, T.A. de Lima, M. Ayala-Rincón. Mechanising Hall’s Theorem for Countable Graphs .pdf, Easy Chair Preprint. LPAR 2023. No. 10365: 1-14.
M. Ayala-Rincón, T. A. de Lima, A. Borges Avelar, A. L. Galdino. Formalization of Algebraic Theorems in PVS. In Proceedings of 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning LPAR, EPiC Series in Computing, vol. 94:1-10 doi, 2023.

L. A. da Silveira, T. A. de Lima and M. Ayala-Rincón. Reconfigurable Heterogeneous Parallel Island Models. SSCI 2022: 1618 - 1625. doi
F.F. Serrano Suárez, T.A. de Lima, M. Ayala-Rincón. Hall’s Theorem for Enumerable Families of Finite Sets .pdf, Intelligent Computer Mathematics. CICM 2022. Lecture Notes in Computer Science(), vol 13467. Springer, Cham., doi

L. A. da Silveira, T. A. de Lima, J. L. Soncco-Álvarez, and M. Ayala-Rincón. Heterogeneous Parallel Island Models. IEEE Symposium Series on Computational Intelligence (SSCI), doi, 2021. See pdf and source at genoma site.
T. A. de Lima, A. L. Galdino, A. Borges 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, doi, 2021.

M. Ayala-Rincón and T. A. de Lima. Teaching Interactive Proofs to Mathematicians. In Proceedings 9th International Workshop on Theorem Prover Components for Educational Software (ThEdu), doi, 2020.
L. A. da Silveira, J. L. Soncco Álvarez, T. A. de Lima, and M. Ayala-Rincón. Behaviour of Bioinspired Algorithms in Parallel Island Models.2020 IEEE Congress on Evolutionary Computation CeC 2020, doi, 2020. Extended version at genoma site.

L.A. da Silveira, J.L. Soncco-Álvarez, T.A. de Lima and M. Ayala-Rincón.Parallel Island models Genetic Algorithms applied in NP-Hard problems. 2019 IEEE Congress on Evolutionary Computation CeC 2019, doi, 2019. Extendend version at genoma site.

A. B. Avelar da Silva, T. A. de Lima, A. L. Galdino. Formalizing Ring Theory in PVS. ITP 2018: 40-47, doi, 2018.
L.A. da Silveira, J.L. Soncco-Álvarez, T.A. de Lima and M. Ayala-Rincón. Parallel Multi-Island Genetic Algorithms for Sorting Unsigned Genomes by Reversals. In Proceedings Congress on Evolutionary Computation CEC 2018. doi, 2018.Extended version at genoma site.
T.A. de Lima and M. Ayala-Rincón.On the average number of reversals needed to sort signed permutations. Discrete Applied Mathematics 235:59-80.doi, 2018.

L.A. da Silveira, J.L. Soncco-Álvarez, T.A. de Lima and M. Ayala-Rincón.Memetic and Opposition-Based Learning Genetic Algorithms for Sorting Unsigned Genomes by Translocations.Proc. NaBIC 2015 (Vol.419, series Advances in Intelligent Systems and Computing pp 73-85, 2016). (doi), 2015.
L.A. da Silveira, J.L. Soncco-Álvarez, T.A. de Lima and M. Ayala-Rincón Computing Translocation Distance by a Genetic Algorithm. IEEE Xplore Proceedings CLEI 2015. (doi), 2015.

T.A. de Lima and M. Ayala-Rincón On the average reversal distance to sort signed permutations. Extended abstract presented at Permutation Patterns 2013, Paris, 2013.
T.A. de Lima and M. Ayala-Rincón. NP-Completeness of Sorting Unsigned Permutations by Reversals. Note MAT/UnB pdf”, Brasília, 2013.

T.A. de Lima and M. Ayala-Rincón.Complexity of Reversal Distance and other General Metrics on Permutation Groups. 7CCC 2012, doi, 2012.