DEMONSTRAçãO AUTOMáTICA DE TEOREMAS
Esta unidade curricular não está em oferta no ano letivo 2019-2020

Código: 22014
ECTS: 5
Departamento: Departamento de Ciências e Tecnologia
Área Científica: Tecnologias de Informação e Comunicação
Palavras-Chave:
    1. lógica de 1ª ordem
    2. demonstração de teoremas
    3. sistemas de demonstração automática
Docente:
Vitor Rocio
Área Científica: Informática; Engenharia Informática.
Correio Eletrónico: vjr@uab.pt

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


Competências:
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.


Conteúdos:
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.


Bibliografia:
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.


Metodologias de Ensino:
E-learning (completamente online).


Total de Horas de Trabalho: 130
Total de Horas de Contacto: 20

Avaliação:
A avaliação tem carácter 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.