Academics

Mauricio Ayala Rincón
Group of Theory of Computation
Department of Mathematics
University of Brasília


Computational Logic 1 (117366 Lógica Computacional 1)
Offered by the Undergraduate Program of the Departamento de Computação, First Semester 2023 - 28th March - 25 Jul 2023 - (Prof. Mauricio Ayala Rincón)

This is a one-semester course for undergraduate computer science students on propositional and predicate logic and their computer science applications, mainly for verification. Logical concepts such as correctness and completeness of natural deduction and undecidability are reviewed carefully. The course's focus is on applying deduction methods and their applications in specification, formalization, and algorithm verification.

Didactic material of the course, semester 2023-1 Classes start on Wesnesday, 29th March 2023, 16:00

  • Zoom Link link to the lectures
    Meeting ID: 814 1398 4380
    Passcode: LogiComp
  • Material of the Course in the platform Aprender 3

    CIC0182 Lógica Computacional 1, Turma 1 (LogComp2023-1)


    Formal and Computational Logic (316601 Lógica Formal Computacional/313998 Lógica Clássica e Extensões)

    Offered by the Graduate Programs of the Departments of Computação and Matemática, First Semester 2023 (Prof. Mauricio Ayala Rincón)
    this is a one semester course for mathematics and computer science graduate students on formal and computational logic. The focus is on the expressiveness and limitations of first-order logic. After briefly reviewing the syntax and semantics and deduction mechanisms of predicate logic, Gödel completeness and incompleteness theorems are carefully studied. Compactness and Löwehneim-Skolem properties are studied and also Lindström theorems on the maximality of first-order logic, as a language for the specification of mathematics and computation. The course brings a solid background for Math and CS students who want to develop research in formal methods, proof and type theory.

    Bibliography:

  • Zoom Link link to the lectures
    Meeting ID: 867 0604 7857 Passcode: LogiForm
  • Material of the Course in the platform Aprender 3

    PPGI0109 - Lógica Formal e Computacional - Turma 01 - 2023/1 (PPG)


    328405 Type Theory (Teoria dos Tipos)

    Offered by the Graduate Programs in Informatics and Mathematics, First Semester 2022 (Prof. Mauricio Ayala Rincón)

    this is a one-semester course for mathematics and computer science graduate students on foundations of type theory and its applications to semantics and logic of computation. Untyped lambda calculus and its typed versions making emphasis on the simple typed case à la Church and à la Curry are covered. Type checking, type inference and the problem of inhabitation are considered.


    Theory of Computing (316296 Teoria da Computação/ 318132 Tópicos em Computação)
    Offered by the Graduate Programs in Informatics and Mathematics, Second Semester 2020 - 1st Feb. - 19 May 2021 - (Prof. Mauricio Ayala Rincón)


    This is a one-semester course for mathematic and computer science graduate students on the mathematical foundations of computation. The semantics of computation is focused from the point of view of the logic and functional programming paradigms. In the first part of the course, the resolution principle, first-order unification, fixed-point theory, and then SLD-resolution and its completeness and soundness are formally studied. In the second part of the course, rewriting theory is examined as the more appropriate formalism for reasoning about the functional programming paradigm. The Turing completeness of both paradigms is checked to show that they are expressive enough to allow the specification of all recursive computable functions.


    Proof Theory (303666 Teoria de Prova)

    Offered by the Graduate Programs in Informatics and Mathematics, First Semester 2021 - 19 Jul - 03 Nov 2021 - (Prof. Mauricio Ayala Rincón)
    this is a one semester graduate course for computer science and mathematics students on proof theory. The course brings a solid background for students who pretend to understand mathematical proofs as rigourous mathematical objects as well as to do research in automated deduction and formal methods. After studying and relating different deductive formal frameworks such as Gentzen, Natural and Hilbert systems, theorems on cut elimination and normal proofs will be studied too.

    Bibliography:

    Didactic material of the course, semester 2021/I
  • Zoom link to the lectures
    Meeting ID: 810 3669 0624
    Passcode: TeoProv
  • Link to the Course in Aprender 3 - Search and register the course Teoria de Prova, Turma A (TeoProva2021-1)


    Formal and Computational Logic (316601 Lógica Formal Computacional/313998 Lógica Clássica e Extensões)

    Offered by the Graduate Programs of the Departments of Computação and Matemática, First Semester 2017 (Prof. Mauricio Ayala Rincón)
    this is a one semester course for mathematics and computer science graduate students on formal and computational logic. The focus is on the expressiveness and limitations of first-order logic. After briefly reviewing the syntax and semantics and deduction mechanisms of predicate logic, Gödel completeness and incompleteness theorems are carefully studied. Compactness and Löwehneim-Skolem properties are studied and also Lindström theorems on the maximality of first-order logic, as a language for the specification of mathematics and computation. The course brings a solid background for Math and CS students who want to develop research in formal methods, proof and type theory.

    Bibliography:

    Program
    Menções 2017/I


    Topics in computation: proof theory (Tópicos em Computação: teoria de prova)

    Offered by the Graduate Program in Informatics, First Semester 2013 (Prof. Mauricio Ayala Rincón)
    this is a semester graduate course for computer science and mathematics students on proof theory. The course brings a solid background for students who pretend to do research in automated deduction and formal methods.

    Bibliography:


    Topics in Computation: Type Theory (Tópicos em Computação: Teoria dos Tipos)

    this is a semester course for mathematics and computer science graduate students on foundations of type theory and its applications to semantics and logic of computation. Untyped lambda calculus and its typed versions making emphasis on the simple typed case à la Church and à la Curry are covered. Type checking, type inference and the problem of inhabitation are considered.

    Bibliography:


    Research Topics in Computation: Formal Methods
    Summer course offered by the Graduate Program in Informatics, Summer Semester 2010 (Prof. Mauricio Ayala Rincón and Cesar Muñoz, NASA Langley Research Center)
    A short course also offered at ITIV, Karlsruher Institute für Technologie (Prof. Mauricio Ayala Rincón)

    this is a summer course on fundamentals of formal methods and proof technologies in the proof assistant PVS.

    foils and exercises for the short course at ITIV.


    Computational Complexity and Computability (Complexidade Computacional e Computabilidade):
    Offered by the Graduate Program of the Departamento de Matemática, First Semester 2010 (Prof. Mauricio Ayala Rincón)
    this is a semester course for mathematics and computer science graduate students on foundations of theory of complexity: the study of why some problems are so hard to solve by computers and, in general, the classification of problems with respect to the necessary computational resources of its solutions. Turing Machines are reviewed introducing the classic computational complexity classes according to the use of computational (time/space) resources. Relations between computational complexity classes are studied from the structural point of view. NP-complete and PSPACE-complete problems are examined. Also, probabilistic algorithms, that result from approximate solution for intratable problems, as well as the corresponding probabilistic classes are considered.

    Bibliography:

    • S. Arora and B. Barak, Computational Complexity: A Modern Approach, Cambridge University Press, 2009.
    • S. Homer and A. L. Selman, Computability and Complexity Theory, Texts in Computer Science, Springer, 2001.
    • D.P. Bovet and P. Crescenzi, Introduction to the Theory of Complexity, C.A.R. Hoare Series Editor. Prentice-Hall, 1994.
    • J.L. Balcázar and J. Díaz and J. Gabarró, Structural Complexity I, EATCS monographs on Theoretical Computer Science. Springer, econd edition, 1995.
    • C.H. Papadimitriou, Computational Complexity, Addison-Wesley Publishing Company, 1994.

    Details of the last program of the course, second semester 2005 (in Portuguese) (postscript) (PDF)


    Analysis of Algorithms (Análise de Algoritmos)
    Offered by the Undergraduate Program of the Departamento de Matemática, First Semester 2009 (Prof. Mauricio Ayala Rincón)

    this is a semester course for mathematic and computer science undergraduate students on design and analysis of computer algorithms. Regularly, simple computer data structures and a collection of efficient algorithms for classical computer science problems, such as sorting, searching, string pattern matching, graph theory problems, mathematical problems, etc. are studied. Also, basic computer programming techniques are presented: divide and conquer, dynamic programming, etc. The course includes a brief introduction on algorithmic complexity classes and parallel models of computation.

    Didactic material of the course, semester 2009/I


    Introduction to Formal Logic (313998 Introdução à Lógica Formal)

    Offered by the Graduate Program of the Departamento de Matemática, First Semester 2009 (Prof. Mauricio Ayala Rincón)

    this is a semester course for mathematics and computer science graduate students on formal logic. The focus is on the expressiveness and limitations of first-order logic. Gödel completeness and incompleteness theorems are carefully studied and Lindström theorems on the maximality of first-order logic as a language to formalize mathematics which satisfies the compactness property and the Löwehneim-Skolem property. The course brings a solid background for mathematics and computer science students who want research in formal methods, proof and type theory.

    Bibliography:


    Topics in Computation: advanced rewriting theory (Tópicos em Computação: teoria de reescrita avançada)
    Offered by the Graduate Program of the Departamento de Matemática, Second Semester 2007 (Prof. Mauricio Ayala Rincón)

    this is a semester course for mathematics and computer science graduate students on advanced topics on rewriting theory.

    Bibliography:

    • F. Baader and T. Nipkow, Term Rewriting and All That Cambridge University Press, 1998.
    • TERESE Term Rewriting Systems by Terese, Cambridge Tracts in Theoretical Computer Science. CUP 2003.


    Advanced Automata Theory and Formal Languages (Linguagens Formais e Autômatos II):
    this is a semester graduate course for mathematics students on algebraic foundations of formal language and computational model theory. The goal of the course is the presentation of the regular and context free languages and their associated models in an algebraic setting.

    Bibliography:


    Numerical Calculus (Cálculo Numérico)
    this is a undergraduate course on foundations of numerical calculus for mathematics, physics and engineering students.
    Didactic material of the course, semester 2005/I


    Topics in Computation: Formal Logic and Computability (Tópicos em Computação: Lógica formal e computabilidade)
    this is a semester course for mathematics and computer science graduate students on formal logic and computability.

    Bibliography:


    Topics in Foundations and Methods of Computation: Algorithms for Computational Biology (Tópicos em Fundamentos e Métodos da Computação: Algoritmos para biologia computacional)
    this is a semester course for mathematics and computer science graduate students on formal logic and computability.

    Bibliography:


    Analysis and Complexity of Algorithms (Projeto e Complexidade de Algoritmos):
    this is a semester course for computer science graduate students on advanced design and analysis of computer algorithms. The course includes a very brief introduction on complexity theory.

    Bibliography:

    Grades (Menções) 2003 I


    Automata Theory and Formal Languages (Linguagens Formais e Autômatos):
    this is a semester undergraduate course for computer science students on foundations of formal language and models of computation. Goals of the course are presentation of the Chomsky Hierarchy and computability notions from a formal point of view. Regular, context free, context sensitive and recursive enumerable languages are studied presenting their corresponding grammars and model s of computation: finite automata, pushdown automata, linear bounded automata and Turing Machines, respectively. Turing machines are reviewed presenting the Church-Turing Thesis and undecidability examples.

    Didactic material of the course, semester 2003/I
    Topics in Computation: Category Theory and Computation (Tópicos em Computação: Teoria de Categorias e Computação):

    this is a semester course for mathematics and computer science graduate students on category theory and its applications in computer science.

    Bibliography:


    Topics in Computation: Advanced Type Theory (Tópicos em Computação: Teoria dos Tipos Avançada)

    this is a semester course for mathematics and computer science graduate students on advanced topics of type theory and its applications to semantics and logic of computation. The problem of inhabitation, dependant and intersection types, typed explicit substitutions calculi and the Barendregt cube are studied.

    Bibliography:


    Seminar on Categories and Computer Science (Seminário de Computação):
    this is a semester seminar course for mathematic and computer science graduate students on foundations of theory of categories and its applications to computer science. In particular, we are interested in the study of applications of categorical methods to rewriting theory.

    Bibliography:


    Seminar on Computational Complexity (Seminário de Computação): this is a semester seminar for mathematic graduate students on foundations of theory of complexity. Turing Machines are reviewed introducing classic computational complexity classes according to the use of computational resources time/space. Relations between computational complexity classes are studied from the structural point of view. NP-complete and PSPACE-complete problems are examined. Probabilistic algorithms and classes as well as the polynomial time hierarchy are studied too.

    Bibliography:

    Details of the last program of the course, first semester 1997 (in Portuguese)


    Calculus I (Cálculo Diferencial e Integral):


    Introduction to the Theory of Graphs (Introdução à Teoria dos Grafos):

    this is a semester course for mathematics and computer science undergraduate students on foundations of theory of graphs, that is given from the algorithmic point of view: diverse applications of this formalism for modeling very simple real problems are given and, subsequently, efficient computational solutions are discused. Topics covered range from the very simple algorithms for searching paths in graphs to the graph coloring problem.

    Bibliography:

    • A. H. Aho, J. E. Hopcroft and J. D. Ullman, The Design and Analysis of Computer Algorithms. Addisson-Wesley, 1974.
    • R. Sedgewick, Algorithms in C++. Addison-Wesley, 1992.
    • T. H. Cormen, C. E. Leiserson, R. L. Rivest and C. Stein, Introduction to Algorithms - Second Edition -. MIT press, 2001.
    • N. Christofides, Graph Theory An Algorithmic Approach Academic Press, 1975.
    • S. Even, Graph Algorithms Computer Science Press, 1979.

    Other courses I like:

    • Undergraduate courses:
      • Numerical Calculus.
    • Graduate courses:
      • Foundations of Mathematical Logic Usually offered by Prof. Haydeé Werneck Poubel first semester every year
      • Analysis of Algorithms and Computer Structures
      • Formal Languages II
      • --> Could be offered second semester 2000 according to alumni interest!
      • Seminar on Mathematical Logic
      • Computational Complexity