TY - GEN
T1 - Combinatorial Proofs for Constructive Modal Logic
AU - Acclavio, Matteo
AU - Straßburger, Lutz
N1 - Publisher Copyright:
© 2022 College Publications. All rights reserved.
PY - 2022/1/1
Y1 - 2022/1/1
N2 - Combinatorial proofs form a syntax-independent presentation of proofs, originally proposed by Hughes for classical propositional logic. In this paper we present a notion of combinatorial proofs for the constructive modal logics CK and CD, we show soundness and completeness of combinatorial proofs by translation from and to sequent calculus proofs, and we discuss the notion of proof equivalence enforced by these translations.
AB - Combinatorial proofs form a syntax-independent presentation of proofs, originally proposed by Hughes for classical propositional logic. In this paper we present a notion of combinatorial proofs for the constructive modal logics CK and CD, we show soundness and completeness of combinatorial proofs by translation from and to sequent calculus proofs, and we discuss the notion of proof equivalence enforced by these translations.
KW - arena nets
KW - combinatorial proofs
KW - constructive modal logic
KW - proof equivalence
UR - https://www.scopus.com/pages/publications/85171882219
M3 - Conference contribution
AN - SCOPUS:85171882219
T3 - Advances in Modal Logic
SP - 15
EP - 36
BT - Advances in Modal Logic, AiML 2022
A2 - Fernandez-Duque, David
A2 - Palmigiano, Alessandra
A2 - Palmigiano, Alessandra
A2 - Pinchinat, Sophie
PB - College Publications
T2 - 14th Conference on Advances in Modal Logic, AiML 2022
Y2 - 22 August 2022 through 25 August 2022
ER -