Genericidade no contexto da demonstração de teoremas: um assistente de prova baseado em nuvem para linguagens orientadas a fluxo

• Processo: 21/01025-3
• Modalidade de apoio: Bolsas no Brasil - Doutorado
• Data de Início da vigência: 01 de novembro de 2021
• Data de Término da vigência: 31 de julho de 2026
• Área de conhecimento: Ciências Humanas - Filosofia - Lógica
• Pesquisador responsável: Marcelo Esteban Coniglio
• Beneficiário: Renato Reis Leme
• Instituição Sede: Instituto de Filosofia e Ciências Humanas (IFCH). Universidade Estadual de Campinas (UNICAMP). Campinas , SP, Brasil
• Bolsa(s) vinculada(s): 23/16021-9 - Ecumenismo Modal via RNmatrizes: Teoria, Implementação e Verificação, BE.EP.DR
• Assunto(s): Raciocínio Linguagem de programação Homomorfismo Grafos
• Palavra(s)-Chave do Pesquisador: grafo | Lógica | proof assistant | Raciocínio diagramático | Proof assistant

Resumo

O presente projeto propõe o desenvolvimento completo de um assistente de prova voltado para o raciocínio diagramático em todas as suas etapas, a saber: (I) desenvolvimento de software; (II) depuração; (III) documentação. Dentre as principais características desta proposta, destacam-se a implementação do paradigma de programação genérica através da noção de homomorfismo entre grafos, a implementação de uma linguagem formal para a especificação de tablôs, a criação de um sistema de cadastro de usuários com distinção de perfil, bem como a hospedagem do ambiente inteiramente em nuvem, facilitando a portabilidade e tornando o sistema ideal para contextos de EAD. Além do software, o projeto prevê o desenvolvimento da tese contendo uma exposição da teoria formal dos assistentes de prova (teoria dos tipos), dos aspectos filosóficos envolvidos no conceito de raciocínio diagramático, e da descrição completa do ambiente, incluindo os resultados obtidos durante a fase de depuração. (AU)

Publicações científicas

(Referências obtidas automaticamente do Web of Science e do SciELO, por meio da informação sobre o financiamento pela FAPESP e o número do processo correspondente, incluída na publicação pelos autores)

LEME, RENATO; CONIGLIO, MARCELO; LOPES, BRUNO; VENTURI, GIORGIO. Ecumenical Propositional Tableau. STUDIA LOGICA, v. N/A, p. 28-pg., 2024-02-16. (21/01025-3)