Total de horas trabalho: 130
Total de horas de contacto: 20
Nesta unidade curricular são introduzidos os conceitos de computação simbólica e demonstração de teoremas em Álgebra, utilizando a linguagem de programação GAP e o demonstrador automático de teoremas PROVER 9.
No final do curso o aluno deverá ser capaz de resolver pequenos problemas adequados a computação simbólica e a demonstração automática de teoremas, nomeadamente, provar teoremas ou encontrar contra-exemplos usando a demonstração automática de teoremas; conhecer algumas das funções mais vulgares do GAP, bem como a sua linguagem de programação.
a. GAP e suas principais funções (listas, rotinas para extrair sublistas, aritmética, matrizes, transformações, grupóides);
b. PROVER 9
c. Fundo algébrico subjacente
- GAP Manuals: http://www.gap-system.org/Doc/manuals.html
- Prover9 Manual: http://www.cs.unm.edu/~mccune/mace4/manual-examples.html
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.
