Cronograma de aulas
DONE Aula 01 - Introdução e motivação
Resumo da aula:
Apresentamos o protocolo covid adotado pela UnB, e o plano de ensino do curso.
- Link para a gravação da aula: Teams - aula 01
DONE Aula 02 - Introdução à Lógica Proposicional (LP)
Resumo da aula:
Reforçamos a necessidade no uso de máscara dentro da sala. Apresentamos os pontos essenciais do texto contendo a apresentação do fragmento implicacional da lógica proposicional. No final da aula, vimos como o sistema ProofWeb pode ser útil para verificar se a solução de um exercício está correta. Exercícios propostos: 1-8 das notas de aula.
- Link para a gravação da aula: Teams - aula 02
- Anotações da aula: pdf
DONE Aula 03 - Dedução Natural na Lógica Proposicional Minimal (LPM)
Resumo da aula:
Resolvemos os exercícios 3 e 8 das notas de aula, e o exercício 8 foi refeito no ProofWeb (link para o arquivo Coq). Sugerimos a leitura das páginas 14-21 para a próxima aula, incluindo a resolução dos exercícios 9-29.
- Link para a gravação da aula: Teams - aula 03
- Anotações da aula: pdf
DONE Aula 04 - Exercícios de Dedução Natural na LPM
Resumo da aula:
Os dois primeiros links abaixo são vídeos de apresentação da teoria. No primeiro, apresentamos as regras restantes de Dedução Natural para a Lógica Proposicional Minimal. O segundo vídeo apresenta uma simplificação na notação a ser utilizada. O terceiro link apresenta uma reunião síncrona com comentários sobre o andamento do curso.
- Apresentação das regras restantes da LPM: Teams - aula 04 - parte 01
- Simplificação da notação na LPM: Teams - aula 04 - parte 02
- Link para a gravação da aula: Teams - aula 04 - parte 03
- Anotações da aula: pdf
DONE Aula 05 - Exercícios de Dedução Natural na LPM
Resumo da aula:
Iniciamos com informações gerais sobre a página web do curso. Em seguida provamos uma das leis de De Morgan (propagação da negação sobre a disjunção - exercício 18) utilizando contextos implícitos e explícitos. Por fim, resolvemos o exercício 6 que se refere a uma propriedade no fragmento implicacional da lógica proposicional. O exercício 6 também foi resolvido utilizando tanto contexto implícito quanto contexto explícito. Concluímos, a partir do minuto 51, com orientações sobre entrega de atividades no Teams.
- Resolução de exercícios: Teams - aula 05
- Anotações da aula: pdf
DONE Aula 06 - Apresentação do assistente de provas Coq
Material da aula:
- Leitura: Seção 2.1 das notas de aula.
- Página do jscoq (o Coq via Browser) (link)
- Página com alguns comandos do jscoq (link)
- Página principal do Coq (link)
- Coq cheatsheet (pdf)
- Táticas Coq
Resumo da aula:
Apresentamos o Coq utilizando tanto uma instalação local, quanto a versão web (https://coq.vercel.app/). Em seguida resolvemos alguns exercícios utilizando as duas interfaces.
- Link para a gravação da aula: Teams - aula 06
- Anotações da aula: feitas diretamente na tela (ver gravação da aula)
DONE Aula 07 - Dedução Natural na Lógica Proposicional Intuicionista (LPI)
TODO Resumo da aula:
Iniciamos discutindo dúvidas apresentadas pelos alunos, e concluímos com a apresentação da lógica proposicional intuicionista.
- Link para a gravação da aula: Teams - aula 07
- Anotações de aula: pdf
DONE Aula 08 - Discussão de dúvidas
Resumo da aula:
Discutimos as dúvidas apresentadas com resolução de alguns exercícios. A leitura da seção sobre a lógica proposicional clássica (notas de aulas) deve ser feita antes da próxima aula.
- Link para a gravação da aula: Teams - aula 08
- Anotações da aula: pdf
DONE Aula 09 - Dedução Natural na Lógica Proposicional Clássica (LPC)
Material da aula:
- Leitura: Seção 2.3 das notas de aula
- pdf (semântica da lógica proposicional clássica - bibliografia principal)
- pdf (correção da lógica proposicional clássica - bibliografia principal)
- pdf (completude da lógica proposicional clássica - bibliografia principal)
Resumo da aula:
Discutimos dúvidas de exercícios.
- Link para a gravação da aula: Teams - aula 09
- Anotações da aula: pdf
DONE Aula 10 - Dedução Natural na Lógica de Primeira Ordem (LPO)
Material da aula:
- Leitura: Capítulo 3 das notas de aula
- pdf (dedução natural na lógica de primeira ordem - bibliografia principal)
Resumo da aula:
Resolvemos alguns exercícios da lógica proposicional, e em seguida apresentamos a lógica de primeira ordem. Concluímos com a resolução de alguns exercícios na lógica de primeira ordem.
- Link para a gravação da aula: Teams - aula 10
- Anotações da aula: pdf
DONE Aula 11 - Indução Matemática
Material da aula:
- Leitura: Seção 3.1 das notas de aula
- Playlist sobre indução (com exercícios): Canal Ad infinitum
- Leitura: indução
Resumo da aula:
Resolvemos alguns exercícios na LPO, e explicamos alguns detalhes da operação de substituição na LPO. Em seguida, apresentamos os princípios da indução matemática, indução generalizada e indução forte com alguns exemplos.
- Link para a gravação da aula: Teams - aula 11
- Anotações da aula: pdf
DONE Aula 12 - Indução Estrutural
Resumo da aula:
Apresentamos o princípio da indução estrutural, e resolvemos alguns exercícios como exemplos. Em seguida, apresentamos algumas propostas para o projeto.
- Link para a gravação da aula: Teams - aula 12
- Anotações da aula: pdf
DONE Aula 13 - Descrição do projeto
Resumo da aula:
Fizemos o gabarito da atividade 3, e durante a aula foram construídas 3 provas distintas. Em seguida, iniciamos a descrição do projeto.
- Link para a gravação da aula: Teams - aula 13
- Arquivo Coq: link
- Anotações da aula: pdf
DONE Aula 14 - Discussão de exercícios
Resumo aula:
Aula de preparação para a prova com discussão de exercícios.
- Link para a gravação da aula: Teams - aula 14
Reunião anual da SBPC
Reunião anual da SBPC
DONE Aula 15 - Discussão de exercícios
Resumo da aula:
Discussão de dúvidas.
- Link para a gravação da aula: Teams - aula 15
- Anotações da aula: pdf
DONE Aula 17 - Discussão do projeto
Material da aula:
- Arquivo Coq: files/lc1_2022_1_projeto.v
- Arquivo TeX (relatório): files/lc1-2022-1-relatorio.tex
- Biblioteca CoqDoc: files/coqdoc.sty
Resumo da aula:
Fizemos uma discussão geral sobre a estrutura do projeto, e mostramos como gerar um relatório em formato pdf diretamente a partir do arquivo coq.
- Link para a gravação da aula: Teams - aula 17
DONE Aula 18 - Correção da LPC
DONE Aula 19 - Semântica da LPO e projeto
Material da aula:
- Seção 3.2 das notas de aula
- Seção 2.4 da bibliografia principal: pdf
- Arquivo coq: files/lc1_2022_1_projeto1508.v
DONE Aula 20 - Completude da LP e projeto
DONE Aula 21 - Correção da LPO
DONE Aula 22 - Completude da LPO
Resumo da aula:
A prova da completude ficou como recomendação de leitura, e durante a aula resolvemos alguns exercícios.
- Link para a gravação da aula:
- Anotações da aula: pdf