Provadores algebricos de teoremas e sua complexidade.

• Processo: 01/01502-2
• Modalidade de apoio: Bolsas no Brasil - Iniciação Científica
• Data de Início da vigência: 01 de maio de 2001
• Data de Término da vigência: 30 de abril de 2002
• Área de conhecimento: Ciências Exatas e da Terra - Ciência da Computação - Teoria da Computação
• Pesquisador responsável: Walter Alexandre Carnielli
• Beneficiário: Cleber Valgas Gomes Mira
• Instituição Sede: Instituto de Filosofia e Ciências Humanas (IFCH). Universidade Estadual de Campinas (UNICAMP). Campinas , SP, Brasil
• Palavra(s)-Chave do Pesquisador: Metodo Dialogico | Principio Da Casa De Pombos | Sistemas Algebricos De Prova

Resumo

Esse projeto de pesquisa tem por objetivo a investigação das principais propriedades dos métodos de provas tradicionais, tais como correção, complexidade e instâncias de resolução ineficiente; relacionando-os às propriedades de sistemas algébricos de prova. Os métodos de prova a serem estudados incluem o método de tableaux semânticos, método de resolução, sistemas de Hilbert, método dialógico e principalmente o método algébrico. A complexidade dos métodos de prova será investigada tomando-se como instância adequada do problema qualquer fórmula que descreva o Princípio da Casa de Pombos. O que se pretende, mais do que estudar questões de complexidade computacional em todo seu detalhamento técnico, é iniciar a investigação acerca das diferentes formulações de provadores de teoremas e a influência que tais formulações podem exercer, tanto no que concerne aos aspectos de mensuração de complexidade quanto ao significado filosófico de tais formulações para a aplicação em diversas áreas. (AU)