- Professor: Hugo Nobrega
- Grupo de discussões: Discord
- Monitores: Matheus Gorchinsky e Bruna Falheiro
- Local das aulas: Sala F2-007
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-007 do CCMN.
Bibliografia
- 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é
Listas de Exercícios
| Lista | Data Limite de Entrega |
|---|---|
| Lista 1 | 20 de setembro às 23:59 |
| Lista 2 | 11 de outubro às 23:59 |
| Lista 3 | 12 de dezembro às 23:59 |
| Lista Extra (modificada em 19/12!) | 23 de dezembro às 23:59 |
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 | Quadros |
|---|---|---|---|
| sex 11/8 | 1 | Introdução à disciplina, assuntos burocráticos | slides sobre um pouco da história da teoria da computação 1 e 2 |
| qua 16/8 | - | sem aula | - |
| sex 18/8 | - | sem aula | - |
| qua 23/8 | 2 | Recursão: discussão e exemplos | 3 a 18 |
| sex 25/8 | 3 | Recursão e indução: discussão e exemplos (“indução é prova feita pelo método de recursão”) | 19 a 42 |
| qua 30/8 | 4 | Recursão e indução: mais discussão e exemplos (“indução como preservação”) | 43 a 55 |
| sex 1/9 | 5 | Lógica (discussão sobre o que é e para que serve); Lógica Proposicional (LC): sintaxe | 56 a 72 |
| qua 6/9 | 6 | Semântica da Lógica Proposicional (definição e Teorema da Concordância) | 73 a 86 |
| sex 8/9 | - | sem aula | - |
| qua 13/9 | 7 | Classificação de fórmulas: válidas, contraditórias (ou insatisfazíveis, ou absurdas), contingentes, satisfazíveis, falsificáveis; Decidibilidade da LC | 87 a 97 |
| sex 15/9 | 8 | Dúvidas da Lista 1; Consequência e equivalência semântica; tabelas-verdade e seus defeitos | 98 a 113 |
| qua 20/9 | 9 | Método de dedução: árvores de avaliação (ideia) | 114 a 129 |
| sex 22/9 | 10 | Definição formal das árvores de avaliação | 130 a 150 |
| qua 27/9 | 11 | Enunciado dos teoremas de completude e corretude para a LC; ideia da prova de corretude | 151 a 168 |
| sex 29/9 | 12 | Prova de corretude | 169 a 184 |
| qua 4/10 | 13 | Lógica de Primeira Ordem (LPO): assinaturas, termos, fórmulas | 185 a 196 |
| sex 6/10 | 14 | Fórmulas da LPO; ocorrências livres e ligadas de variáveis; escopo; notação de de Bruijn; conversão α | 197 a 212 |
| qua 11/10 | 15 | ? | |
| sex 13/10 | - | sem aula | |
| qua 18/10 | 16 | Aula de revisão para Prova 1 | slides |
| sex 20/10 | 17 | Semântica da LPO: estruturas, interpretações, significados de termos e fórmulas | slides |
| qua 25/10 | 18 | Semântica da LPO: exemplos, definição de validade, satisfabilidade, etc | slides |
| sex 27/10 | 19 | Prova de que “∀x φ ⊧ φ[t/x]” para qualquer termo. | vídeo 1; vídeo 2; slides |
| qua 1/11 | 20 | Extensão de assinaturas e estruturas com novas constantes; Árvores de avaliação para LPO | vídeo; slides |
| sex 3/11 | - | sem aula | |
| qua 8/11 | 21 | Árvores de avaliação para LPO (regras “relaxadas”) | vídeo; slides |
| sex 10/11 | - | PROVA 1 | |
| qua 15/11 | - | sem aula | |
| sex 17/11 | 22 | Discussões sobre a prova e reorganização da disciplina | slides (sem vídeo) |
| qua 22/11 | 23 | A ideia da prova da indecidibilidade da LPO; modelos de computação; paradoxos; diagonalização de Cantor; redução entre problemas; problema da parada | vídeo; slides |
| sex 24/11 | 24 | Máquinas de Turing: definição semi-formal e primeiros exemplos | vídeo; slides |
| qua 29/11 | 25 | Máquinas de Turing: definição formal; representação diagramática; poder de MTs: memória, várias trilhas, várias fitas, não-determinismo (tudo equivalente) | vídeo; slides |
| sex 1/12 | 26 | Máquinas de Turing: linguagens RE, coRE, DEC; Códigos; Linguagem “Diag” não é RE; Linguagem “Parada” não é DEC | vídeo; slides |
| qua 6/12 | - | sem aula (falta de água) | |
| sex 8/12 | 27 | Revisão para a Prova 2 | vídeo; slides; código |
| assíncrona | 28 | Indecidibilidade de PARADA, ACEITA e LPO | vídeo; slides |
| qua 13/12 | - | Prova 2 | |
| sex 15/12 | - | sem aula | |
| qua 20/12 | - | Prova de Segunda Chamada | |
| sex 22/12 | - | sem aula |
Método de avaliação
Teremos ~4 listas de exercícios e 2 provas.
Descartaremos a pior nota dentre as listas de exercícios, e ML será a média aritmética das restantes.
MP será a média aritmética das notas das provas.
A média final é a média ponderada entre ML e MP, sendo ML com peso 1 e MP com peso 2.
A nota para aprovação é 5,0; não há prova final.