Coq Formalization of a Tableau for the Classical-Intuitionistic Propositional Fragment of Ecumenical Logic - Leme, Renato R.; Venturi, Giorgio; Lopes, Bruno (Anais do Workshop Brasileiro de Lógica (WBL); 2022: Anais do III Workshop Brasileiro de Lógica, 2022)
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.