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:
Vitor Rocio
Área Científica: Informática; Engenharia Informática.
Correio Eletrónico: vitor.rocio@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.
Código: 22014
ECTS: 5
Departamento: Departamento de Ciências e Tecnologia
Área Científica: Tecnologias de Informação e Comunicação
Palavras-Chave:
- lógica de 1ª ordem
- demonstração de teoremas
- sistemas de demonstração automática
Vitor Rocio
Área Científica: Informática; Engenharia Informática.
Correio Eletrónico: vitor.rocio@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.