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)
(→Tarefas em Andamento)
(→Backlog)
Linha 44: Linha 44:
 
#** ou seja
 
#** ou seja
 
#** tam(o_co(n))=n+1 -- tam(c1_co(n))=2*tam(c1_co(n-1))+3=O(<math>2^n</math>)
 
#** 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?
 +
 +
 +
* 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)
  
 
= Descrição das Atividades =
 
= Descrição das Atividades =

Edição de 16h17min 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?


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=2678"
Ferramentas pessoais