A linear logic framework for multimodal logics

DOI10.1017/S0960129522000366OpenAlexW4309783737MaRDI QIDQ5889307

Carlos Olarte, Bruno Xavier, Elaine Pimentel

Publication date: 19 April 2023

Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1017/s0960129522000366

zbMATH Keywords

cut eliminationlinear logicmultimodal logicslinear-nested systems

Mathematics Subject Classification ID

Computer science (68-XX)

Uses Software

• HYBRID
• Quati
• GitHub

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A framework for proof systems
• Focusing and polarization in linear, intuitionistic, and classical logics
• Light linear logic
• Cut-free sequent calculi for some tense logics
• A semantical view of proof systems
• Structural cut elimination. I: Intuitionistic and classical logic
• Nominal logic, a first order theory of names and binding
• A formal framework for specifying sequent calculus proof systems
• A formally verified cut-elimination procedure for linear nested sequents for tense logic
• Sequentialising nested systems
• A fresh view of linear logic as a logical framework
• Mechanizing focused linear logic in Coq
• On subexponentials, focusing and modalities in concurrent systems
• Formalized meta-theory of sequent calculi for linear logics
• On structuring proof search for first order linear logic
• Quati: An Automated Tool for Proving Permutation Lemmas
• Linear Nested Sequents, 2-Sequents and Hypersequents
• An Adequate Compositional Encoding of Bigraph Structure in Linear Logic with Subexponentials
• The Method of Tree-Hypersequents for Modal Propositional Logic
• From Proofs to Focused Proofs: A Modular Proof of Focalization in Linear Logic
• Logic Programming with Focusing Proofs in Linear Logic
• An analysis of (linear) exponentials based on extended sequents
• A modal view of linear logic
• FORMALIZING THE META-THEORY OF FIRST-ORDER PREDICATE LOGIC
• Modularisation of Sequent Calculi for Normal and Non-normal Modalities
• A uniform framework for substructural logics with modalities
• A focused linear logical framework and its application to metatheory of object logics
• Parametric higher-order abstract syntax for mechanized semantics
• Subexponentials in non-commutative linear logic
• An extended framework for specifying and reasoning about proof systems
• Eine Darstellung der Intuitionistischen Logik in der Klassischen
• Proving structural properties of sequent systems in rewriting logic

This page was built for publication: A linear logic framework for multimodal logics