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 2017 (Prof. Mauricio Ayala Rincón)

this is a one semester course for computer science undergraduate students on propositional and predicate logic and their applications in computer science mainly for verification. Despite concepts such as correctness and completeness and incompleteness are reviewed the emphasis is on deduction methods and their applications in specification, formalization and verification.

Didactic material of the course, semester 2017/I Classes started on Wednesday 8th March 2017


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
Classes started on Monday, 13 March 2017
Menções 2017


Theory of Computing (316296 Teoria da Computação)
Offered by the Graduate Program of the Departamento de Computação, Second Semester 2016 (Prof. Mauricio Ayala Rincón)


this is a one semester course for mathematic and computer science engineering graduate students on mathematical foundations of computation. Semantics of computation is focused from the point of view of the logic and functional programming paradigms. Initially, the resolution principle, first-order unification, fixed-point theory and then SLD-resolution, its completeness and its soundness are formally studied. After that, rewriting theory is examined as the more appropriate formalism for reasoning about the functional programming paradigm. Both paradigms are checked showing that their expressiveness is enough to allow the specification of the class of recursive computable functions.

Didactic material of the course, semester 2016/II


Proof Theory (303666 Teoria de Prova)

Offered by the Graduate Program in Informatics, First Semester 2016 (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 2016/I


Topics in Computation: Type Theory (Tópicos em Fundamentos e Métodos da Computação: Teoria dos Tipos)

Offered by the graduate Program in Informatics, First Semester 2015 (Prof. Mauricio Ayala Rincón)

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:


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:

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:


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