We present a proof net calculus for the Displacement calculus and show its
correctness. This is the first proof net calculus which models the Displacement
calculus directly and not by some sort of translation into another formalism.
The proof net calculus opens up new possibilities for parsing and proof search
with the Displacement calculus.

提出一种证网演算用于位移演算，并证明其正确性。这是第一个直接模拟位移演算而不是通过某种形式的转换到其他形式的证网演算。该证网演算为使用位移演算进行句法分析和证明搜索带来了新的可能性。

位移演算的证明网

Proof nets for the Displacement calculus

First-order multiplicative intuitionistic linear logic (MILL1) can be seen as
an extension of the Lambek calculus. In addition to the fragment of MILL1 which
corresponds to the Lambek calculus (of Moot & Piazza 2001), I will show
fragments of MILL1 which generate the multiple context-free languages and which
correspond to the Displacement calculus of Morrilll e.a.

该研究介绍一阶乘性直觉线性逻辑（MILL1），展示 Lambek calculus、multiple context-free languages 以及 Displacement calculus (Morrill 等人) 三种不同的 MILL1 片段。