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

Lambeks Syntactic Calculus, commonly referred to as the Lambek calculus, was
innovative in many ways, notably as a precursor of linear logic. But it also
showed that we could treat our grammatical framework as a logic (as opposed to
a logical theory). However, though it was successful in giving at least a basic
treatment of many linguistic phenomena, it was also clear that a slightly more
expressive logical calculus was needed for many other cases. Therefore, many
extensions and variants of the Lambek calculus have been proposed, since the
eighties and up until the present day. As a result, there is now a large class
of calculi, each with its own empirical successes and theoretical results, but
also each with its own logical primitives. This raises the question: how do we
compare and evaluate these different logical formalisms? To answer this
question, I present two unifying frameworks for these extended Lambek calculi.
Both are proof net calculi with graph contraction criteria. The first calculus
is a very general system: you specify the structure of your sequents and it
gives you the connectives and contractions which correspond to it. The calculus
can be extended with structural rules, which translate directly into graph
rewrite rules. The second calculus is first-order (multiplicative
intuitionistic) linear logic, which turns out to have several other,
independently proposed extensions of the Lambek calculus as fragments. I will
illustrate the use of each calculus in building bridges between analyses
proposed in different frameworks, in highlighting differences and in helping to
identify problems.

该论文通过建立 Lambek calculus 的扩展和变体的两个统一框架，利用证明网和图重写规则建立逻辑框架，用于在不同的语言分析框架之间架起桥梁，强调区别，帮助识别问题。