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

De Wiki DAINF
(Diferença entre revisões)
(→Descrição das Atividades)
(→Novos rumos)
 
(23 edições intermediárias de um usuário não apresentadas)
Linha 1: Linha 1:
−
== Informações ==
+
= Informações =
  
 
* Projeto de Iniciação Científica
 
* 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
 
* 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 Shigeo Sugimoto]].
+
* Estudante (bolsista IC UTFPR): [[Emerson Shigueo Sugimoto]].
 
* Orientador: Professor [[Adolfo Neto]].
 
* Orientador: Professor [[Adolfo Neto]].
 
* Período: 08/2009 a 07/2010.
 
* Período: 08/2009 a 07/2010.
 +
* Grupo de Pesquisa: [[Grupo de Pesquisa em Inteligência Computacional]]
  
 +
= Gerenciamento de Tarefas =
  
−
== Descrição das Atividades ==
+
== Tarefas em Andamento ==
  
−
# Levantamento bibliográfico sobre implementações de provadores de teoremas para a lógica C1
+
# 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
 +
# 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
 +
# [[Testes do KEMS em Lote]]
 +
#** Início: 11/11/2009
 +
#** Término prvisto: 22/11/2009
 +
 
 +
== Tarefas temporariamente suspensas ==
 +
 
 +
# Página Wiki sobre [[A lógica C1 | a lógica C1]].
 +
#* Início: 09/09/2009
 +
#* Término previsto: 26/09/2009
 +
# 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 ==
 +
 
 +
# 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 =
 +
 
 +
# Levantamento bibliográfico sobre implementações de provadores de teoremas para [[A lógica C1| a lógica C1]]
 
#* Leituras sobre padrões de projeto utilizados no KEMS
 
#* Leituras sobre padrões de projeto utilizados no KEMS
 
#*# Padrão Strategy
 
#*# 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://serpeerless.wordpress.com/category/design-patterns/
 
#*#* http://www.dsc.ufcg.edu.br/~jacques/cursos/1998.2/lp4/material/patterns/pat4.htm
 
#*#* http://www.dsc.ufcg.edu.br/~jacques/cursos/1998.2/lp4/material/patterns/pat4.htm
Linha 25: Linha 84:
 
# Escrita do Relatório Final
 
# Escrita do Relatório Final
  
−
== Cronograma de Atividades ==
+
= Cronograma de Atividades (Inicial) =
  
 
* Período: Mês 1 ao mês 12.
 
* Período: Mês 1 ao mês 12.

Edição atual tal como 16h21min de 14 de dezembro de 2009

Tabela de conteúdo

Informações

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).

Descrição das Atividades

  1. Levantamento bibliográfico sobre implementações de provadores de teoremas para a lógica C1
  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
Obtida de "http://dainf.ct.utfpr.edu.br/wiki/index.php?title=Implementa%C3%A7%C3%A3o_de_uma_Estrat%C3%A9gia_Eficiente_para_a_L%C3%B3gica_C1_em_um_Provador_de_Teoremas_Multi-Estrat%C3%A9gia&oldid=2680"
Ferramentas pessoais