Lógica Computacional

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

Tópicos

Avisos

31/07 Já estão disponíveis as notas referentes à Época de Recurso. (aqui)

17/07 Já estão disponíveis as notas referentes à Época Normal. (aqui)

20/06 Foram disponibilizados exercícios teorico-práticos.

11/06 Já estão disponíveis as notas do segundo mini-teste prático e as notas práticas finais. (aqui)

05/06 Já estão disponíveis os slides correspondentes ao módulo de lógica de primeira ordem.

31/05 Já estão disponíveis (secção "Material de Apoio") os slides correspondentes ao terceiro módulo de lógica proposicional.

28/05 Já estão disponíveis as notas do primeiro mini-teste prático (aqui)

07/05 Na próxima 5ª e 6ª-feira (10 e 11/05) realizam-se as JOIN 2007. Por esse motivo não haverá aula teórica.

19/02 Na próxima 6ª-feira (26/02) não haverá aula teórica.


Programa Resumido

Componente Teórica

  • Lógica Proposicional
    • Sintaxe e Semântica
    • Sistemas Dedutivos
    • Métodos de Verificação
    • Aspectos de Complexidade (SAT)
  • Lógica de Primeira Ordem
    • Sintaxe e Semântica da Lógica de Predicados
    • Modelos de Herbrand da LPO
    • Sistemas Deductivos
    • Resolução de primeira ordem
    • Inferência em Teorias de Horn
  • Analogia de Curry-Howard
    • Identidade das provas e normalização
    • Sistemas de anotações de termos
    • Lambda-calculus com tipos
    • Analogia de Curry-Howard

Componente Teórico-Prática

  • Programação Lógica na linguagem Prolog
  • Utilização do Sistema de Prova Assistida Coq (opcional)


Programa detalhado do ano lectivo 2006/2007

  • Lógica Proposicional
    • Sintaxe e Semântica
    • Sistemas Dedutivos
      • Dedução Natural
      • Dedução Natural formulada com sequentes
      • Cálculo de Sequentes
    • Resultados de Correcção, Completude e Eliminação do Corte
    • Formas normais (negativa, disjuntiva e conjuntiva)
    • Métodos de Verificação
      • Tableaux
      • Algoritmo de Davis Putnam
      • BDDs
      • Resolução Proposicional
  • Lógica de Primeira Ordem
    • Sintaxe e Semântica
    • Modelos de Herbrand
    • Formas Prenex e Skolenização
    • Sistemas dedutivos (cálculo de sequentes)
    • Resolução proposional em lógica de Predicados
    • Unificação
    • Resolução de primeira ordem
    • Teorias de Horn
    • Resolução SLD e inferência da linguagem PROLOG
  • Analogia de Curry-Howard
    • Identidade das Provas (em Dedução Natural)
    • Normalização de provas
    • Sistemas de Anotação de Termos
    • Lambda-Calculus com tipos (formulação de Curry)
    • Beta-redução e suas propriedades
    • Analogia de Curry-Howard

  • PROLOG
    • Conceitos básicos
      • Átomos, variáveis, termos;
      • Variáveis lógicas; substituições e unificação;
      • Factos e Regras.
    • Inferência e backtracking.
    • Listas e termos estruturados.
    • Cut e negação por falha.
    • Definição de operadores em Prolog.
    • Estratégia Gerar e Testar.
    • Predicados de segunda ordem.

r3 - 04 Jul 2007 - 18:17:30 - JoseBacelarAlmeida
This site is powered by the TWiki collaboration platform Copyright © by the contributing authors. Ideas, requests, problems? Send feedback.
Syndicate this site RSSATOM