@inproceedings{be73dfc4a04c459bb413fc2b156c06c7,
title = "On Combinatorial Proofs for Modal Logic",
abstract = "In this paper we extend Hughes{\textquoteright} combinatorial proofs to modal logics. The crucial ingredient for modeling the modalities is the use of a self-dual non-commutative operator that has first been observed by Retor{\'e} through pomset logic. Consequently, we had to generalize the notion of skew fibration from cographs to Guglielmi{\textquoteright}s relation webs. Our main result is a sound and complete system of combinatorial proofs for all normal and non-normal modal logics in the -tesseract. The proof of soundness and completeness is based on the sequent calculus with some added features from deep inference.",
keywords = "Combinatorial proofs, Modal logic, Relation webs, S4-tesseract, Skew fibration",
author = "Matteo Acclavio and Lutz Stra{\ss}burger",
note = "Publisher Copyright: {\textcopyright} 2019, Springer Nature Switzerland AG.; 28th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2019 ; Conference date: 03-09-2019 Through 05-09-2019",
year = "2019",
month = jan,
day = "1",
doi = "10.1007/978-3-030-29026-9\_13",
language = "English",
isbn = "9783030290252",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer",
pages = "223--240",
editor = "Serenella Cerrito and Andrei Popescu",
booktitle = "Automated Reasoning with Analytic Tableaux and Related Methods - 28th International Conference, TABLEAUX 2019, Proceedings",
}