2020/01/07 by Simone Martini, Martini, Simone, Andrea Masini +3
Computer Science · #Advanced Algebra and Logic #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems
paper · pdf · doi:10.48550/arxiv.2001.02029
openalex publication_date 2020/01/07 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
Extending and generalizing the approach of 2-sequents (Masini, 1992), we present sequent calculi for the classical modal logics in the K, D, T, S4 spectrum. The systems are presented in a uniform way-different logics are obtained by tuning a single parameter, namely a constraint on the applicability of a rule. Cut-elimination is proved only once, since the proof goes through independently from the constraints giving rise to the different systems. A sequent calculus for the discrete linear temporal logic ltl is also given and proved complete. Leitmotiv of the paper is the formal analogy between modality and first-order quantification.