Lógica Computacional 1
2020-2

Table of Contents

Plano de ensino pdf

Quadro de avisos

Link para a primeira aula que será realizada em [2021-02-01 Seg 19:00] via Microsoft Teams institucional: clique aqui

Cronograma de aulas

  1. Introdução e Motivação
    • Será apresentada a estrutura geral do curso, incluindo os temas a serem abordados, os critérios de avaliação e as ferramentas a serem utilizadas.
    • A apresentação será feita via Microsoft Teams às 19h.
    • Resolução do primeiro desafio lógico
    • Atividade: resolução de outro desafio lógico
  2. Desafios lógicos e Semântica da Lógica Proposicional
    • Resolução informal de alguns problemas lógicos
    • Resolução via tabelas de verdade
  3. Lógica Proposicional Intuicionista (LPI)
    • Introdução da Lógica Proposicional. Serão apresentados os conectivos, a definição de sequente, e uma possível modelagem na LPI dos desafios lógicos vistos nas aulas anteriores
  4. Dedução Natural (DN) na LPI
    • Introdução ao sistema de DN na LPI, e solução dos sequentes construídos na aula anterior via DN
    • Resolução dos problemas anteriores via DN
    • Apresentação da parte 1 do projeto
  5. Assistentes de Prova - parte 1
    • Introdução ao assistente de provas Coq, via a reconstrução das provas feitas manualmente na aula anterior
  6. Lógica Proposicional Clássica (LPC)
    • Introdução à LPC via o sistema DN, e resolução manual de sequentes de exercícios anteriores e exercícios novos
    • Disponibilização da primeira lista de exercícios
  7. Desafios lógicos - parte 2
  8. Assistentes de Prova - parte 2
    • Resolução de diversos sequentes no Coq
  9. Semântica da LPC
    • Tabelas de verdade
  10. Indução, correção e completude da LPC
    • Indução matemática e indução estrutural
    • A correção da LPC
    • A completude da LPC
  11. Assistentes de Prova - parte 3
    • Exercícios envolvendo indução
  12. Lógica de Primeira Ordem (LPO)
    • Disponibilização da segunda lista de exercícios
  13. Formalização de algoritmos de ordenação - parte 1
  14. Formalização de algoritmos de ordenação - parte 2
  15. Formalização de algoritmos de ordenação - parte 3
  16. Formalização de algoritmos de ordenação - parte 4
  17. Assistentes de Prova - parte 4
    • Apresentação da parte 2 do projeto
  18. Assistentes de Prova - parte 5
  19. Assistentes de Prova - parte 6
  20. Assistentes de Prova - parte 7
  21. Assistentes de Prova - parte 8
  22. Assistentes de Prova - parte 9
  23. Assistentes de Prova - parte 10
  24. Correção da LPO
  25. Completude da LPO - parte 1
  26. Completude da LPO - parte 2
  27. Indecidibilidade da LPO - parte 1
  28. Indecidibilidade da LPO - parte 2
  29. Indecidibilidade da LPO - parte 3

Author: Flávio L. C. de Moura

Email: flavio@flaviomoura.info, flaviomoura@unb.br

Created: 2021-01-31 Dom 10:49

Validate