Esta é uma disciplina de 4 créditos, e portanto ela possui (4/2)*16 = 32 encontros planejados, dos quais 27 são Aulas, 4 são Avaliações Parciais e 1 é obrigatoriamente destinado aos Encontros Universitários. Adicionalmente, poderá ser realizada também uma Avaliação Final. Cada AP cobrirá exata ou aproximadamente 3 capítulos de livro. Abaixo estão as datas e descrições de cada encontro:
| Aula | Data | Descrição |
|---|---|---|
| 01 | 17/08 | Apresentação da Disciplina; Basics. |
| 02 | 22/08 | Basics |
| 03 | 24/08 | Induction |
| 04 | 29/08 | Lists |
| 05 | 31/08 | Lists |
| * | 05/09 | AP1 |
| 07/09 | SEM AULA: Feriado da Proclamação da República | |
| 06 | 12/09 | Poly |
| 07 | 14/09 | Poly |
| 08 | 19/09 | Tactics |
| 09 | 21/09 | Tactics |
| 10 | 26/09 | Logic |
| 11 | 28/09 | Logic |
| 12 | 03/10 | Logic |
| * | 05/10 | AP2 |
| 13 | 10/10 | IndProp |
| 12/10 | SEM AULA: Feriado de Nossa Senhora Aparecida | |
| 14 | 17/10 | IndPrinciples |
| 15 | 19/10 | IndProp |
| 16 | 24/10 | IndProp |
| 17 | 26/10 | Rel |
| 18 | 31/10 | ProofObjects |
| 02/11 | SEM AULA: Feriado de Finados | |
| 19 | 07/11 | ProofObjects |
| * | 09/11 | Participação Obrigatória nos Encontros Universitários 2017 |
| * | 14/11 | AP3 |
| 20 | 16/11 | Proof Search by Logic Programming |
| 21 | 21/11 | Proof Search by Logic Programming |
| 22 | 23/11 | Proof Search by Logic Programming |
| 23 | 28/11 | Proof Search in Ltac |
| 24 | 30/11 | Proof Search in Ltac |
| 25 | 05/12 | Proof Search in Ltac |
| 26 | 07/12 | Proving in the Large |
| 27 | 12/12 | Proving in the Large |
| * | 14/12 | AP4 |
| * | 19/12 | AF |
| 21/12 | Notas da AF |