Implementação de uma Estratégia Eficiente para a Lógica C1 em um Provador de Teoremas Multi-Estratégia

Informações

• Projeto de Iniciação Científica
• Título: Implementação de uma Estratégia Eficiente para a Lógica C1 em um Provador de Teoremas Multi-Estratégia
• Estudante (bolsista IC UTFPR): Emerson Shigueo Sugimoto.
• Orientador: Professor Adolfo Neto.
• Período: 08/2009 a 07/2010.
• Grupo de Pesquisa: Grupo de Pesquisa em Inteligência Computacional

Gerenciamento de Tarefas

Tarefas em Andamento

1. Demonstração da instância 3 da família 5 usando os dois sistemas KE para C1
   • Início: 14/09/2009
   • Término previsto: 16/09/2009
2. Demonstração de várias instâncias de várias das famílias de problemas para LFIs com o objetivo de descobrir:
   • Qual é a família mais difícil para a C1SimpleStrategy?
   • Que regras podemos adicionar o sistema para tornar o processo de demonstração mais eficiente?
     • Início: 15/09/2009
     • Término previsto: 22/09/2009
3. Testes do KEMS em Lote
   • • Início: 11/11/2009
     • Término prvisto: 22/11/2009

Tarefas temporariamente suspensas

1. Página Wiki sobre a lógica C1.
   • Início: 09/09/2009
   • Término previsto: 26/09/2009
2. Leituras sobre padrões de projeto
   • Elaboração de resumo sobre os padrões de projeto utilizados no KEMS
     • Início: 01/09/2009
     • Término previsto: 28/09/2009

Backlog

1. Pensar em como receber como entrada um sequente contendo fórmulas como @A (A é consistente) e, sem traduzir para !A&!A, demonstrar o sequente em C1.
   • Talvez seja necessário traduzir toda ocorrência de !A&!A para @A
   • Justificativa: usando @A os sequentes ficam menores:
     • tamanho(@A)=2 -- tamanho(!(A&!A))=5
     • tamanho(@@A)=3 -- tamanho(!(@A&!@A))=2*5+3
     • tamanho(@...@A)=n+1 (onde "@...@"=n vezes @) -- tamanho(!(@..@A&!@...@A))=?
     • ou seja
     • tam(o_co(n))=n+1 -- tam(c1_co(n))=2*tam(c1_co(n-1))+3=O(<math>2^n</math>)

Novos rumos

• Como desenhar melhor a árvore de prova?
  • Que ordem seguir ao desenhar? (atualmente faz busca em profundidade)
  • Registrar em alguma estrutura de dados em que posição estão as strings?

• Ideia: percorrer toda a árvore de prova antes de desenhar para calcular a largura de cada sub-árvore. Usar as font metrics para calcular os tamanhos das strings. Só depois definir o tamanho da janela e desenhar a árvore. Utilizar melhor o espaço (ramos esquerdo e direito não precisam ter a mesma largura - atualmente eles têm).

• Dar uma olhada em:
  • http://www.graphviz.org/Gallery.php
  • Pesquisar "draw tree algorithm" (sem aspas) no http://scholar.google.com
  • http://www2.research.att.com/~john/Grappa/ (A Java Graph Package)
  • http://www.informatik.uni-koeln.de/ls_juenger/teaching/ss_09/gd/TidierDrawingsofTrees.pdf (já impresso)
  • http://www.cs.brown.edu/~rt/papers/gdbiblio.pdf (parcialmente impresso - até p.7)

Descrição das Atividades

1. Levantamento bibliográfico sobre implementações de provadores de teoremas para a lógica C1
   • Leituras sobre padrões de projeto utilizados no KEMS
     1. Padrão Strategy
        • Livros disponíveis na Biblioteca:
          • GAMMA, Erich; JOHNSON, Ralph, 1948-; HELM, Richard; VLISSIDES, John. Padrões de projeto: soluções reutilizáveis de software orientado a objetos . Porto Alegre: Bookman, 2002 364 p.
          • METSKER, Steven John. Padrões de projeto em Java. Porto Alegre: Bookman, 2004. 407 p.
          • LARMAN, Craig. Utilizando UML e padrões: uma introdução à análise e ao projeto orientados a objetos e ao desenvolvimento iterativo. 3. ed. Porto Alegre: Bookman, 2007. 695 p.
          • SHALLOWAY, Alan. Explicando padrões de projeto: uma nova perspectiva em projeto orientado a objeto. Porto Alegre: Bookman, 2004. 328 p.
        • http://serpeerless.wordpress.com/category/design-patterns/
        • http://www.dsc.ufcg.edu.br/~jacques/cursos/1998.2/lp4/material/patterns/pat4.htm
        • http://www.lcg.ufrj.br/Cursos/designpatterns/structural.html
        • http://en.wikipedia.org/wiki/Strategy_pattern
        • http://today.java.net/pub/a/today/2005/04/07/pojostrategy.html
        • http://www.c2.com/cgi/wiki?StrategyPattern
2. Estudo detalhado do sistema KEMS
3. Especificação e Projeto da Estratégia
4. Implementação da Estratégia
5. Testes
6. Escrita do Relatório Final

Cronograma de Atividades (Inicial)

• Período: Mês 1 ao mês 12.

ATIVIDADE	Mês
	1	2	3	4	5	6	7	8	9	10	11	12
1	X	X
2		X	X
3			X	X
4				X	X	X	X	X	X	X
5				X	X	X	X	X	X	X
6											X	X