MENU: [ Avisos | Informações Gerais | Regras | Plano de Atividades ]
Última atualização: 27/09/2017 (curso da turma).
Leia toda esta página no início do semestre: ela contém informações essenciais, como as regras para solicitação de segunda chamada e para o cálculo da nota na disciplina.
Esta página está em contínua construção. Por favor, entre em contato caso você precise de alguma informação adicional, ou caso acredite ter encontrado um erro aqui. Obrigado!
Nesta disciplina, nós aprendemos a usar o assistente de prova Coq, utilizando como livro-texto principalmente o excelente Software Foundations. Na parte final da disciplina, estudamos automatização de demonstrações pelo CPDT, que é um livro mais aprofundado.
Na regulamentação desta disciplina você pode acessar as informações oficiais sobre ela, incluindo justificativa, objetivos, ementa e bibliografia. Parte dessas informações também está no PPC do curso de Ciência da Computação (página 123).
O conteúdo e a data de cada aula e prova da disciplina está no plano de atividades. Se você percebeu um choque de datas importantes com outra disciplina, ou se você já sabe que não poderá fazer uma das nossas provas na data prevista, por favor me comunique o quanto antes!
A minha sugestão para a obtenção de um bom desempenho na disciplina é (1) acompanhar as aulas com atenção, tirando dúvidas o quanto antes, e (2) fazer os exercícios com regularidade. Caso você possua uma dúvida no horário da aula, o ideal é tirá-la na própria ocasião, para que os demais alunos também se beneficiem das explicações. Esteja, porém, à vontade para me contactar fora do horário de aula.
Segunda chamada: consulte as regras para a solicitação de prova de segunda chamada.
Nota da disciplina: Consistirá na média aritmética das notas obtidas pelo aluno nas 4 avaliações parciais da disciplina:
| Média das APs | ≥ 7 | 7 > média ≥ 4 | < 4 |
|---|---|---|---|
| Situação | Aprovado | AF | Reprovado |
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 Independência do Brasil | |
| 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 |