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.