Lógica Computacional 1
2020-2
Table of Contents
Quadro de avisos
Link para a primeira aula que será realizada em via Microsoft Teams institucional: clique aqui
Cronograma de aulas
- 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
- 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.
- Desafios lógicos e Semântica da Lógica Proposicional
- Resolução informal de alguns problemas lógicos
- Resolução via tabelas de verdade
- Resolução informal de alguns problemas lógicos
- 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
- 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
- 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
- Introdução ao sistema de DN na LPI, e solução dos sequentes construídos na aula anterior via DN
- Assistentes de Prova - parte 1
- Introdução ao assistente de provas Coq, via a reconstrução das provas feitas manualmente na aula anterior
- Introdução ao assistente de provas Coq, via a reconstrução das provas feitas manualmente na aula anterior
- 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
- Introdução à LPC via o sistema DN, e resolução manual de sequentes de exercícios anteriores e exercícios novos
- Desafios lógicos - parte 2
- Assistentes de Prova - parte 2
- Resolução de diversos sequentes no Coq
- Resolução de diversos sequentes no Coq
- Semântica da LPC
- Tabelas de verdade
- Tabelas de verdade
- 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
- Indução matemática e indução estrutural
- Assistentes de Prova - parte 3
- Exercícios envolvendo indução
- Exercícios envolvendo indução
- Lógica de Primeira Ordem (LPO)
- Disponibilização da segunda lista de exercícios
- Disponibilização da segunda lista de exercícios
- Formalização de algoritmos de ordenação - parte 1
- Formalização de algoritmos de ordenação - parte 2
- Formalização de algoritmos de ordenação - parte 3
- Formalização de algoritmos de ordenação - parte 4
- Assistentes de Prova - parte 4
- Apresentação da parte 2 do projeto
- Apresentação da parte 2 do projeto
- Assistentes de Prova - parte 5
- Assistentes de Prova - parte 6
- Assistentes de Prova - parte 7
- Assistentes de Prova - parte 8
- Assistentes de Prova - parte 9
- Assistentes de Prova - parte 10
- Correção da LPO
- Completude da LPO - parte 1
- Completude da LPO - parte 2
- Indecidibilidade da LPO - parte 1
- Indecidibilidade da LPO - parte 2
- Indecidibilidade da LPO - parte 3