Coq Formalization of a Tableau for the Classical-Intuitionistic Propositional Fragment of Ecumenical Logic

Autor:	Renato R. Leme, Giorgio Venturi, Bruno Lopes
Rok vydání:	2022
Zdroj:	Anais do III Workshop Brasileiro de Lógica (WBL 2022).
Popis:	In this paper, we describe a tableau system for reasoning about ecumenical propositional logic, and introduce the central definitions of its implementation in the Coq proof assistant.
Databáze:	OpenAIRE
Externí odkaz:	https://explore.openaire.eu/search/publication?articleId=doi_________::52d0da31945b89966a0a7aac41742892 https://doi.org/10.5753/wbl.2022.223071 Zobrazit plný text záznamu