Tableaux analíticos para os sistemas proposicionais paraconsistentes Cn de da costa 1 <= n <= w

• Processo: 01/10791-8
• Modalidade de apoio: Bolsas no Brasil - Iniciação Científica
• Data de Início da vigência: 01 de dezembro de 2001
• Data de Término da vigência: 30 de novembro de 2002
• Área de conhecimento: Ciências Humanas - Filosofia - Lógica
• Pesquisador responsável: Itala Maria Loffredo D'Ottaviano
• Beneficiário: Gilberto Z. Pastorello
• Instituição Sede: Instituto de Filosofia e Ciências Humanas (IFCH). Universidade Estadual de Campinas (UNICAMP). Campinas , SP, Brasil
• Assunto(s): Cálculo proposicional Método dos Tableaux
• Palavra(s)-Chave do Pesquisador: Tableaux Analiticos | Tableaux Semanticos

Resumo

Este Projeto de Pesquisa tem como objetivo o estudo da hierarquia de cálculos proposicionais paraconsistentes de da Costa Cn, de predicados Cn* e de predicados com igualdade Cn=, 1 n (ver [1] e [2]), a análise de quatro sistemas de tableaux, que constituem métodos de decisão para essas hierarquias: o de Marconi (ver [5]) para o sistema C1, com possibilidade de adaptação para os Cn; os sistemas TC1 e TC1=, propostos por Carnielli e Lima-Marques (ver [6]) para a decidibilidade de extensões de C1 e C1=, respectivamente; um método de prova automático para C1*, através dos sistemas SC1* e S'C1* criados por Buchsbaum e Pequeno (ver [7]); e também os sistemas TNDCn, 1 n , que estão sendo introduzidos por D'Ottaviano e Castro (ver [8]) para a decidibilidade da hierarquia Cn, 1 n , de cálculos proposicionais de da Costa. Pretende-se ainda avaliar as possíveis inter-relações entre os sistemas de decisão citados. Pretendemos também implementar um software para a verificação automática dos teoremas de Cn, utilizando os sistemas TNDCn, 1 n , de D'Ottaviano e Castro. (AU)