×

On combinatorial proofs for modal logic. (English) Zbl 1435.03041

Cerrito, Serenella (ed.) et al., Automated reasoning with analytic tableaux and related methods. 28th international conference, TABLEAUX 2019, London, UK, September 3–5, 2019. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 11714, 223-240 (2019).
Summary: In this paper we extend Hughes’ 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é through pomset logic. Consequently, we had to generalize the notion of skew fibration from cographs to Guglielmi’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 S4-tesseract. The proof of soundness and completeness is based on the sequent calculus with some added features from deep inference.
For the entire collection see [Zbl 1428.68011].

MSC:

03B45 Modal logic (including the logic of norms)
03F07 Structure of proofs
PDFBibTeX XMLCite
Full Text: DOI HAL