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.