非可換論理

ヨアヒム・ランベックは、 1958年の論文「文構造の数学」で、自然言語の構文の組み合わせの可能性をモデル化するために、最初の非可換論理を提案した。^{[ 1 ]} その後の1961年の論文「構文型の計算について」では、非結合性も含むように分析を拡張した。彼の計算は、それ以来、計算言語学の基本的な形式体系の1つとなっている。

デイビッド・N・イェッターは、線形論理の交換規則の代わりに、より弱い構造規則を提案し、循環線形論理を生み出した。^{[ 2 ]} 循環線形論理のシーケントはサイクルを形成するため、回転に対して不変であり、多重前提規則は、規則で記述された式でサイクルを結合する。この計算は、3つの構造様相、交換を可能にするが依然として線形である自己双対様相、および 線形論理の通常の指数（?と!)をサポートし、非線形構造規則を交換とともに使用できるようにする。

ポムセット論理は、クリスチャン・レトレによって、通常の線形論理のテンソル積演算子とパー演算子に加えて2つの双対逐次演算子が存在する意味論的形式で提案され、可換演算子と非可換演算子の両方を持つ最初の論理として提案されました。^{[ 3 ]} この論理のシーケント計算は与えられましたが、カット除去定理が欠けていました。代わりに、計算の意味は表示的意味論によって確立されました。

アレッシオ・グリエルミは、レトーレの計算体系BVの変形版を提案した。この変形版では、2つの非可換演算が単一の自己双対演算子に縮約され、この計算体系に対応するために、構造計算という新しい証明計算体系が提案された。構造計算の主な斬新さは、深層推論を広く用いている点であり、これは可換演算子と非可換演算子を組み合わせた計算体系には必要であると主張された。この説明は、カット除去を持つポムセット論理のシーケントシステムを設計することの難しさと一致する。

ルッツ・シュトラスブルガーは、構造計算の分野において、混合規則を持つ線形論理をサブシステムとして用いる関連システムであるNELを考案した。