Related papers: Sequent calculi for a unity of logic
Monoidal closed categories naturally model NMILL, non-commutative multiplicative intuitionistic linear logic: the monoidal unit and tensor interpret the multiplicative verum and conjunction; the internal hom interprets linear implication.…
Full Intuitionistic Linear Logic (FILL) is multiplicative intuitionistic linear logic extended with par. Its proof theory has been notoriously difficult to get right, and existing sequent calculi all involve inference rules with complex…
In this paper we consider the class of truth-functional many-valued logics with a finite set of truth-values. The main result of this paper is the development of a new \emph{binary} sequent calculi (each sequent is a pair of formulae) for…
We present a novel linear $\lambda$-calculus for Classical Multiplicative Exponential Linear Logic (\MELL) along the lines of the propositions-as-types paradigm. Starting from the standard term assignment for Intuitionistic Multiplicative…
Classical first-order logic is in many ways central to work in mathematics, linguistics, computer science and artificial intelligence, so it is worthwhile to define it in full detail. We present soundness and completeness proofs of a…
Session type systems have been given logical foundations via Curry-Howard correspondences based on both intuitionistic and classical linear logic. The type systems derived from the two logics enforce communication correctness on the same…
Multiplicative linear logic is a very well studied formal system, and most such studies are concerned with the one-sided sequent calculus. In this paper we look in detail at existing translations between a deep inference system and the…
We introduce proper display calculi for intuitionistic, bi-intuitionistic and classical linear logics with exponentials, which are sound, complete, conservative, and enjoy cut-elimination and subformula property. Based on the same design,…
Justification logics are modal-like logics that provide a framework for reasoning about justifications. This paper introduces labeled sequent calculi for justification logics, as well as for hybrid modal-justification logics. Using the…
Nominal logic is a variant of first-order logic that provides support for reasoning about bound names in abstract syntax. A key feature of nominal logic is the new-quantifier, which quantifies over fresh names (names not appearing in any…
We present a proof-theoretical study of the interpretability logic IL, providing a wellfounded and a non-wellfounded sequent calculus for IL. The non-wellfounded calculus is used to establish a cut elimination argument for both calculi. In…
We propose a categorial grammar based on classical multiplicative linear logic. This can be seen as an extension of abstract categorial grammars (ACG) and is at least as expressive. However, constituents of {\it linear logic grammars (LLG)}…
We introduce the $L_!^S$-calculus, a linear lambda-calculus extended with scalar multiplication and term addition, that acts as a proof language for intuitionistic linear logic (ILL). These algebraic operations enable the direct expression…
Linear logic (LL) is a resource-aware, abstract logic programming language that refines both classical and intuitionistic logic. Linear logic semantics is typically presented in one of two ways: by associating each formula with the set of…
In a previous work we introduced a non-associative non-commutative logic extended by multimodalities, called subexponentials, licensing local application of structural rules. Here, we further explore this system, exhibiting a classical…
Linear logic has provided new perspectives on proof-theory, denotational semantics and the study of programming languages. One of its main successes are proof-nets, canonical representations of proofs that lie at the intersection between…
In a previous work we introduced a non-associative non-commutative logic extended by multimodalities, called subexponentials, licensing local application of structural rules. Here, we further explore this system, considering a classical…
In this paper we investigate two logics from an algebraic point of view. The two logics are: MALL (multiplicative-additive Linear Logic) and LL (classical Linear Logic). Both logics turn out to be strongly algebraizable in the sense of Blok…
Cirquent calculus is a new proof-theoretic and semantic framework, whose main distinguishing feature is being based on circuits, as opposed to the more traditional approaches that deal with tree-like objects such as formulas or sequents.…
This paper introduces a logical system, called BV, which extends multiplicative linear logic by a non-commutative self-dual logical operator. This extension is particularly challenging for the sequent calculus, and so far it is not achieved…