A decidable linear logic for transforming DRSs in context
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), slimed 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. The resulting logic is weaker
than classical intuitionistic logic because no formulas in the form of !A -o B can be
constructed as they lead to the occurrence of !A in the consequence by the -o Left rule. Its
model is given as processes with geometric structure, which can also be seen as proofnets explicit with respect to
locations. We show that the model is rich enough to encode DRSs and that the proof search is bound to be finite
and terminates.
Tsutomu Fujinami