HTTP/2 200 server: GitHub.com content-type: text/html; charset=utf-8 last-modified: Mon, 08 Dec 2025 20:43:02 GMT access-control-allow-origin: * etag: W/"69373856-168b" expires: Mon, 29 Dec 2025 15:01:09 GMT cache-control: max-age=600 content-encoding: gzip x-proxy-cache: MISS x-github-request-id: 7D99:2916CC:90571E:A1D8E2:6952955D accept-ranges: bytes age: 0 date: Mon, 29 Dec 2025 14:51:09 GMT via: 1.1 varnish x-served-by: cache-bom-vanm7210025-BOM x-cache: MISS x-cache-hits: 0 x-timer: S1767019869.242409,VS0,VE216 vary: Accept-Encoding x-fastly-request-id: f83248ff2ce2309bef439488ceaa62ffb965f5ab content-length: 2502 

Mauricio Ayala Rincón, Dr. rer. nat. Full Professor Theory of Computation Departments of Computer Science and Mathematics Brasilia University Address: Departamento de Matemática, Universidade de Brasília Campus Universitário Darcy Ribeiro, Asa Norte 70910-900 Brasília D. F., Brasil Tels. +55-61- 3307 2441|2442| +55-61- 3107 6453 | 3676 Fax +55-61-3273 2737 e-mail: ayala[at]unb.br Publications Courses 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

---

Opportunities

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. Current edition: FSCD 2025, Birmingham, UK. 18th Conference on Intelligent Computer Mathematics CICM 2025, Brasília, 6-11 Oct 2025 (CICM + LSFA). Deadlines: a:05, p:12 May 2025. 20th Logical and Semantic Frameworks, with Applications LSFA 2025, Brasília, 6-11 Oct 2025 (CICM + LSFA) The 17th NASA Formal Methods Symposium NFM 2025, Williamsburg VA, USA. International Conference on Interactive Theorem Proving ITP web page. ITP 2025, Reykjavik, Iceland. 14th International Workshop on Confluence IWC 2025, Lepzig, Germany. 39th International Workshop on Unification UNIF 2025, Co-located with FSCD 2025, Birmingham, UK. Recent Talks at GTC/UnB: Track on Logic and Computation ( Final Progam), part of the XVL SW in Mathematics (UnB) - (7-9 February, 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.

---

ayala[at]unb.br