Multi-type Sequent Calculi
Sabine Frittella, Giuseppe Greco, Alexander Kurz, Alessandra, Palmigiano, Vlasta Sikimic

TL;DR
This paper introduces multi-type sequent calculi that extend display calculi by allowing multiple types and relaxing display properties, enabling better handling of complex logics like multi-modal and dynamic logics.
Contribution
It generalizes display calculi to a multi-type framework and weakens display properties, broadening applicability to diverse logical systems.
Findings
Establishes a canonical cut elimination meta-theorem for multi-type calculi.
Shows the framework's usefulness for multi-modal and dynamic logics.
Provides a unified proof-theoretic setting for generalized calculi.
Abstract
Display calculi are generalized sequent calculi which enjoy a `canonical' cut elimination strategy. That is, their cut elimination is uniformly obtained by verifying the assumptions of a meta-theorem, and is preserved by adding or removing structural rules. In the present paper, we discuss a proof-theoretic setting, inspired both to Belnap's Display Logic and to Sambin's Basic Logic, which generalises these calculi in two directions: by explicitly allowing different types, and by weakening the so-called display and visibility properties. The generalisation to a multi-type environment makes it possible to introduce specific tools enhancing expressivity, which have proved useful e.g. for a smooth proof-theoretic treatment of multi-modal and dynamic logics. The generalisation to a setting in which full display property is not required makes it possible to account for logics which admit…
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.
Taxonomy
TopicsLogic, Reasoning, and Knowledge · Logic, programming, and type systems · Semantic Web and Ontologies
