Academics

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:

H. D. Ebbinghaus, J. Flum, and W. Thomas, Mathematical Logic. Springer, 1984.
D.W. Loveland and R.E. Hodel, Three Views of Logic: Mathematics, Philosophy, and Computer SciencePrinceton University Press, 2014.
D. van Dalen, Logic and Structure , 5th ed., Springer Verlag, 2012.
R. Cori and D. Lascar, Mathematical Logic - a course with exercises. Oxford UP, 2000.
W. Rautenberg, Einfürung in die Mathematische Logik. Vieweg, 2002.
H. B. Enderton, A Mathematical Introduction to Logic. Academic Press Inc., 1972.
A. Yasuhara, Recursive Function Theory and Logic. Computer Science and Applied Mathematics. Academic Press, 1971.

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.

H.P. Barendregt and W. Dekkers and R. Statman, Lambda Calculus with Types Cambridge University Press, 2013.
H.P. Barendregt, Lambda Calculus with Types. Chapter in Handbook of Logic in Computer Science, Vol. 2, pages 117-309, S. Abramsky, D.M. Gabbay and T.S.E. Maibaum, eds., Clarendon Press | Oxford, 1992. 1974.
J.R. Hindley, Basic Simple Type Theory. Cambridge Tracts in Theoretical Computer Science, n. 42, Cambridge University Press, 1997.
H. Simmons, Derivation and Computation: Taking the Curry-Howard Correspondence Seriously. Cambridge Tracts in Theoretical Computer Science, n. 51, Cambridge University Press, 2000.
A. Church, A Formulation of the Simple Theory of Types Journal of Symbolic Logic, 5:56-68, 1940.
Kamareddine, F. D. and T. Laan and R. Nederpelt, A Modern Perspective on Type Theory Applied Logic Series 29, Kluewer, 2004.
F. Kamareddine, T. Laan and R. Nederpelt, Types in logic and mathematics before 1940, in Bull. Symbolic Logic, 8(2):185-245, 2002.
Online Resources from Peter Aczel URL: http://www.cs.man.ac.uk/~petera/Types_course/types_resources.html

Program for the semester 2020/I Classes started on Monday, 9th March 2020 - Sala A, Térreo do MAT

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:

A. S. Troelstra and H. Schwitchtenberg, Basic Proof Theory Cambridge Tracts in Theoretical Computer Science, CUP 2000.
S. R. Buss (Ed), Handbook of Proof Theory, Studies in Logic and the Foundations of Mathematics, Vol. 137, North Holland, Elsevier, 1998.
S. Negri and J. von Plato, Structural Proof Theory CUP 2001.
P. Aczel, H. Simmons and S. Wainer (Eds), Proof Theory CUP 1994.

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:

H. D. Ebbinghaus, J. Flum, and W. Thomas, Mathematical Logic. Springer, 1984.
D.W. Loveland and R.E. Hodel, Three Views of Logic: Mathematics, Philosophy, and Computer SciencePrinceton University Press, 2014.
D. van Dalen, Logic and Structure , 5th ed., Springer Verlag, 2012.
R. Cori and D. Lascar, Mathematical Logic - a course with exercises. Oxford UP, 2000.
W. Rautenberg, Einfürung in die Mathematische Logik. Vieweg, 2002.
H. B. Enderton, A Mathematical Introduction to Logic. Academic Press Inc., 1972.
A. Yasuhara, Recursive Function Theory and Logic. Computer Science and Applied Mathematics. Academic Press, 1971.

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:

A. S. Troelstra and H. Schwitchtenberg, Basic Proof Theory Cambridge Tracts in Theoretical Computer Science, CUP 2000.
S. R. Buss (Ed), Handbook of Proof Theory, Studies in Logic and the Foundations of Mathematics, Vol. 137, North Holland, Elsevier, 1998.
S. Negri and J. von Plato, Structural Proof Theory CUP 2001.
P. Aczel, H. Simmons and S. Wainer (Eds), Proof Theory CUP 1994.

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:

H.P. Barendregt, Lambda Calculus with Types. Chapter in Handbook of Logic in Computer Science, Vol. 2, pages 117-309, S. Abramsky, D.M. Gabbay and T.S.E. Maibaum, eds., Clarendon Press | Oxford, 1992. 1974.
J.R. Hindley, Basic Simple Type Theory. Cambridge Tracts in Theoretical Computer Science, n. 42, Cambridge University Press, 1997.
H. Simmons, Derivation and Computation: Taking the Curry-Howard Correspondence Seriously. Cambridge Tracts in Theoretical Computer Science, n. 51, Cambridge University Press, 2000.
A. Church, A Formulation of the Simple Theory of Types Journal of Symbolic Logic, 5:56-68, 1940.
Kamareddine, F. D. and T. Laan and R. Nederpelt, A Modern Perspective on Type Theory Applied Logic Series 29, Kluewer, 2004.
F. Kamareddine, T. Laan and R. Nederpelt, Types in logic and mathematics before 1940, in Bull. Symbolic Logic, 8(2):185-245, 2002.
Online Resources from Peter Aczel URL: http://www.cs.man.ac.uk/~petera/Types_course/types_resources.html
- Lecture notes - by Ralph Loader (39 pages)
- The impact of the lambda calculus in logic and computer science - by Henk Barendregt
- Foundations of Functional Programming Lecture Notes, by Larry Paulson (54 pages)
- Lambda Calculi with Types, by Henk Barendregt, Handbook of Logic in Computer Science, Volume II (193 pages)
- Proof Assistants using Dependent Type Systems , by Henk Barendregt and Herman Geuvers, Handbook of Automated Reasoning, edited by Alan Robinson and Andrei Voronkov, 2001, (89 pages)
- Lecture notes, by Luke Ong (89 pages)
- Lectures on the Curry-Howard Isomorphism by Morten Heine B. Sorensen (University of Copenhagen), Pawel Urzyczyn (University of Warsaw) (275 pages)
- Type Systems, By Luca Cardelli (42 pages)
  An introductory overview
