A decidable linear logic for transforming DRSs in context

Abstract

We present a decidable linear logic for encoding and transforming Discourse Representation Structures (DRSs) in context. The logic is a particular fragment of intuitionistic propositional linear logic (ILL), slimmed down by not allowing for any occurrence of exponential, !, in the consequence and slightly enriched by allowing to combine commutative and non-commutative multiplicative connectives. Its model is given as processes with geometric structure, which can also be seen as proofnets explicit with respect to location and direction We show that the model is rich enough to encode DRSs and that the proof search is bound to be finite and terminates.