FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
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: