Genericity in the context of theorem proving: a cloud based proof assistant for flow-based languages

• Grant number: 21/01025-3
• Support type: Scholarships in Brazil - Doctorate
• Effective date (Start): November 01, 2021
• Effective date (End): July 31, 2025
• Field of knowledge: Humanities - Philosophy - Logic
• Principal researcher: Giorgio Venturi
• Grantee: Renato Reis Leme
• Home Institution: Instituto de Filosofia e Ciências Humanas (IFCH). Universidade Estadual de Campinas (UNICAMP). Campinas , SP, Brazil

Abstract

This project proposes the complete development of a proof assistant focused on diagrammatic reasoning in all its stages, namely: (i) software development (ii) debugging (iii) documentation. Among the main characteristics of this proposal, we highlight the implementation of the generic language paradigm through the notion of homomorphism between graphs, the implementation of a formal language for the specification of tableaux, the creation of a user management system with distinction of profiles, as well as hosting the environment entirely in the cloud, facilitating portability and making the system ideal for distance learning contexts. In addition to the software, we propose to develop the thesis containing an exposition of the formal theory of test assistants (type theory), the philosophical aspects involved in the concept of diagrammatic reasoning, and the complete description of the environment, including the results obtained during debugging phase. (AU)