Proof-Theoretic Semantics for Intuitionistic Multiplicative Linear Logic

Citations of this article
Mendeley users who have this article in their library.

This article is free to access.


This work is the first exploration of proof-theoretic semantics for a substructural logic. It focuses on the base-extension semantics (B-eS) for intuitionistic multiplicative linear logic ($$\mathrm IMLL$$ ). The starting point is a review of Sandqvist’s B-eS for intuitionistic propositional logic (IPL), for which we propose an alternative treatment of conjunction that takes the form of the generalized elimination rule for the connective. The resulting semantics is shown to be sound and complete. This motivates our main contribution, a B-eS for $$\mathrm IMLL$$, in which the definitions of the logical constants all take the form of their elimination rule and for which soundness and completeness are established.




Gheorghiu, A. V., Gu, T., & Pym, D. J. (2023). Proof-Theoretic Semantics for Intuitionistic Multiplicative Linear Logic. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 14278 LNAI, pp. 367–385). Springer Science and Business Media Deutschland GmbH.

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free