Labelled Connection-based Proof Search for Multiplicative Intuitionistic Linear Logic
Authors: Daniel Mery and Didier Galmiche
Paper Information
Title: | Labelled Connection-based Proof Search for Multiplicative Intuitionistic Linear Logic |
Authors: | Daniel Mery and Didier Galmiche |
Proceedings: | ARQNL Full papers, demo papers and invited contributions |
Editors: | Christoph Benzmüller and Jens Otten |
Keywords: | Linear Logic, Connection-based proof-search, Labelled proof-systems |
Abstract: | 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 worlds semantics of the logic. We briefly recall the purely syntactic sequent calculus for MILL, which we call LMILL and then propose a sound and complete labelled sequent calculus GMILL for MILL. We then show how to translate every LMILL proof into a GMILL proof. From this translation, refining our results on BI (The logic of Bunched Implications), we show the soundness of the connection-based characterization and its completeness without the need for any notion of multiplicity. |
Pages: | 1 |
Talk: | Jul 18 12:00 (Session 126A: ARQNL Regular Papers 2) |
Paper: |