Titulo Estágio
Implementação do Método das Bases de Dados Deductivas para a Geometria
Áreas de especialidade
Sistemas Inteligentes
Local do Estágio
Departamento de Matemática, FCTUC
Enquadramento
Nenhum dos actuais demonstradores de teoremas de geometria possui capacidades de auto-aprendizagem. O poder do demonstrador de resolver problemas não pode ser aprimorado através de treinamento. Se um tal demonstrador de teorema da geometria com capacidade de auto-aprendizagem poderá ser especificado e implementado continua sendo um importante assunto para investigação.
De facto, o demonstrador armazena teoremas de geometria demonstrador por si próprio na sua base de dados para uso futuro, o que pode ser entendido como uma espécie de aprendizagem automática em si mesmo. Se o demonstrador pudesse ser configurado para selecionar os teoremas a serem armazenados permanentemente e recusar os teoremas que provavelmente serão inúteis, então a aprendizagem automática daria um contributo importante para a melhoria do demonstrador automático de teoremas. Esta aproximação tem duas dificuldades fundamentais: uma é como determinar os teoremas que precisavam ser armazenados permanentemente e a outra é como decidir se o teorema a ser provado já está na base de dados do demonstrador ou não. Se o demonstrador adquirir essa capacidade de aprendizagem, a sua capacidade de resolução de problemas tornar-se-ia muito mais forte, com mais e mais teoremas de geometria a serem armazenados. No fim do percurso obter-se-ia o geómetra inteligente [Kuh04,Bri10,BHP14].
[BHP14] James P Bridge, Sean B Holden, and Lawrence C Paulson. Machine learning for first-order theorem proving. Journal of automated reasoning, 53(2):141–172, 2014.
[Bri10] James P. Bridge. Machine learning and automated theorem proving. techreport UCAM-CL-TR-792, University of Cambridge, Computer Laboratory, 15 JJ Thomson AvenueCambridge CB3 0FDUnited Kingdom, November 2010.
[Kuh04] Daniel Kühlwein. Machine Learning for Automated Reasoning. PhD thesis, Radboud University, Netherlands, 2004.
Objetivo
O objectivo acima descrito é um projeto muito ambicioso.
Para um começo mais humilde, porém importante, pretende-se implementar, no OpenGeoProver (https://github.com/opengeometryprover/OpenGeometryProver) [PKW+12], o Método de Bases de Dados Dedutivas (em Inglês, Geometry Deductive Databases Method, GDDM) [CGZ00,GMN84,RH94,Gao99].
[CGZ00] Shang-Ching Chou, Xiao-Shan Gao, and Jing-Zhong Zhang. A deductive database approach to automated geometry theorem proving and discovering. Journal of Automated Reasoning, 25:219–246, 2000.
[Gao99] X. S. Gao. Building dynamic mathematical models with Geometry Expert, III. a geometry deductive database. In Proc. Of ATCM’99, pages 153–162. ATCM Inc., USA, 1999.
[GMN84] Herve Gallaire, Jack Minker, and Jean-Marie Nicolas. Logic and databases: A deductive approach. ACM Comput. Surv., 16:153–185, June 1984.
[PKW+12] Ivan Petrović, Zoltán Kovács, Simon Weitzhofer, Markus Hohenwarter, and Predrag Janičić. Extending GeoGebra with automated theorem proving by using OpenGeoProver. In proceedings CADGME 2012, Novi Sad, Serbia, 2012.
[RH94]Kotagiri Ramamohanarao and James Harland. An introduction to deductive database languages and systems. VLDB Journal, 3:107–122, 1994.
Plano de Trabalhos - Semestre 1
Estudo do artigo: Shang-Ching Chou, Xiao-Shan Gao and Jing-Zhong Zhang, A Deductive Database Approach to Automated Geometry Theorem Proving and Discovering}, aonde é apresentada uma abordagem ao GDDM.
Implementação em Java (início), no OpenGeoProver, do método GDDM.
Plano de Trabalhos - Semestre 2
Implementação em Java (finalizar), no OpenGeoProver, do método GDDM.
Encontrar heurísticas e/ou aplicar técnicas de aprendizagem automática para melhorar a eficiência do GDDM. Isto é, de forma a evitar a explosão combinatorial no espaço das provas, descobrir como podar a árvore de demonstração de maneira a que se possam evitar ramificações desnecessárias.
Condições
Está disponível um bolsa para estudantes de mestrado (FCT/BI). Duração da bolsa: 8 meses; Bolsa FCT-BI: 798€/mês + Seguro Social Voluntário (SSV) 130€/mês.
O desenvolvimento será feito em ambientes Linux e na linguagem Java. O aluno terá acesso aos meio computacionais do Departamento de Matemática da FCTUC, acesso remoto a um servidor Linux (Debian) e, se necessário a um portátil em Linux (Debian).
O aluno poderá trabalhar em um qualquer outro ambiente computacional, sendo que a implementação final terá de ser em ambiente Linux.
Orientador
Pedro Henrique e Figueiredo Quaresma de Almeida
pedro@mat.uc.pt 📩