Sumários
Docente: José Carlos Bacelar
Aulas Teóricas
08/06: Esclarecimento de dúvidas.
05/06: Referência às propriedades básicas do Lambda-calculus com tipos:
subject-reduction,
Church-Rosser, normalização forte.
01/06: Lambda-calculus com tipos. Analogia de Curry-Howard.
29/05: Identidade das provas e processo de normalização. Sistemas de anotação de termos.
25/05: Motor de inferência do PROLOG: selecção das cláusulas; unificação;
backtracking; árvores de inferência.
22/05: Resolução em cláusulas de primeira ordem. Cláusulas de Horn. Resolução SLD e inferência do PROLOG.
18/05: Tolerância de ponto:
enterro da gata.
15/05: Tolerância de ponto:
enterro da gata.
11/05: JOIN'2007
08/05: Resolução proposicional em fórmulas de primeira ordem. Unificação.
04/05: Correcção das regras no cálculo de sequentes. Versão semântica do teorema de Herbrand.
27/04: Prenex Normal Forms e
Skolenização. Modelos de Herbrand.
24/04: Cálculo de Sequentes para Lógica de Primeira Ordem.
20/04: Sobre o problema SAT: noções de complexidade. Lógica de Primeira Ordem: sintaxe e semântica.
17/04: BDDs: redução de árvores de decisão e construção
bottom up.
13/04: Algoritmo
Davis Putnam.
30/03: Não houve aula (ETAPS 07)
27/03: Não houve aula (ETAPS 07)
23/03: Algoritmo de resolução de Robinson. Exemplos de aplicação.
20/03: Formas Normais Conjuntivas e Formas Normais Disjuntivas. Resolução de cláusulas em formulas na FNC.
16/03: Apresentação do método de
Tableaux. Formas normais negativas.
13/03: Esboço da demonstração da propriedade de
eliminação de corte no cálculo de sequentes. Resumo das propriedades
do cálculo de sequentes.
09/03: Demonstração dos teoremas de correcção e completude para o cálculo de sequentes (LC).
06/03: Apresentação do cálculo de sequentes (sistema LC)
02/03: Sintaxe e semântica da lógica proposicional. Consequência semântica e sistemas de dedução. Dedução natural.
27/02: Apresentação da disciplina.
23/02: Não houve aula (
Simpósio Doutoral).
Aulas Teórico-Práticas
05/06: Unificação em cláusulas LPO.
29/05: Cálculo de sequentes em Lógica de Primeira Ordem.
22/05: Formas
Prenex e
Skolenização.
15/05: Tolerância de ponto:
enterro da gata.
08/05: BDDs: redução e construção
bottom-up.
24/04: Algoritmo
Davis-Putman: exercícios de aplicação.
17/04: Algoritmo de resoluçao de Robinson: exemplos de aplicação.
27/03: Formas clausais: Fórmulas Normais Conjuntivas e Fórmulas Normais Disjuntivas. Resulução proposicional.
20/03: Avaliação de fórmulas proposicionais por aplicação do método
tableaux. Formas normais negativas.
13/03: Demonstrações simples envolvendo indução sobre estrutura das fórmulas e derivações em sistemas de dedução. Construção de derivações no sistema de cálculo de sequentes.
06/03: Exercícios sobre noções elementares da lógica proposicionais: validade de fórmulas; consequência semântica; derivações em Dedução Natural.
27/02: Inscrição nos turnos.
Aulas Práticas
05/06: Mini-teste 2
29/05 Predicados de segunda ordem.
22/05: Estratégia
Gerar e Testar.
15/05: Tolerância de ponto:
enterro da gata.
08/05: Utilização de operadores em
Prolog. Manipulação de fórmuas lógicas.
24/04: Utilização de
cut e negação por falha.
17/04: Mini-teste 1
27/03: Árvores de Prova. Tipos algébricos.
20/03: Continuação da manipulação de listas. Exploração do mecanismo de
backtracking.
13/03: Utilização de termos, introdução à manipulação de Listas.
06/03: Apresentação da linguagem
Prolog.
27/02: Inscrição nos turnos.
Docente: Olga Pacheco
Aulas Teórico-Práticas
17/03: Prova de que a relação de consequência semântica é uma relação de dedução.
Representação no cálculo de sequentes das regras da dedução natural.
07/03: Exercícios sobre noções elementares da lógica proposicional: validade de fórmulas; consequência semântica; derivações em Dedução Natural.
28/02: Inscrição nos turnos.
Aulas Práticas
14/03: Utlilização de termos estruturados. Representação dos naturais baseada nos construtores 0 e sucessor
(definição dos predicados: menor, maior ou igual, soma e multiplicação).
Manipulação de listas em
Prolog (definição dos predicados: cabeça, cauda, ultimo elemento, elemento na posição n, e membro).
07/03: Apresentação da linguagem
Prolog.
Representação em
Prolog de informação sobre árvores geneológicas (definição dos predicados: mãe, pai, irmão, tio, avô, avó, avô paterno, avó paterna, bisavô, bisavó,...).
28/02: Inscrição nos turnos.