A linear logic framework for multimodal logics

DOI10.1017/S0960129522000366MaRDI QIDQ5889307zbMATH OpenOpenAlexFDO

Authors Bruno Xavier, Carlos Olarte, Elaine Pimentel

Publication date 19 April 2023

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

Copyright license Creative Commons Attribution 4.0 International

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

zbMATH Keywords

linear logiccut eliminationmultimodal logicslinear-nested systems

Mathematics Subject Classification ID

Computer science (68-XX)

Recommendations

• A fresh view of linear logic as a logical framework
• An extended framework for specifying and reasoning about proof systems
• A uniform framework for substructural logics with modalities
• On the Specification of Sequent Systems
• A framework for proof systems

Cites work

• scientific article; zbMATH DE number 1612551 (Why is no real title available?)
• scientific article; zbMATH DE number 956466 (Why is no real title available?)
• scientific article; zbMATH DE number 517072 (Why is no real title available?)
• scientific article; zbMATH DE number 1749009 (Why is no real title available?)
• scientific article; zbMATH DE number 7204444 (Why is no real title available?)
• A focused linear logical framework and its application to metatheory of object logics
• A formal framework for specifying sequent calculus proof systems
• A formally verified cut-elimination procedure for linear nested sequents for tense logic
• A framework for proof systems
• A fresh view of linear logic as a logical framework
• A modal view of linear logic
• A semantical view of proof systems
• A uniform framework for substructural logics with modalities
• An adequate compositional encoding of bigraph structure in linear logic with subexponentials
• An analysis of (linear) exponentials based on extended sequents
• An extended framework for specifying and reasoning about proof systems
• Cut-free sequent calculi for some tense logics
• Eine Darstellung der Intuitionistischen Logik in der Klassischen
• Focusing and polarization in linear, intuitionistic, and classical logics
• Formalized meta-theory of sequent calculi for linear logics
• Formalizing the meta-theory of first-order predicate logic
• From Proofs to Focused Proofs: A Modular Proof of Focalization in Linear Logic
• Light linear logic
• Linear Nested Sequents, 2-Sequents and Hypersequents
• Logic Programming with Focusing Proofs in Linear Logic
• Mechanizing focused linear logic in Coq
• Modularisation of sequent calculi for normal and non-normal modalities
• Nominal logic, a first order theory of names and binding
• On structuring proof search for first order linear logic
• On subexponentials, focusing and modalities in concurrent systems
• Parametric higher-order abstract syntax for mechanized semantics
• Proving structural properties of sequent systems in rewriting logic
• Quati: an automated tool for proving permutation lemmas
• Sequentialising nested systems
• Structural cut elimination. I: Intuitionistic and classical logic
• Subexponentials in non-commutative linear logic
• The Method of Tree-Hypersequents for Modal Propositional Logic

Cited in

(2)

• Unification and Inference Rules in the Multi-modal Logic of Knowledge and Linear Time LTK
• A decidable multi-modal logic of context

Describes a project that uses

Uses Software

• GitHub
• Quati
• HYBRID

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5889307)