Mauricio Ayala Rincón, Dr. rer. nat.
Full Professor
Institute of Mathematics and Statistics
Graduate Program in Mathematics (PPGMAT)
Federal University of Goiás
Affiliated Researcher, Graduate Programs in Informatics and Mathematics, Brasilia University

Address:
Institute of Mathematics and Statistics, Federal University of Goiás
Campus Samambaia
74001-970 Goiânia, Goiás, Brazil

e-mail: ayala[at]ufg.br
Publications
Courses
PVS Class 2017 (affiliated to ITP 2017) Mechanizing Mathematics (Tutorial UNCOL Manizales, 2023)
Formal Proofs in PVS (tutorial affiliated to CICM 2025)
Professional Activities CV Lattes
Grupo de Teoria da Computação
Focus of Research:
Properties and applications of term rewriting systems and its extensions - Related links
TRS PVS theory (PVS lib)
Nominal PVS theory (PVS lib)
Evol. algorithms for sorting permutations

Opportunities

  • Enter in contact if you are interested in Algoritmics, Computational and Mathematical Formalization, Theorem Proving, Automated Reasoning, Equational and Rewrite-based Deduction, Integration of AI agents and Proof Assistants, Ethics in AI, Evolutionary and Genetic Algorithms, and Genomic Data Processing.
  • RTA (1983 ... 2015) and TLCA (1993 ... 2015) evolved to Int. Conf. on Formal Structures for Computation and Deduction FSCD in 2016. Current edition: FSCD 2026. FSCD 2027, collocated with CADE, Nijmegen, The Netherlands, August 21-27, 2027.
  • Certified Programs and Proofs CPP 2027, Mexico City, Mexico, 10-16 January 2027. a:3/9, p:10/9.
  • 19th Conference on Intelligent Computer Mathematics CICM 2026, Ljubljana, 21-25 Sep 2026. Deadlines: TBD
  • 40th International Workshop on Unification UNIF 2026, Co-located with FSCD/FloC 2026, Lisbon. Deadlines: p 7 May.
  • 21th Logical and Semantic Frameworks, with Applications LSFA 2026, Affiliated with FSCD/FloC 2026, Lisbon, 18-19 July 2026. 22nd Logical and Semantic Frameworks with Applications LSFA 2027, Santo André, Brazil, 22-24 September, 2027.
  • International Conference on Interactive Theorem Proving ITP web page. ITP 2026, part of FloC, 26-29 July, Lisbon. Deadlines: a 12 Feb, p 19 Feb.
  • 15th International Workshop on Confluence IWC 2026, affiliated with FSCD/FloC, Lisbon, 24 July, 2026. Deadlines: a 1 Mar, p 9 Mar. Germany.
  • Recent Talks at GTC/UnB: Track on Logic and Computation (Progam), part of the XVIII SW in Mathematics (UnB) - (2-4 February, 2026)


    		• M. Ayala-Rincón & Flávio L.C. de Moura, Fundamentos da Programação Lógica e Funcional - O Princípio de Resolução e a Teoria de Reescrita -, Course Notes, Ed. UnB, December 2014. In Portuguese.


    M. Ayala-Rincón, Flávio L.C. de Moura, and Thaynara A. de Lima Applied Logic for Computer Scientists and Mathematicians: Computational Deduction and Formal Proofs, Springer, 2026.

    ayala[at]unb.br