Raciocínio Automático

Conhecimentos de Base Recomendados

Conhecimentos de grupos obtidos num primeiro curso de Álgebra a nível de licenciatura.   

Métodos de Ensino

O processo de ensino/aprendizagem observa uma abordagem colaborativa online, em turma virtual, que se baseia na realização de trabalhos individuais e em grupo.

 

Resultados de Aprendizagem

Esta UC visa proporcionar os conhecimentos e competências fundamentais acerca dos princípios, conceitos e técnicas da área do raciocínio automático aplicado à álgebra abstracta, nomeadamente, princípios do raciocínio automático e raciocínio equacional; modelação de problemas da álgebra para o raciocínio automático; estratégias de demonstração automática de teoremas; utilização efectiva dos mais avançados demonstradores automáticos de teoremas e construtores de modelos finitos. Ao concluir esta  unidade curricular o aluno deverá ser capaz de:

-Reconhecer a importância do raciocínio automático na álgebra abstracta contemporânea, tanto nos sucessos como nas limitações.

- Identificar, classificar e integrar os princípios, modelos, algoritmos e técnicas do raciocínio automático aplicada à álgebra;

- Identificar, analisar, categorizar e avaliar o software de raciocínio automático disponível; aplica-lo a problemas na teoria de quasigrupos, semigrupos, etc.    

Estágio(s)

Não

Programa

1) Fundamentos do raciocínio automático: história e desenvolvimento da área; regras de inferência e raciocínio equacional; algoritmos e implementações; raciocínio de primeira ordem versus ordem elevada; limitações dos métodos; construção de contra exemplos finitos; áreas da álgebra onde o raciocínio automático foi aplicado com sucesso, tais como a teoria de quasigrupos e a teoria dos reticulados.

2) Quasigrupos e loops: conceitos e princípios básicos.

3) Teoria de reticulados e ordens: conceitos e princípios básicos.

4) Principais demonstradores automáticos de teoremas e construtores de contra-exemplos; modelação de problemas da álgebra para software do raciocínio automático; estratégias avançadas de demonstração automática de teoremas; modificação de demonstrações e redução de complexidade; outras referências para prosseguimento dos estudos.   

Métodos de Avaliação

Avaliação
Exame: 30.0%
Trabalho de investigação: 35.0%
Resolução de problemas: 35.0%

Bibliografia

  - “Automated Reasoning and Discovery of Missing and Elegant Proofs”, L. Wos and G. W. Pieper, Rinton Press,2003, ISBN:1-58949-023-1

- “Automated Reasoning: Introduction and Applications”, L. Wos, R. Overbeek, E. Lusk and J. Boyle,

- “Handbook of Automated Reasoning”, A. Robinson and A. Voronkov (Ed.), Elsevier, ISBN 978-0-444-50813-3, online edition: http://www.sciencedirect.com/science/book/9780444508133

- “Loop Theory”, A. Drapal, M. Kinyon and P. Vojtechovsky, manuscript.