- Lecture Notes by H. Schwichtenberg
- Introduction to the Literature on Semantics, by Gary T. Leavens

Ementa primeiro semestre de 2011 ( PDF) In Portuguese.

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:

H. D. Ebbinghaus, J. Flum, and W. Thomas, Mathematical Logic. Springer, 1984.
W. Rautenberg, Einfürung in die Mathematische Logik. Vieweg, 2002.
H. B. Enderton, A Mathematical Introduction to Logic. Academic Press Inc., 1972.
A. Yasuhara, Recursive Function Theory and Logic. Computer Science and Applied Mathematics. Academic Press, 1971.

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:

D. Kozen, Automata and Computability Springer-Verlag, 1997.
C.C. Sims, Computation with Finitely Presented Groups (Chapter 3), CUP 1994.

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:

G. S. Boolos, J. P. Burgess, and R. C. Jeffrey, Computability and Logic. Cambridge University Press, fourth edition, 2002.
H. D. Ebbinghaus, J. Flum, and W. Thomas, Mathematical Logic. Springer, 1984.
H. B. Enderton, A Mathematical Introduction to Logic. Academic Press Inc., 1972.
A. Yasuhara, Recursive Function Theory and Logic. Computer Science and Applied Mathematics. Academic Press, 1971.

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:

D. Gusfield, Algorithms on Strings, Trees and Sequences: Computer Science and Computational Biology. Cambridge University Press, 1997.
J. C. Setubal and J. Meidanis, Introduction to Computational Molecular Biology . PWS Publushing Company, 1997.
D. Voet and J. G. Voet, Biochemistry. John Wiley and Sons, 1990.
Michael S. Waterman, Introduction to Computational Biology: Maps, Sequences and Genomes. CRC Press, 1995.
P. A. Pevzner, Computational Molecular Biology: An Algorithmic Approach. MIT Press, 2000.
R. Durbin, S. R. Eddy, A. Krogh and G. Mitchison, Biological Sequence Analysis : Probabilistic Models of Proteins and Nucleic Acids. Cambridge University Press, 1999.
Bryan Bergeron, Bioinformatics Computing. Prentice Hall PTR, 2002.

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:

S. Baase and A. van Gelder Computer Algorithms, Introduction to Design and Analysis, Third Edition. Addison-Wesley, 1998.
A. H. Aho, J. E. Hopcroft and J. D. Ullman, The Design and Analysis of Computer Algorithms. Addisson-Wesley, 1974.
T. H. Cormen, C. E. Leiserson, R. L. Rivest and C. Stein, Introduction to Algorithms - Second Edition -. MIT press, 2001.
D. Gusfield, Algorithms on Strings, Trees and Sequences. Cambridge University Press, 1997.
J. von sur Gathen and J. Gerhard, Modern Computer Algebra. Cambridge University Press, 1999.

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:

P. Blauth Menezes , E. H. Haeusler, Teoria das Categorias para Ciência da Computação. Sagra Luzzatto, 2001,
R. F. C. Walters, Categories and Computer Science. Cambridge Computer Science Texts, 1991.
R. Bird and O. de Moor, Algebra of Programming. C.A.R. Hoare Series Editor, 100th Title, Prentice Hall International Series in Computer Science, 1997.

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:

H.P. Barendregt, Lambda Calculus with Types. Chapter in Handbook of Logic in Computer Science, Vol. 2, pages 117-309, S. Abramsky, D.M. Gabbay and T.S.E. Maibaum, eds., Clarendon Press | Oxford, 1992. 1974.
J.R. Hindley, Basic Simple Type Theory. Cambridge Tracts in Theoretical Computer Science, n. 42, Cambridge University Press, 1997.
J.C. Mitchell, Foundations for Programming Languages. MIT Press, 1996.

Ementa segundo semestre de 2002 (postscript 56 KB) In Portuguese.

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:

R. F. C. Walters, Categories and Computer Science. Cambridge Computer Science Texts, 1991.
R. Bird and O. de Moor, Algebra of Programming. C.A.R. Hoare Series Editor, 100th Title, Prentice Hall International Series in Computer Science, 1997.
E. Moggi and G. Rosolini (Eds), Category Theory and Computer Science, Seventh Int. Conference, CTCS'97, Santa Margherita Ligure, Italy, September 1997. Lecture Notes in Computer Science 1290. Springer, 1997.
F. Baader and T. Nipkow, Term Rewriting and All That Cambridge University Press, 1998.

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:

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, first semester 1997 (in Portuguese)

Calculus I (Cálculo Diferencial e Integral):

Menções da disciplina para o primeiro semestre de 2002 Revisão Prova 1: Quarta, 17.07.2002, 11:00-12:00

Material da disciplina (Gavaritos, Listas de Exercícios, etc)

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.

Grades (Menções) 2001 II COMPLETO, 26.04.2002
Ementa da disciplina para o segundo semestre de 2001 modificada após a greve ( postscript 100 KB) In Portuguese.

Monografia sobre o teorema das quatro cores para o segundo semestre de 2001 ( postscript 63 KB) In Portuguese.

Primeira prova, segundo semestre de 2000 (postscript 100 KB) In Portuguese.

Segunda prova, segundo semestre de 2000 (postscript 100 KB) In Portuguese.

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
Seminar on Mathematical Logic
Computational Complexity

Mauricio Ayala Rincón

Group of Theory of Computation

Department of Mathematics

University of Brasília

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

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