- Professor: Hugo Nobrega
- Turma: 12939
- Grupo de discussões: Discord
- Monitores: a definir
- Local das aulas: F2-006
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-006 do CCMN.
Bibliografia
- Notas de aula de 25-2
- Notas de aula de turmas anteriores dessa disciplina: 24-1 24-2
- 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 setembro às 20:00 |
| Lista 2 | |
| Lista 3 | 8 de dezembro à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 6 ago | 01 | Informações burocráticas sobre o funcionamento da disciplina; discussão “filosófica” sobre formalização; a origem da teoria da computabilidade a partir de problemas da lógica | Vídeo; Quadros |
| sex 8 ago | 02 | Recursão: análise de quando “funciona”, em visões “top-down” (expansão e contração) e “bottom-up” (agendamento) | Vídeo; Quadros |
| qua 13 ago | 03 | Mais exemplos de recursão com e sem legibilidade única; Indução | Vídeo; Quadros |
| sex 15 ago | 04 | Mais exemplos de indução: árvores estritamente binárias têm quantidade ímpar de vértices; todo grafo planar é 6-colorível; todo grafo planar é 5 colorível | Vídeo; Quadros |
| qua 20 ago | 05 | Sintaxe da LC; ocorrências, substituições | Vídeo; Quadros |
| sex 22 ago | 06 | Implementação de coisas sintáticas em python; Semântica da LC: “contextos” e valor-verdade de uma fórmula em um contexto | Vídeo; Quadros |
| qua 27 ago | 07 | Semântica da LC: tautologias, contradições, contingências, satisfazíveis e falsificáveis; Teorema da Concordância; tabelas-verdade | Vídeo; Quadros |
| sex 29 ago | 08 | Semântica da LC: consequência semântica, equivalência semântica; conjuntos completos de conectivos (início) | Vídeo; Quadros |
| qua 3 set | 09 | (In-)completude de conectivos; formas normais | Vídeo (sem áudio); Quadros |
| sex 5 set | 10 | Forma Normal Conjuntiva; Árvores de Avaliação/Tableaux (ideia) | Vídeo (sem áudio); Quadros |
| qua 10 set | 11 | Árvores de Avaliação para Lógica Proposicional: definição e exemplos; Consequência Sintática; Enunciado dos Teoremas de Corretude e Completude | Vídeo; Quadros |
| sex 12 set | 12 | Mais exemplos de uso de árvores de avaliação; Corretude | Vídeo; Quadros |
| qua 17 set | 13 | Discussão sobre corretude e completude; introdução à Lógica de Primeira Ordem | Vídeo; Quadros |
| sex 19 set | 14 | Fim da discussão sobre corretude/completude; sintaxe da LPO (assinaturas, termos, fórmulas) | Vídeo; Quadros |
| qua 24 set | sem aula | Semana de Integração Acadêmica - SIAc | |
| sex 26 set | sem aula | Semana de Integração Acadêmica - SIAc | |
| qua 1 out | 15 | Aula de revisão para a P1 | Vídeo; Quadros |
| sex 3 out | P1 | PROVA 1 | |
| qua 8 out | 16 | Sintaxe da LPO: notação De Bruijn, variáveis livres/ligadas, substituição | Vídeo; Quadros |
| sex 10 out | 17 | Substituição em LPO; semântica da LPO: estruturas, atribuições; significados de termos | Vídeo; Quadros |
| qua 15 out | 18 | Semântica da LPO: valor de fórmula em estrutura e atribuição; fórmulas válidas em estruturas; fórmulas válidas | Vídeo; Quadros |
| sex 17 out | 19 | Semântica da LPO: consequência semântica; definibilidade em LPO (elementos, operações, relações) e exemplos | Vídeo; Quadros |
| qua 22 out | 20 | Semântica da LPO: extensões de assinaturas e estruturas; Árvores de Avaliação para LPO | Vídeo; Quadros |
| sex 24 out | 21 | Árvores de avaliação para LPO: exemplos e discussão sobre as regras “particularizantes” ∃:V e ∀:F; Regras para igualdade | Vídeo; Quadros |
| qua 29 out | sem aula | Aula cancelada por problemas de segurança pública | |
| sex 31 out | 22 | Dúvidas da Lista 2; Máquinas de Turing: introdução e exemplos informais; definição formal (“parte estática”) | Vídeo; Quadros; Código (simulador de MTs) |
| qua 5 nov | 23 | MTs: completando definição (configurações, execuções) e mais exemplos | Vídeo; Quadros |
| sex 7 nov | 24 | MTs: mais exemplo (linguagem 0^n1^n2^n); robustez do modelo | Vídeo; Quadros |
| qua 12 nov | 25 | Aula de revisão para a P2 | Vídeo (áudio ruim); Quadros |
| sex 14 nov | P2 | PROVA 2 | |
| qua 19 nov | 26 | Discussão da P2; definição de classes RE (recursivamente enumeráveis) e Decidíveis; codificação de MTs; MT universal | Vídeo; Quadros |
| sex 21 nov | sem aula | Recesso | |
| qua 27 nov | 27 | “Diag” não é RE; Reduzibilidade entre linguagens; “Aceita” e “Parada” são RE mas não Decidíveis | Vídeo; Quadros |
| sex 28 nov | 28 | LPO é recursivamente enumerável mas não decidível | Vídeo; Quadros |
| qua 3 dez | sem aula | ||
| sex 5 dez | sem aula | ||
| qua 10 dez | 29 | Aula de revisão para a P3 | Vídeo; Quadros |
| sex 12 dez | P3 | PROVA 3 | |
| qua 17 dez | Provas | Provas de Segunda Chamada: P1, P2 | |
| sex 19 dez | |||
Método de avaliação
Teremos 3 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.
A média das provas, MP, será a média ponderada das notas das 3 provas, sendo a maior nota com peso 3, a segunda maior com peso 2, e a menor com peso 1.
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.