Ecumenismo Modal via RNmatrizes: Teoria, Implementação e Verificação

• Processo: 23/16021-9
• Modalidade de apoio: Bolsas no Exterior - Estágio de Pesquisa - Doutorado
• Data de Início da vigência: 20 de junho de 2024
• Data de Término da vigência: 19 de junho de 2025
• Área de conhecimento: Ciências Humanas - Filosofia - Lógica
• Pesquisador responsável: Marcelo Esteban Coniglio
• Beneficiário: Renato Reis Leme
• Supervisor: Carlos Olarte
• Instituição Sede: Instituto de Filosofia e Ciências Humanas (IFCH). Universidade Estadual de Campinas (UNICAMP). Campinas , SP, Brasil
• Instituição Anfitriã: Laboratoire D'Informatique De Paris Nord, França
• Vinculado à bolsa: 21/01025-3 - Genericidade no contexto da demonstração de teoremas: um assistente de prova baseado em nuvem para linguagens orientadas a fluxo, BP.DR
• Assunto(s): Ecumenismo
• Palavra(s)-Chave do Pesquisador: Coq | Ecumenismo | RNmatriz | Tableau | verificação de software | Ecumenismo lógico

Resumo

A lógica ecumênica modal oferece uma alternativa filosoficamente fundamentada para a busca pela harmonia entre a lógica modal clássica e intuicionista. RNmatrizes, por sua vez, são estruturas algébricas não-determinísticas que têm se mostrado promissoras para a caracterização de lógicas que não admitem semânticas de matrizes finitas tradicionais, como é o caso da lógica ecumênica. O presente projeto tem como principal objetivo obter uma nova semântica para a lógica ecumênica modal por meio das RNmatrizes. Para isso, propomos desenvolver o trabalho em três frentes: teoria, implementação e verificação. Ao final, esperamos ter obtido, como sub-produtos, novos sistemas de prova implementados em software para a lógica ecumênica modal proposicional e de primeira ordem.