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 2008/2009

• 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

• 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.