Coq Formalization of a Tableau for the Classical-Intuitionistic Propositional Fragment of Ecumenical Logic
Resumo
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.
Palavras-chave:
proof assistants, logical frameworks, non-classical logics
Referências
Fitting, M. (2013). Proof methods for modal and intuitionistic logics, volume 169. Springer Science & Business Media.
Krauss, P. (1992). A constructive refinement of classical logic.
Pereira, L. C. and Rodriguez, R. O. (2017). Normalization, soundness and completeness for the propositional fragment of prawitz’ecumenical system. Revista Portuguesa de Filosofia, 73(3):1153–1168. Publisher: JSTOR.
Pimentel, E., Pereira, L. C., and de Paiva, V. (2021). An ecumenical notion of entailment. Synthese, 198(22):5391–5413.
Krauss, P. (1992). A constructive refinement of classical logic.
Pereira, L. C. and Rodriguez, R. O. (2017). Normalization, soundness and completeness for the propositional fragment of prawitz’ecumenical system. Revista Portuguesa de Filosofia, 73(3):1153–1168. Publisher: JSTOR.
Pimentel, E., Pereira, L. C., and de Paiva, V. (2021). An ecumenical notion of entailment. Synthese, 198(22):5391–5413.
Publicado
31/07/2022
Como Citar
LEME, Renato R.; VENTURI, Giorgio; LOPES, Bruno.
Coq Formalization of a Tableau for the Classical-Intuitionistic Propositional Fragment of Ecumenical Logic. In: WORKSHOP BRASILEIRO DE LÓGICA (WBL), 3. , 2022, Niterói.
Anais [...].
Porto Alegre: Sociedade Brasileira de Computação,
2022
.
p. 25-32.
ISSN 2763-8731.
DOI: https://doi.org/10.5753/wbl.2022.223071.
