Sumários
Aulas Teóricas (3ª 14:00-15:00; 5ª 16:00-17:00)
26/02: Não houve aula.
28/02: Não houve aula.
04/03: Aula de substituição em
27/03, às 15:00.
06/03: Revisões de Lógica Proposicional: sintaxe das fórmulas; noção de modelo e validade; tautologias e contradições; teorias; consequência semântica.
11/03: Relações de dedução. Sistema de Dedução Natural (formulação clássica e com sequentes).
13/03: Propriedades do sistema de Dedução Natural. Apresentação do Cálculo de Sequentes.
27/03 (15:00): Demonstração do teorema de Correcção e Completude do sistema de Dedução Natural.
27/03: Continuação das demonstrações de Correcção e Completude do sistema de Dedução Natural.
01/04: Esboço das demonstrações da Correcção e Completude do Cálculo de Sequentes e da propriedade de Eliminação do Corte. Apresentação do método de
Tableaux.
03/04: Formal Normal Negativa (FNN) e Formais Clausais (Forma Normal Disjuntiva (FND) e Forma Normal Conjuntiva (FNC)).
08/04: Método de
resolução proposicional. Apresentação do
algoritmo de Robinson e ilustração da aplicação.
10/04: Algoritmo de
Davis-Putnam.
15/04: BDDs: motivação e definição; redução de árvores de decisão binárias.
17/04: Construção
bottom-up de BDDs.
22/04: TESTE INTERMÉDIO.
24/04: Lógica de Primeira Ordem: Sintaxe e Semântica.
29/04: Formas Normais:
Prenex;
Herbrand e
Skolen.
06/05: Modelos de Herbrand.
08/05: Não houve aula (impossibilidade do docente).
13/05: Tolerância de Ponto: Enterro da Gata.
15/05: Tolerância de Ponto: Enterro da Gata.
20/05: Cálculo de Sequentes para Lógica de Primeira Ordem.
27/05: Resolução Proposicional em Lógica de Primeira Ordem.
29/05: Unificação.
03/06: Resolução de Primeira Ordem.
05/06: Analogia de
Curry Howard: motivação; normalização das provas.
10/06: Sistemas de Anotação de Provas para Dedução Natural. Lambda-Calculus com tipos.
12/06: Esclarecimento de dúvidas. Correcção do primeiro teste.
TP1
Aulas Teórico-Práticas (3ª 10:00-11:00)
26/02: Não houve aula.
04/03: Não houve aula.
11/03: Exercícios sobre validade e consequência semântica.
01/04: Exercícios sobre relações de dedução. Construção de árvores em
Dedução Natural.
08/04: Exercícios sobre construção de derivações no Cálculo de Sequentes.
15/04: Exercícios sobre Formas Clausais e Resolução Proposicional.
22/04: TESTE INTERMÉDIO.
29/04: Exercícios spbre método
Davis Putnam .
06/05: Exercícios sobre validade em lógica de primeira ordem.
13/05: Tolerância de Ponto: Enterro da Gata.
20/05: Exercícios sobre formas normais (prenex, skolen e herbrand)
27/05: Exercícios sobre cálculo de sequentes para lógica de predicados.
03/06: Exercícios sobre resolução.
Aulas Práticas (3ª 11:00-13:00)
26/02: Não houve aula.
04/03: Não houve aula.
11/03: Apresentação da linguagem Prolog.
01/04: Operações aritméticas e manipulação de listas.
08/04: Árvores de Inferência.
15/04: Exercícios de Manipulação de Listas e Tipos Algébricos.
22/04: TESTE INTERMÉDIO.
29/04: Utilização de
Cut e Negação por falha.
06/05: Estratégia
Gerar e Testar.
13/05: Tolerância de Ponto: Enterro da Gata.
20/05: Predicados de ordem superior.
27/05: Manipulação de Fórmulas Lógicas em Prolog.
03/06: Implementação do algoritmo de
Davis-Putnam.
TP2
Aulas Teórico-Práticas (4ª 10:00-11:00)
27/02: Não houve aula.
05/03: Não houve aula.
12/03: Exercícios sobre validade e Consequência semântica.
26/03: Exercícios sobre relações de dedução. Construção de árvores em
Dedução Natural.
02/04: Exercícios sobre construção de derivações no Cálculo de Sequentes.
09/04: Exercícios sobre o método de
Tableaux e cálculo de formas normais.
16/04: Exercícios sobre resolução proposicional.
23/04: TESTES INTERMÉDIOS.
30/04: Exercícios sobre método
Davis Putnam.
07/05: Exercícios sobre validade em lógica de primeira ordem.
14/05: Tolerância de Ponto: Enterro da Gata.
21/05: Exercícios sobre formas normais (prenex, skolen e herbrand).
28/05: Exercícios sobre cálculo de sequentes para lógica de predicados.
04/06: Exercícios sobre resolução.
11/06: Esclarecimento de Dúvidas.
Aulas Práticas (4ª 11:00-13:00)
27/02: Não houve aula.
05/03: Não houve aula.
12/03: Apresentação da linguagem PROLOG.
26/03: Operações aritméticas e manipulação de listas.
02/04: Árvores de Inferência.
09/04: Exercícios de Manipulação de Listas e Tipos Algébricos.
16/04: Utilização de
Cut e Negação por falha.
23/04: TESTES INTERMÉDIOS.
30/04: Continuação da aula anterior.
07/05: Estratégia
Gerar e Testar.
14/05: Tolerância de Ponto: Enterro da Gata.
21/05: Predicados de ordem superior.
28/05: Manipulação de Fórmulas Lógicas em Prolog.
04/06: Implementação do algoritmo de
Davis-Putnam.
11/06: Esclarecimento de dúvidas.