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.
