Lógica Computacional

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

Tópicos

Avisos

24/09: Já estão disponíveis as notas da época de especial.

28/07: Já estão disponíveis as notas da época de recurso.

02/07: Já estão disponíveis as notas do 2º teste.

23/06: Sala do 2º teste: CP2-201 (hora: 14:00).

11/05: Já estão disponíveis as notas do 1º teste.

08/05: Estão disponíveis propostas para os projectos práticos em Projectos0708.

17/04: A data do teste intermédio passou para o dia 23/04 (4a-feira), às 14:00 (sala CP2-204CP2-104) .

08/04: A aula teórico-prática do turno 1 (3a, 10:00-11:00) passa para o lab. DI 1.04.

13/03: Já foram disponibilizadas as datas dos testes intermédios (site LCC). Os testes de Lógica Computacional são nos dias 23/04 22/04 e 27/06.

13/03: Foi marcada uma aula suplementar de Lógica Computacional para o dia 27/03 às 15:00 (em substituição da aula de PLC).

22/02: As aulas da disciplina de Lógica Computacional terão início somente no dia 06/03 (5a-feira).


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

  • 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 e Lambda-Calculus com tipos (formulação de Curry)

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

r1 - 20 Feb 2008 - 15:22:48 - JoseBacelarAlmeida
This site is powered by the TWiki collaboration platform Copyright © by the contributing authors. Ideas, requests, problems? Send feedback.
Syndicate this site RSSATOM