Lógica Computacional

Licenciatura em Ciências da Computação - 2º ano

Tópicos

Avisos

22/07/2009: Disponíveis notas da época de recurso.

07/05/2009: Disponível enunciado do projecto prático.

06/03/2009: Já disponível o guião da primeira aula prática (aqui).

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.


r16 - 11 Jun 2007 - 19:45:02 - JoseBacelarAlmeida
This site is powered by the TWiki collaboration platform Copyright © by the contributing authors. Ideas, requests, problems? Send feedback.
Syndicate this site RSSATOM