Carga horária da disciplina: 4 horas/aula

Professor(es) em 2022-1

Turma 11

Professor: Rodrigo Geraldo Ribeiro - www | e-mail Horários: Segunda-feira (17h10 - 18h50) Quarta-feira (17h10 - 18h50)

Objetivos

O objetivo do curso é expor os alunos a diferentes formalismos da lógica matemática e suas aplicações para solução de problemas na ciência da computação. Os seguintes resultados são esperados após o curso desta disciplina:
• Codificar problemas usando fórmulas da lógica e uso de resolvedores SAT e SMT para solucioná-los.
• Compreender a relação entre a lógica e teoria de tipos e ser capaz de usar assistentes de provas para
construção de formalizações.
• Construir e compreender provas por indução e co-indução para correção de programas.
• Modelar problemas usando verificadores de modelos para lógica temporal.

Ementa

1. Lógica de primeira ordem, o algoritmo DPLL e uso de SAT e SMT solvers.
2. Lógica intuicionista e teoria de tipos. Uso de assistentes de prova.
3. Indução e co-indução e seu uso para verificação de programas.
4. Lógica Temporal e verificação de modelos.

Conteúdo Programático

- 1) Apresentação da disciplina: Motivação e critérios de avaliação (2 aulas)
- 2) Revisão de lógica proposicional: Sintaxe, semântica e dedução natural (2 aulas).
- 3) Revisão de lógica de predicados: Sintaxe, semântica e dedução natural (2 aulas).
- 4) O problema SAT e o algoritmo DPLL (4 aulas).
- 5) Modelagem de problemas usando SAT e uso de resolvedores SAT (4 aulas).
- 6) Satisfiability Modulo Theories (SMT) e o algoritmo DPLL-T (4 aulas).
- 7) Modelagem de problemas usando SMT e resolvedores SMT (2 aulas).
- 8) Lógica intuicionista e lambda-cálculo tipado: o isomorfismo de Curry-Howard (4 aulas)
- 9) Introdução ao uso de assistentes de provas baseado em teoria de tipos (2 aulas)
- 10) Revisão: indução matemática. Provas por indução estrutural (2 aulas)
- 11) Indução sobre relações bem formadas (2 aulas).
- 12) Provas por co-indução. Uso de co-indução em assistentes de provas (2 aulas)
- 13) Lógica temporal e verificação de modelos (4 aulas).

Bibliografia

- Básica
- 1) HUTH, MICHAEL; RYAN, MARK. Lógica para ciência da computação: Modelagem e Argumentação sobre sistemas. 2a edição, LTC, 2008.
- 2) BERTOT, YVES; CASTERRÁN, PIERRE. Interactive Theorem Proving and Program Development: The Coq’Art – The calculus of inductive constructions. 1a edição. Springer-Verlag. 2002
- 3) MITCHEL, JOHN. Foundations for Programming Languages, MIT Press, 1996.

Bibliografia complementar

- 1) BIERE, ARMIN; HEULE, MARTIN. Handbook of Satisfiability: Volume 185 Frontiers in Artificial Intelligence and Applications, 1a edição, IOS Press.
- 2) CLARKE, EDMUND; GRUMBERG, ORNA. Model Checking, 1a edição, MIT Press, 1999.
- 3) BAIER, CHRISTEL; KATOEN, JOOST-PIETER. Principles of Model Checking. 1a edição. MIT Press. 2008.
- 4) SANGIORGI, DAVID. Introduction to Bisimulation and Coinduction, 1a edição. Cambridge University Press.
- 2011.