Busca avançada
Ano de início
Entree

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 racioc1nio diagramático em todas as suas etapas, a saber: (i) desenvolvimento de software (ii) depuração (iii) documentação. Dentre as principais caracter1sticas 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 racioc1nio diagramático, e da descrição completa do ambiente, incluindo os resultados obtidos durante a fase de depuração.

Matéria(s) publicada(s) na Agência FAPESP sobre a bolsa:
Mais itensMenos itens
Matéria(s) publicada(s) em Outras Mídias ( ):
Mais itensMenos itens
VEICULO: TITULO (DATA)
VEICULO: TITULO (DATA)

Publicações científicas
(As publicações científicas contidas nesta página são originárias da Web of Science ou da SciELO, cujos autores mencionaram números dos processos FAPESP concedidos a Pesquisadores Responsáveis e Beneficiários, sejam ou não autores das publicações. Sua coleta é automática e realizada diretamente naquelas bases bibliométricas)
LEME, RENATO R.; CONIGLIO, MARCELO E.; LOPES, BRUNO. . JOURNAL OF SYMBOLIC LOGIC, v. N/A, p. 36-pg., . (20/16353-3, 21/01025-3)
LEME, RENATO; CONIGLIO, MARCELO; LOPES, BRUNO; VENTURI, GIORGIO. . STUDIA LOGICA, v. N/A, p. 28-pg., . (21/01025-3)