- Professor: Hugo Nobrega
- Turma: 9151
- Grupo de discussões: Discord
- Monitores: a definir
- Local das aulas: F2-005
Funcionamento da disciplina
O meio primário de comunicação entre os alunos, monitores e professores será o grupo listado acima.
As aulas serão realizadas em modalidade presencial, com aulas às 4as e 6as de 08:00 às 10:00 na sala F2-005 do CCMN.
Bibliografia
- Notas de aula de turmas anteriores dessa disciplina: 24-1 24-2 25-1
- Notas de aula de Petrucio Viana e Renata de Freitas (UFF)
- David J. Hunter, Fundamentos de Matemática Discreta, Capítulo 3: Pensamento Recursivo. LTC, 2019
- Apostila de autômatos, linguagens formais e computabilidade do Collier & Luis Menasché
- Raymond M. Smullyan, First-Order Logic. Springer, 1971
- Herbert B. Enderton, A Mathematical Introduction to Logic, 2a edição. Academic Press, 2001
- Flávio Silva, Marcelo Finger, Ana Cristina Melo, Lógica para Computação, 2a edição. Cengage, 2017
- João Nunes de Souza, Lógica para Ciência da Computação. Campus, 2002
Listas de Exercícios
| Lista | Data Limite de Entrega |
|---|---|
| Lista 1 | 18 de maio às 20:00 |
| Lista 2 | 30 de junho às 20:00 |
| Lista 3 | 14 de julho às 20:00 |
Regras de colaboração
As listas de exercícios podem ser entregues em duplas. Não poderá haver repetição de duplas em diferentes listas! Isso é feito para aumentar a confiança do professor ao dar uma nota individual para cada aluno no final da disciplina.
As diferentes duplas podem sempre discutir os problemas e as ideias de como resolvê-los (e isso é recomendado, pois é uma ótima forma de estudar e aprender!), porém: soluções de exercícios não devem ser compartilhadas entre diferentes duplas (nem de outros períodos). O recomendável é que você não mostre suas soluções completas para alunos de outras duplas, nem veja as soluções completas de outros.
Soluções iguais ou parecidas demais entre duplas diferentes serão desconsideradas.
Cronograma planejado/registro de atividades
| Data | Aula | Conteúdo | Material |
|---|---|---|---|
| qua 19/mar | 00 | Introdução e burocracias | Vídeo; Quadros |
| sex 21/mar | sem aula | Professor doente | - |
| qua 26/mar | 01 | Recursão e Indução: definições e exemplos | Vídeo; Quadros; Código |
| sex 28/mar | 02 | Recursão e Indução: legibilidade única; Lógica Proposicional (LC): sintaxe | Vídeo; Quadros |
| qua 2/abr | sem aula | Semana da Computação | - |
| sex 4/abr | sem aula | Semana da Computação | - |
| qua 9/abr | 03 | Sintaxe de LC (exemplos de definições, provas e código usando recursão); Semântica da LC (contextos, definição de valor-verdade) | Vídeo; Quadros; Código |
| sex 11/abr | 04 | Semântica da LC: classificação de fórmulas em tautologias, contradições, satisfazíveis, insatisfazíveis, contingências; teorema da concordância | Vídeo; Quadros |
| qua 16/abr | 05 | Consequência/Equivalência Semântica; conjuntos completos de conectivos | Vídeo; Quadros |
| sex 18/abr | sem aula | Feriado (Sexta-feira Santa) | - |
| qua 23/abr | sem aula | Feriado (São Jorge) | - |
| sex 25/abr | 06 | Formas normais | Vídeo; Quadros |
| qua 30/abr | 07 | Satisfabilidade, validade, etc, de conjuntos de fórmulas; Árvores de Avaliação (ideia e começo da definição) | Vídeo; Quadros |
| sex 2/mai | sem aula | Recesso (Trabalhador) | - |
| qua 7/mai | 08 | Árvores de avaliação (definição completa e exemplos) | Vídeo; Quadros |
| sex 9/mai | 09 | Mais exemplo de árvore de avaliação; enunciado de corretude e completude; início da prova de corretude | Vídeo; Quadros |
| qua 14/mai | 10 | Teorema da Corretude das árvores de avaliação para LC | Vídeo; Quadros |
| sex 16/mai | 11 | Lógica de Primeira Ordem: introdução e sintaxe (início) | Vídeo; Quadros |
| qua 21/mai | 12 | Sintaxe da lógica de primeira ordem: fórmulas, ocorrências de variáveis livres e ligadas | Vídeo; Quadros |
| sex 23/mai | 13 | Ocorrências livres e ligadas de variáveis; notação De Bruijn; substituição | Vídeo; Quadros |
| qua 28/mai | 14 | Aula de dúvidas para a Prova 1 | Vídeo; Quadros |
| sex 30/mai | P1 | Prova 1 | |
| qua 4/jun | 15 | Substituição; Semântica da LPO: estruturas; Comentários sobre a P1 | Vídeo; Quadros |
| sex 6/jun | 16 | Semântica da LPO: termos, fórmulas; fórmulas válidas | Vídeo; Quadros |
| qua 11/jun | 17 | Consequência semântica em LPO; definibilidade | Vídeo; Quadros |
| sex 13/jun | 18 | Definibilidade de operações e relações em LPO; árvores de avaliação para LPO | Vídeo; Quadros |
| qua 18/jun | 19 | Definição completa e mais exemplos de árvores de avaliação para LPO | Vídeo; Quadros |
| sex 20/jun | sem aula | Recesso (Corpus Christi) | - |
| qua 25/jun | 20 | Máquinas de Turing: definição e primeiros exemplos | Vídeo; Quadros; Programa em Python para simular MTs |
| sex 27/jun | 21 | Mais sobre máquinas de Turing; as classes de linguagens R.E. e DEC; as linguagens Aceita, Diagonal, Parada; Prova de que Aceita e Parada são R.E. mas Diagonal não é | Vídeo; Quadros |
| qua 2/jul | 22 | Aula de dúvidas para a P2 | Vídeo; Quadros |
| sex 4/jul | P2 | Prova 2 | |
| qua 9/jul | 23 | Parada, Aceita e LPO são indecidíveis | Vídeo; Quadros |
| sex 11/jul | 24 | Revisão para a P3 | Vídeo; Quadros |
| qua 16/jul | P3 | Prova 3 | |
| sex 18/jul | PSc | Provas de Segunda Chamada: P2, P3 |
Método de avaliação
Teremos ?? listas de exercícios e 3 provas.
Descartaremos a pior nota dentre as listas de exercícios, e ML será a média aritmética das restantes.
Também descartaremos a pior nota dentre as provas, e MP será a média aritmética das restantes.
A média final é:
- MP, se MP \(<\) 5;
- a média ponderada entre ML e MP, sendo ML com peso 1 e MP com peso 2, caso contrário.
A nota para aprovação é 5,0; não há prova final.