Mauricio Ayala Rincón, Dr. rer. nat.
Full Professor
Theory of Computation
Departments of Computer Science and Mathematics
Brasilia University

Departamento de Matemática, Universidade de Brasília
Campus Universitário Darcy Ribeiro, Asa Norte
70910-900 Brasilia D. F., Brasil
Tels. +55-61- 3307 2441|2442| +55-61- 3107 6453 | 3676 Fax +55-61-3273 2737
e-mail: ayala[at]
PVS Class 2017 (affiliated to ITP 2017) Mechanizing Mathematics (Tutorial UNCOL Manizales, 2023)
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
Nominal PVS theory
Evol. algorithms for sorting permutations


  • Ph.D. scholarships Please, enter in contact ASAP, if you are interested in Algoritmics, Computational and Mathematical Formalization, Theorem Proving, Automated Reasoning, Equational and Rewrite-based Deduction, 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.
    FSCD 2024, Tallinn, Estonia. Deadlines: a:5 Feb, p:12 Feb 2024.
  • 27th International Conference on Foundations of Software Science and Computation Structures FoSSaCS 2024. Luxembourg. Deadline: 12 Oct 2023.
  • Logical and Semantic Frameworks, with Applications LSFA 2024, TBD.
  • International Conference on Interactive Theorem Proving ITP web page. ITP 2024, Tbilisi, Georgia.
  • 17th and 18th Conference on Intelligent Computer Mathematics CICM 2024, 2025, Montreal, Brasília.
  • 12th International Workshop on Confluence IWC 2024, Proposed to be Colocated with FSCD 2024, Tallinn, Estonia.
  • 37th International Workshop on Unification UNIF 2023, affiliated to FSCD 2023, Rome, Italy.
  • Current Conferences at GTC/UnB: Final Progam of the Track on Logic and Computation, part of the XVL SW in Mathematics (UnB) - 7-9 February, 2024
  • Next talks by Temur Kutsia (RISC/JKU Linz) (22 and 25 March, 2024) and Mariano Moscato (AMA/NASA LaRC Formal Methods) (21 April - 5 May) in the context of CAPES PrInt, and Maribel Fernández (King's College London) (13-21 May, 2024).

  • 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, Applied Logic for Computer Scientists: Computational Deduction and Formal Proofs, Springer, 2017.