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)
(→Cronograma de Atividades) |
(→Novos rumos) |
||
(32 edições intermediárias de um usuário não apresentadas) | |||
Linha 1: | Linha 1: | ||
+ | = Informações = | ||
+ | |||
* Projeto de Iniciação Científica | * Projeto de Iniciação Científica | ||
− | * Estudante (bolsista IC UTFPR): [[Emerson | + | * 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]]. | * 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 = | ||
− | == | + | == 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 | ||
+ | #*# 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 | ||
# Estudo detalhado do sistema KEMS | # Estudo detalhado do sistema KEMS | ||
# Especificação e Projeto da Estratégia | # Especificação e Projeto da Estratégia | ||
Linha 14: | Linha 84: | ||
# Escrita do Relatório Final | # Escrita do Relatório Final | ||
− | + | = Cronograma de Atividades (Inicial) = | |
− | + | ||
* Período: Mês 1 ao mês 12. | * Período: Mês 1 ao mês 12. | ||
Linha 22: | Linha 91: | ||
{| class="prettytable" | {| class="prettytable" | ||
− | | <center> | + | | <center>ATIVIDADE</center> |
| colspan="12" | <center>Mês</center> | | colspan="12" | <center>Mês</center> | ||
|- | |- |
Edição atual tal como 16h21min de 14 de dezembro de 2009
Tabela de conteúdo |
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
- 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.
- 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
- Elaboração de resumo sobre os padrões de projeto utilizados no KEMS
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
- Leituras sobre padrões de projeto utilizados no KEMS
- 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
- Livros disponíveis na Biblioteca:
- Padrão Strategy
- Leituras sobre padrões de projeto utilizados no KEMS
- Estudo detalhado do sistema KEMS
- Especificação e Projeto da Estratégia
- Implementação da Estratégia
- Testes
- Escrita do Relatório Final
Cronograma de Atividades (Inicial)
- Período: Mês 1 ao mês 12.
|
| |||||||||||
|
|
|
|
|
|
|
|
|
|
|
| |
|
X | X | ||||||||||
|
X | X | ||||||||||
|
X | X | ||||||||||
|
X | X | X | X | X | X | X | |||||
|
X | X | X | X | X | X | X | |||||
|
X | X | ||||||||||