Cronograma de aulas

DONE Aula 01 - Introdução e motivação <2022-06-06 Mon 19:00>

Material de aula:

  • Notas de aula
    • Ler até a página 14 (versão de [2022-06-07 Tue]);
    • Fazer até o exercício 8.
  • pdf (introdução da bibliografia principal)

Resumo da aula:

Apresentamos o protocolo covid adotado pela UnB, e o plano de ensino do curso.

DONE Aula 02 - Introdução à Lógica Proposicional (LP) <2022-06-08 Wed 19:00>

Material da aula:

  • Arquivo para utilização do ProofWeb em uma instalação local do Coq: ProofWeb.v

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.

DONE Aula 03 - Dedução Natural na Lógica Proposicional Minimal (LPM) <2022-06-13 Mon 19:00>

Material da aula:

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.

DONE Aula 04 - Exercícios de Dedução Natural na LPM <2022-06-15 Wed 19:00>

Material da aula:

  • Leitura das notas de aula (até página 21) e resolução até o exercício 29.

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.

DONE Aula 05 - Exercícios de Dedução Natural na LPM <2022-06-20 Mon 19:00>

Material da aula:

  • Leitura: O mesmo material da aula anterior.

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.

DONE Aula 06 - Apresentação do assistente de provas Coq <2022-06-22 Wed 19:00>

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)

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)

TODO Aula 07 - Dedução Natural na Lógica Proposicional Intuicionista (LPI) <2022-06-27 Mon 19:00>

Material da aula:

TODO Resumo da aula:

TODO Aula 08 - Dedução Natural na Lógica Proposicional Clássica (LPC) <2022-06-29 Wed 19:00>

TODO Aula 09 - Semântica da LPC <2022-07-04 Mon 19:00>

TODO Aula 10 - Introdução à Lógica de Primeira Ordem (LPO) <2022-07-06 Wed 19:00>

TODO Aula 11 - Dedução Natural na LPO <2022-07-11 Mon 19:00>

TODO Aula 12 - Indução Matemática <2022-07-13 Wed 19:00>

TODO Aula 13 - Indução Estrutural <2022-07-18 Mon 19:00>

TODO Aula 14 - Correção da LPC <2022-07-20 Wed 19:00>

TODO Aula 15 - Completude da LPC <2022-07-25 Mon 19:00>

TODO Aula 16 - Correção da LPO <2022-07-27 Wed 19:00>

TODO Aula 17 - Completude da LPO <2022-08-01 Mon 19:00>

TODO Aula 18 - Primeira prova <2022-08-03 Wed 19:00>

TODO Aula 19 - Cálculo de sequentes (CS) <2022-08-08 Mon 19:00>

TODO Aula 20 - Exercícios em CS <2022-08-10 Wed 19:00>

TODO Aula 21 - Exercícios em CS <2022-08-15 Mon 19:00>

TODO Aula 22 - DN versus CS <2022-08-17 Wed 19:00>

TODO Aula 23 - DN versus CS <2022-08-22 Mon 19:00>

TODO Aula 24 - DN versus CS <2022-08-24 Wed 19:00>

Semana Universitária <2022-08-29 Mon>

Semana Universitária <2022-08-31 Wed>

TODO Aula 25 - Indecidibilidade da LPO <2022-09-05 Mon 19:00>

Feriado <2022-09-07 Wed>

TODO Aula 26 - Discussão do projeto <2022-09-12 Mon 19:00>

TODO Aula 27 - Discussão do projeto <2022-09-14 Wed 19:00>

TODO Aula 28 - Segunda prova <2022-09-19 Mon 19:00>