Graphical Sequent Calculi for Modal Logics
Minghui Ma (Sun Yat-Sen University), Ahti-Veikko Pietarinen (Tallinn, University of Technology)
TL;DR
This paper introduces graphical sequent calculi for modal logics based on Peirce's graphical notation, reformulating classical propositional logic and establishing translations between graphs and modal formulas.
Contribution
It develops deep inference graphical calculi for normal modal logics, connecting them with traditional sequent calculi through formal translations.
Findings
Graphical calculi are based on Peirce's notation.
Translations between graphs and modal formulas are established.
Graphical calculi are of the deep inference type.
Abstract
The syntax of modal graphs is defined in terms of the continuous cut and broken cut following Charles Peirce's notation in the gamma part of his graphical logic of existential graphs. Graphical calculi for normal modal logics are developed based on a reformulation of the graphical calculus for classical propositional logic. These graphical calculi are of the nature of deep inference. The relationship between graphical calculi and sequent calculi for modal logics is shown by translations between graphs and modal formulas.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.