Código: 22014
Departamento: DCET
ECTS: 5
Área científica: Tecnologias de Informação e Comunicação
Total de horas trabalho: 130
Total de horas de contacto: 20

Esta unidade curricular aborda os processos mecânicos de demonstração de teoremas, com recurso ao computador.

  1. lógica de 1ª ordem
  2. demonstração de teoremas
  3. sistemas de demonstração automática

No final da unidade curricular o aluno deverá ser capaz de:
- identificar as teorias subjacentes à automatização de demonstrações.
- aplicar sistemas automáticos de dedução a vários problemas de matemática, nomeadamente, minimização de teorias, determinação de contra-exemplos, demonstração de teoremas.

A teoria da programação em lógica é aprofundada nesta cadeira, com o objectivo de estudar processos de demonstração automática de teoremas. Alguns dos tópicos abordados serão: fórmulas e interpretações na lógica, formas normais, teorema de Herbrand, princípio de resolução, resolução semântica, resolução linear, paramodulação.

C. L. Chang, R. C. T. Lee: Symbolic Logic and Mechanical Theorem Proving, Academic Press, London, 1973.
J. A. Kalman: Automated Reasoning with OTTER, Rinton Press, Princeton, New Jersey, 2001.

E-learning (completamente online).

A avaliação tem caráter individual e implica a coexistência de duas modalidades: avaliação contínua (60%) e avaliação final (40%). Essa avaliação será desenvolvida na aplicação de formas diversificadas, definidas no Contrato de Aprendizagem da unidade curricular.