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

  • Renato R. Leme UNICAMP
  • Giorgio Venturi UNICAMP
  • Bruno Lopes UFF

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.
Publicado
31/07/2022
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.