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)
(Backlog)
(Gerenciamento de Tarefas)
Linha 20: Linha 20:
 
#** Início: 15/09/2009
 
#** Início: 15/09/2009
 
#** Término prvisto: 22/09/2009
 
#** Término prvisto: 22/09/2009
 
 
  
 
== Tarefas temporariamente suspensas ==
 
== Tarefas temporariamente suspensas ==
Linha 32: Linha 30:
 
#** Início: 01/09/2009
 
#** Início: 01/09/2009
 
#** Término previsto: 28/09/2009
 
#** Término previsto: 28/09/2009
 
  
 
== Backlog ==
 
== 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.
 
# 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''
  
 
= Descrição das Atividades =
 
= Descrição das Atividades =

Edição de 13h29min de 15 de setembro 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 prvisto: 22/09/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

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