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.