Modularisation of sequent calculi for normal and non-normal modalities
B Lellmann, E Pimentel - ACM Transactions on Computational Logic …, 2019 - dl.acm.org
In this work, we explore the connections between (linear) nested sequent calculi and
ordinary sequent calculi for normal and non-normal modal logics. By proposing local …
ordinary sequent calculi for normal and non-normal modal logics. By proposing local …
Linear logic by levels and bounded time complexity
P Baillot, D Mazza - Theoretical Computer Science, 2010 - Elsevier
We give a new characterization of elementary and deterministic polynomial time
computation in linear logic through the proofs-as-programs correspondence. Girard's …
computation in linear logic through the proofs-as-programs correspondence. Girard's …
[PDF][PDF] A uniform framework for substructural logics with modalities.
It is well known that context dependent logical rules can be problematic both to implement
and reason about. This is one of the factors driving the quest for better behaved, ie, local …
and reason about. This is one of the factors driving the quest for better behaved, ie, local …
A linear logic framework for multimodal logics
B Xavier, C Olarte, E Pimentel - Mathematical Structures in …, 2022 - cambridge.org
One of the most fundamental properties of a proof system is analyticity, expressing the fact
that a proof of a given formula F only uses subformulas of F. In sequent calculus, this …
that a proof of a given formula F only uses subformulas of F. In sequent calculus, this …
An approach to infinitary temporal proof theory
S Baratella, A Masini - Archive for Mathematical Logic, 2004 - Springer
Aim of this work is to investigate from a proof-theoretic viewpoint a propositional and a
predicate sequent calculus with an ω–type schema of inference that naturally interpret the …
predicate sequent calculus with an ω–type schema of inference that naturally interpret the …
A fresh view of linear logic as a logical framework
C Olarte, E Pimentel, B Xavier - Electronic Notes in Theoretical Computer …, 2020 - Elsevier
One of the most fundamental properties of a proof system is analyticity, expressing the fact
that a proof of a given formula F only uses subformulas of F. In sequent calculus, this …
that a proof of a given formula F only uses subformulas of F. In sequent calculus, this …
Nested Sequents or Tree-Hypersequents—A Survey
B Lellmann, F Poggiolesi - Saul Kripke on Modal Logic, 2024 - Springer
This paper presents an overview of the methods of nested sequents or tree-hypersequents
that were originally introduced to provide a comprehensive proof theory for modal logic. The …
that were originally introduced to provide a comprehensive proof theory for modal logic. The …
A proof-theoretic investigation of a logic of positions
S Baratella, A Masini - Annals of Pure and Applied Logic, 2003 - Elsevier
We introduce an extension of natural deduction that is suitable for dealing with modal
operators and induction. We provide a proof reduction system and we prove a strong …
operators and induction. We provide a proof reduction system and we prove a strong …
Type inference in intuitionistic linear logic
P Baillot, M Hofmann - Proceedings of the 12th international ACM …, 2010 - dl.acm.org
We study the type checking and type inference problems for intuitionistic linear logic: given a
System F typed λ-term,(i) for an alleged linear logic type, determine whether there exists a …
System F typed λ-term,(i) for an alleged linear logic type, determine whether there exists a …
Multi-modalities and non-commutativity/associativity in functorial linear logic: a case study
C Olarte, E Pimentel - arXiv preprint arXiv:2404.11445, 2024 - arxiv.org
Similar to modal connectives, the exponential! in intuitionistic linear logic (ILL) is not
canonical, in the sense that if $ i\not= j $ then $!^ i F\not\equiv!^ j F $. Intuitively, this means …
canonical, in the sense that if $ i\not= j $ then $!^ i F\not\equiv!^ j F $. Intuitively, this means …