Código: 22141
ECTS: 5
Departamento: Departamento de Ciências e Tecnologia
Área Científica: Matemática
Palavras-Chave:

Automated Reasoning
Computação Simbólica
GAP

Docente:
Gilda Ferreira
Área Científica: matemática
Correio Eletrónico: Gilda.ferreira@uab.pt

Sinopse:
Nesta unidade curricular são introduzidos os conceitos de computação simbólica e demostração de teoremas, utilizando a linguagem de programação GAP.

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

Conteúdos:
1. Automated Reasoning:
               a. Enquadramento histórico e teórico da demonstração automática.
               b. Regras de inferência e lógica equacional.
               c. Principais demonstradores automáticos e construtores de contra-exemplos.
               d. Modelação de problemas para que possam ser resolvidos por demonstradores automáticos.
2. GAP
               a. As principais funções do GAP (listas, rotinas para extrair sublistas, aritmética, matrizes, transformações, grupóides);
                b. A linguagem de programação GAP.

Bibliografia:
- GAP Manuals: http://www.gap-system.org/Doc/manuals.html
 
- Prover9 Manual: http://www.cs.unm.edu/~mccune/mace4/manual-examples.html

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

Avaliação:
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.