Skip to Main content Skip to Navigation
Conference papers

Labelled Connection-based Proof Search for Multiplicative Intuitionistic Linear Logic

Didier Galmiche 1 Daniel Méry 1
1 TYPES - Logic, Proof Theory and Programming
LORIA - FM - Department of Formal Methods
Abstract : We propose a connection-based characterization for multiplicative intuitionistic linear logic ({\MILL}) which is based on labels and constraints that capture Urquhart's possible world semantics of the logic. We first briefly recall the purely syntactic sequent calculus for {\MILL}, which we call LMILL. Then, in the spirit of our previous results on the Logic of Bunched Implications (BI), we present a connection-based characterization of MILL provability. We show its soundness and completeness without the need for any notion of multiplicity. From the characterization, we finally propose a labelled sequent calculus for MILL.
Document type :
Conference papers
Complete list of metadatas

https://hal.univ-lorraine.fr/hal-02982539
Contributor : Didier Galmiche <>
Submitted on : Wednesday, October 28, 2020 - 4:27:53 PM
Last modification on : Friday, October 30, 2020 - 3:29:45 AM

Identifiers

  • HAL Id : hal-02982539, version 1

Collections

Citation

Didier Galmiche, Daniel Méry. Labelled Connection-based Proof Search for Multiplicative Intuitionistic Linear Logic. International Workshop on Automated Reasoning in Quantified Non-Classical Logics, ARQNL 2018, 2018, Oxford, United Kingdom. pp.49-63. ⟨hal-02982539⟩

Share

Metrics

Record views

3