線形論理

線形論理は、フランスの論理学者ジャン＝イヴ・ジラールが古典論理と直観主義論理の改良として提案した部分構造論理であり、前者の双対性と後者の構成的性質の多くを結びつけている。 ^[¹^]この論理はそれ自体としても研究されてきたが、より広く言えば、線形論理の考え方は、プログラミング言語、ゲーム意味論、量子物理学（線形論理は量子情報理論の論理と見なせるため）^[²^] 、そして言語学[ ³^{]などの分野に影響を与えてきた。特に、リソース}^の制約、双対性、相互作用を重視していることがその理由である。

線形論理は、さまざまな表現、説明、直観に適しています。証明論的には、古典的なシーケント計算の分析から派生しており、そこでは（構造規則である）縮約と弱化の使用が慎重に制御されています。操作的には、これは論理的演繹がもはや永続的な「真理」の絶えず拡大する集合に関するものではなく、常に複製したり、自由に破棄したりできるとは限らないリソースを操作する方法でもあることを意味します。単純な表示モデルの観点から見ると、線形論理は、直観主義論理の解釈を、デカルト（閉じた）カテゴリを対称モノイド（閉じた）カテゴリに置き換えることによって洗練したもの、あるいは古典論理の解釈を、ブール代数を C*-代数に置き換えることによって洗練したものと見なすことができます。

表記法の比較

この記事ではジラールの記法に従います。さまざまな記法に慣れている読者のために、パオリが2002年にまとめた次の表^{[ 4 ]}は、複数の資料における線形論理結合子と定数の記法を比較しています。

接続詞、二元性、極性

構文

言語 $\displaystyle {\mathcal {L}}}$ 古典的な命題線形論理は、以下のように再帰的に定義できる。

もし $\varphi$ 原子式であれば、 $\varphi$ は、 $\displaystyle {\mathcal {L}}}$ 。
もし $\varphi$ 原子式であれば、 $\varphi ^{\bot }$ は、 $\displaystyle {\mathcal {L}}}$ 。
もし $\varphi$ そして $\psi$ は、 $\displaystyle {\mathcal {L}}}$ 、それから $\varphi \otimes \psi$ そうだ。
もし $\varphi$ そして $\psi$ は、 $\displaystyle {\mathcal {L}}}$ 、それから $\varphi$ $⅋$ $\psi$ そうだ。
もし $\varphi$ そして $\psi$ は、 $\displaystyle {\mathcal {L}}}$ 、それから $\varphi \ \&\ \psi$ そうだ。
もし $\varphi$ そして $\psi$ は、 $\displaystyle {\mathcal {L}}}$ 、それから $\varphi \oplus \psi$ そうだ。
もし $\varphi$ は、 $\displaystyle {\mathcal {L}}}$ 、それから ${\displaystyle$ も同様です。
もし $\varphi$ は、 $\displaystyle {\mathcal {L}}}$ 、それから ${\displaystyle$ も同様です。
${\bf {1}}$ は、 $\displaystyle {\mathcal {L}}}$ 。
$\bot$ は、 $\displaystyle {\mathcal {L}}}$ 。
$\top$ は、 $\displaystyle {\mathcal {L}}}$ 。
$\displaystyle {\bf {0}}}$ は、 $\displaystyle {\mathcal {L}}}$ 。

ここで $、p$ と $p ⊥ は$ 論理原子の範囲をとります。後述する理由により、結合子⊗、⅋、1、および ⊥ は乗法、結合子 &、⊕、⊤、および 0 は加法、結合子 ! および ? は指数と呼ばれます。さらに、次の用語を用いることができます。

二項結合子⊗、⊕、&、⅋は結合法則と交換法則を満たします。⊗の単位は1、⊕の単位は0、⅋の単位は⊥、&の単位は⊤です。

CLLにおけるすべての命題 $A$ には、以下のように定義される双対 $A⊥ が$ 存在する。

$(-) ⊥ は$ 対合であることに注意してください。つまり、すべての命題に対して $A ⊥⊥ = A$ です。A $⊥ は$ $A$ の線形否定とも呼ばれます。

表の列は、線形論理の結合子を分類する別の方法を示唆している。極性：左列で否定されている結合子（⊗、⊕、1、0、!正と呼ばれ、右列のそれらの双対（⅋、&、⊥、⊤、?負と呼ばれます。右の表を参照してください。

線形含意は接続詞の文法には含まれませんが、CLLでは線形否定と乗法選言を用いて、 $A ⊸ B := A ⊥ ⅋ B$ と定義できます。接続詞 ⊸ はその形状からロリポップ

シーケント微積分プレゼンテーション

線形論理を定義する一つの方法は、シーケント計算として定義することです。命題の有限リスト $A$ $1$ $, ...,$ $A$ $n$ (コンテキストとも呼ばれる) を、文字 $Γ$ と $Δ$ で表します。シーケントは、コンテキストをターンスタイル ( $Γ$ と表記) の左右に配置します。 $\vdash$ $Γ$ の連言が $Δ$ の選言を含意すると主張します(ただし、ここで言う連言と選言は、後述する「乗法的」なものです)。ジラールは、古典的な線形論理を片側シーケント (左側のコンテキストが空の場合) のみを使用して記述しており、ここではそのより簡潔な表現に従います。これは、ターンスタイルの左側にある前提は常に反対側に移動して双対化できるため可能です。

ここでは、シーケントの証明を構築する方法を記述する推論規則を示します。 ^{[ 8 ]}

まず、文脈内の命題の順序を気にしないという事実を形式化するために、交換の構造規則を追加します。

弱化と縮約の構造規則は追加しないことに注意してください。なぜなら、シーケントにおける命題の欠如と、存在するコピーの数に関心があるからです。

次に、初期シーケントとカットを追加します。

カット規則は証明を構成する方法と見なすことができ、初期シーケントは構成単位として機能します。ある意味では、これらの規則は冗長です。以下で証明を構築するための追加の規則を導入すると、任意の初期シーケントが原子初期シーケントから導出できること、およびシーケントが証明可能である場合はいつでもカットフリーの証明を与えることができるという性質が得られます。最終的に、この標準形の性質（原子初期シーケントの完全性とカット除去定理に分けられ、解析的証明の概念を誘導します）は、線形論理を証明探索やリソース認識ラムダ計算に使用できるため、コンピュータ科学における線形論理の応用の根底にあります。

さて、論理規則を与えることで、結合子について説明します。通常、シーケント計算では、各結合子に対して「右規則」と「左規則」の両方が与えられ、その結合子を含む命題に関する2つの推論モード（例えば、検証と反証）が記述されます。一方、片側的な説明では、代わりに否定を用います。結合子（例えば⅋）の右規則は、その双対（⊗）の左規則の役割を果たします。したがって、結合子の規則と双対の規則の間には、ある種の「調和」が期待されます。

乗法

乗法的な論理積（⊗）と論理和（⅋）の規則：

そして各部隊については：

乗法的な連言と選言の規則は、古典的な解釈の下では、単純な連言と選言に対して許容される（つまり、それらは LKにおいて許容される規則である）ことに注意してください。

添加物

加法的な論理積（&）と論理和（⊕）の規則：

そして各部隊については：

加法的な結合と選言の規則は、古典的な解釈の下では再び許容されることに注意してください。しかし、ここで、2 つの異なる結合の規則における乗法/加法の区別の根拠を説明できます。乗法的な結合子 (⊗) の場合、結論 ( $Γ, Δ$ ) の文脈は前提間で分割されますが、加法的な結合子 (&) の場合、結論 ( $Γ$ ) の文脈は両方の前提にそのまま引き継がれます。

指数関数

指数関数は、弱化と収縮への制御されたアクセスを提供するために使用されます。具体的には、 $?$ 'd 命題に対する弱化と収縮の構造規則を追加します。 ^{[ 9 ]}

そして、次の論理規則を使用します。ここで $、?Γは、それぞれに$ $?$ が接頭辞として付いた命題のリストを表します。

指数関数の規則は他の結合子の規則とは異なるパターンに従っており、通常の様相論理 S4のシーケント計算形式化における様相を支配する推論規則に似ており、双対 $!$ と $?の間にはもはや明確な対称性がないことに気づくかもしれない。この状況は、CLLの別の表現（例えば、$ LU表現）で改善される。

驚くべき公式

上述のド・モルガンの双対性に加えて、線形論理における重要な等価性には以下のようなものがある。

分配性

$A ⊸ Bを$ $A ⊥ ⅋ B$ と定義すると、最後の 2 つの分配法則から次の式も導かれる。

（ここで $A ≣ B$ は $(A ⊸ B) かつ (B ⊸ A)$ を意味します。）

指数同型性

線形分布

同型写像ではないが、線形論理において重要な役割を果たす写像は次のとおりである。

線形分布は、線形論理の証明論において基本的なものである。この写像の結果は、Cockett & Seely (1997) で初めて調査され、「弱い分布」と呼ばれた。^{[ 10 ]}その後の研究では、線形論理との基本的なつながりを反映するために、「線形分布」と改名された。

その他の影響

以下の分配法則は一般に同値関係ではなく、単なる含意関係である。

古典論理／直観主義論理の拡張

直観主義的含意と古典的含意の両方は、指数を挿入することで線形含意から復元できます。直観主義的含意は $! A ⊸ B$ $と符号化され、古典的含意は!? A ⊸ ? B$ または $! A ⊸ ?! B$ (またはさまざまな代替可能な翻訳)と符号化できます。 ^{[ 11 ]}指数を使用すると、必要なだけ式を使用できるため、これは古典的論理と直観主義的論理では常に可能です。

形式的には、直観主義論理の式を線形論理の式に変換する方法が存在し、その変換によって、元の式が直観主義論理で証明可能であるのは、変換後の式が線形論理で証明可能である場合に限る、ということが保証される。ゲーデル＝ゲンツェンの否定変換を用いることで、古典一階述語論理を線形一階述語論理に埋め込むことができる。

プルーフシステム

プルーフネット

ジャン＝イヴ・ジラールによって導入された証明ネットは、官僚主義を回避するために作られた。官僚主義とは、論理的な観点からは2つの導出を異ならせるが、「道徳的」な観点からは異ならないすべてのことである。

例えば、以下の2つの証明は「道徳的に」同一である。

プルーフネットの目的は、それらをグラフィカルに表現することで、それらを同一にすることである。

意味論

線形論理には、リソースに敏感な論理システムとしての複雑な性質を反映して、複数の異なる意味論が開発されてきました。古典論理や直観主義論理とは異なり、線形論理は式を組み合わせるさまざまな方法を区別し、仮定を無限に再現できるものではなく、証明中に消費される有限のリソースとして扱います。^{[ 5 ]}

主な意味論的アプローチには以下が含まれます。

フェーズ意味論: 証明可能性に焦点を当てた初期モデル。
カテゴリー意味論: 証明を射としてモデル化する代数的枠組み。適切な圏は、連続線形写像を持つ完全分離ボルノロジーベクトル空間の部分圏である。^[¹²^]
ゲーム意味論: 数式をゲーム、証明を戦略として解釈するインタラクティブなモデル。^{[ 13 ]}
指示的意味論: 証明を数学的対象として解釈するモデル。^{[ 14 ]}

線形論理の代数的意味論は、量子論理の代数的意味論である。

言語学では、線形論理モデルは文法解析を演繹としてモデル化する。この場合、有効な構文木は、文法を符号化する含意規則を使用して文の存在を証明することに対応する。^{[ 15 ]}

資源の解釈

ラフォン（1993）は、直観主義線形論理がリソースの論理として説明できることを初めて示し、古典論理のように非論理的な述語や関係を用いるのではなく、論理自体の中でリソースについて推論するために使用できる形式体系を論理言語に提供しました。トニー・ホーア（1985）は、自動販売機での購入を例に論理を説明し、料理の取引は、接続詞の使用を説明する伝統的な例となっています。^[¹⁶^]

特に、定額メニューは価格から食事への線形的な関係に対応します。

（現金）⊸（食事）

または同等に

（現金）^⊥ ⅋（食事）

含意またはパラグラフを原始的な結合子とするかどうかによって異なります。次に、購入した食事には必ず両方が含まれるため、異なるコースはテンソルを使用して結合されます。たとえば、(食事) を次のように定義できます。

（食事） := （前菜）⊗ （メイン）⊗ （デザート）⊗ （飲み物）

顧客の選択肢は& :を使用して結合されます

（前菜） :=（スープ）＆（サラダ）

これは、顧客がスープかサラダのどちらかを選ばなければならないことを示しています。逆に、レストランの選択は⊕を使用して分離されます。デザートが季節の果物である場合、それは次のようにモデル化できます。

（デザート） := （夏のベリー）⊕ （リンゴのスライス）⊕ （冬のパイナップル）⊕ （チェリー）

最後に、食べ放題/飲み放題のアイテムは !: ^{[ 16 ]でモデル化されます。}

（飲み物） := （コーヒー）＆（紅茶）＆ !（水道水）

リソース解釈では、定数 1 はリソースの不在を表し、⊗ の単位として機能します (任意の式 $Aは$ $A \otimes 1$ と同等です)。⊤ は&の単位であり、不要なリソースを消費します。0 は製造できない製品を表し、⊕ の単位として機能します ( $A$ または $0を生成する可能性のある機械は、0 を生成することに成功しないため、常に$ $A を$ 生成する機械と同じです)。⊥ は消費できないリソースを表します。^{[ 17 ]}

決定可能性／含意の複雑性

完全な CLL における含意関係は決定不能である。[ 18 ] ^CLLの断片を考慮すると、決定問題の複雑さは変化する。

乗法線形論理 (MLL): 乗法結合子のみ。MLL の含意は、純粋に含意的な断片のホーン節に限定した場合でも、NP 完全である^[¹⁹^]または原子を含まない式に限定した場合でも^[²⁰^{] 。}
乗法加法線形論理 (MALL): 乗法と加法のみ (つまり、指数関数を含まない)。MALL の含意はPSPACE 完全である。^{[ 18 ]}
乗法指数線形論理 (MELL): 乗法と指数のみ。ペトリネットの到達可能性問題からの還元により、^{[ 21 ]} MELL の含意は少なくともEXPSPACE 困難でなければならないが、決定可能性自体は長年未解決の問題であった。2015 年に、Theoretical Computer Science誌に決定可能性の証明が掲載されたが、^{[ 22 ]}後に誤りであることが示された。^{[ 23 ]}
アフィン線形論理（つまり、弱化を伴う線形論理、断片ではなく拡張）は、1995年に決定可能であることが示された。^{[ 24 ]}

バリエーション

線形論理の多くのバリエーションは、構造規則をさらに微調整することによって生じる。

アフィン論理は、縮約を禁じるが、大域的弱化（決定可能な拡張）は許容する。
厳密論理または関連性論理は、弱化を禁じるが、全体的な収縮は許容する。
非可換論理、または順序論理は、交換規則を排除するだけでなく、弱化と収縮も禁止する。順序論理では、線形含意はさらに左含意と右含意に分けられる。

直観主義的な線形論理のさまざまな変種が検討されてきた。ILL（直観主義線形論理）のように、単一結論シーケント計算表現に基づく場合、結合子⅋、⊥、および ?は存在せず、線形含意は原始的な結合子として扱われる。FILL（完全直観主義線形論理）では、結合子⅋、⊥、および ?が存在し、線形含意は原始的な結合子であり、直観主義論理と同様に、すべての結合子（線形否定を除く）は独立している。線形論理には、形式的な展開がある程度標準化されている一階および高階拡張も存在する（一階論理および高階論理を参照）。

注記

↑ジラール 1987。
↑ Baez & Stay 2008 .
↑デ・パイバ、ヴァン・ジェナビス、リッター、1999 年。
1 2 Paoli, Francesco (2002). "部分構造論理入門" . Trends in Logic . 13 : 42. doi : 10.1007/978-94-017-3179-9 . ISBN 978-90-481-6014-3ISSN 1572-6126
1 2 Jean-Yves, Girard. "線形論理: その構文と意味論" (PDF) .線形論理: その構文と意味論: 42.
↑ Troelstra, AS (Anne Sjerp) (1992).線形論理に関する講義. インターネットアーカイブ. スタンフォード、カリフォルニア州: 言語情報研究センター. ISBN 978-0-937073-78-0。
↑レスタル、グレッグ（2000）。『部分構造論理入門』サイコロジー・プレス。ISBN 978-0-415-21534-3。
↑ジラール 1987、p.22、定義1.15。
↑ジラール 1987、p.25-26、定義1.21。
↑コケット＆シーリー 1997。
↑ディ・コスモ 1996 .
↑ブルート、リチャード。エアハルト、トーマス。タッソン、クリスティーン（2011年1月13日）。「便利な微分カテゴリ」(PDF)。{{cite journal}}:ジャーナルを引用するには|journal=（ヘルプ）
↑ Andreas Blass: 「線形論理のためのゲーム意味論」、 Annals of Pure and Applied Logic、第56巻183～ 220ページ。
↑ディ・コスモ、ロベルト；ミラー、デール（2023）「線形論理」、ザルタ、エドワード・N；ノーデルマン、ウリ（編）『スタンフォード哲学百科事典』（2023年秋版）、形而上学研究室、スタンフォード大学、 2025年9月20日取得
↑ Crouch, Dick; van Genabith, Josef (2000年6月20日). "Linear Logic for Linguists" (PDF) . p. 8.
1 2 Crouch & van Genabith 2000、p. 15。
↑ Crouch & van Genabith 2000、pp. 60–61。
1 2この結果および以下の断片の一部についての議論については、 Lincoln et al. (1992)を参照してください。
↑カノヴィッチ 1992。
↑リンカーン＆ウィンクラー 1994。
↑グンター＆ゲロット 1989。
↑ビンボ 2015。
↑ Straßburger 2019 .
↑コピロフ 1995。

参考文献

Baez, John ; Stay, Mike (2008). Bob Coecke (編). "Physics, Topology, Logic and Computation: A Rosetta Stone" (PDF) . New Structures of Physics .
Bimbó, Katalin (2015年9月13日). 「古典線形論理の内包的断片の決定可能性」 . Theoretical Computer Science . 597 : 1–17 . doi : 10.1016/j.tcs.2015.06.019 . ISSN 0304-3975 .
Cockett, J. Robin ; Seely, Robert (1997). "Weakly distributive categories". Journal of Pure and Applied Algebra . 114 (2): 133– 173. doi : 10.1016/0022-4049(95)00160-3 .
ディ・コスモ、ロベルト（1996）。「2」。線形論理入門（講義ノート）。
デ・パイバ、V. ;ヴァン・ジェナビス、J.リッター、E. (1999)。「線形論理とアプリケーションに関する Dagstuhl セミナー 99341」(PDF)。Drops-Idn/V2/Document/10.4230/Dagsemrep.248。 Schloss Dagstuhl – Leibniz-Zentrum für Informatik: 1–21 . doi : 10.4230/DagSemRep.248。
Girard, Jean-Yves (1987). "線形論理" (PDF) . Theoretical Computer Science . 50 (1): 1– 102. doi : 10.1016/0304-3975(87)90045-4 . hdl : 10338.dmlcz/120513 .
Gunter, CA; Gehlot, V. (1989). Nets as Tensor Theories (PDF) (技術報告書). ペンシルベニア大学. MS-CIS-89-68.
Kanovich, Max I. (1992年6月22日). 「線形論理におけるホーンプログラミングはNP完全である」.第7回IEEEコンピュータサイエンスにおける論理シンポジウム、1992年。LICS '92。議事録。第7回IEEEコンピュータサイエンスにおける論理シンポジウム、1992 年。LICS '92。議事録。pp. 200–210。doi : 10.1109 / LICS.1992.185533。ISBN 0-8186-2735-2。
Kopylov, AP (1995年6月1日). 「線形アフィン論理の決定可能性」.第10回IEEEコンピュータサイエンスにおける論理シンポジウム、1995年。LICS '95。議事録。第10回IEEEコンピュータサイエンスにおける論理シンポジウム、1995年。LICS '95 。議事録。pp . 496–504。CiteSeerX 10.1.1.23.9226。doi : 10.1109/LICS.1995.523283。ISBN 0-8186-7050-9。
Lincoln, Patrick; Mitchell, John; Scedrov, Andre; Shankar, Natarajan (1992). "命題線形論理の決定問題" . Annals of Pure and Applied Logic . 56 ( 1–3 ): 239–311 . doi : 10.1016/0168-0072(92)90075-B .
Lincoln, Patrick; Winkler, Timothy (1994). "定数のみの乗法線形論理はNP完全である" . Theoretical Computer Science . 135 : 155–169 . doi : 10.1016/0304-3975(94)00108-1 .
Straßburger, Lutz (2019年5月10日). 「MELLの決定問題について」 . Theoretical Computer Science . 768 : 91–98 . doi : 10.1016/j.tcs.2019.02.022 . ISSN 0304-3975 .

さらに読む

n ラボにおける線形論理
Braüner, Torben (1996 年 12 月)。「線形論理入門」(PDF)。BRICS 講義シリーズ。コンピュータ科学の基礎研究 (BRICS) 。2025年5 月 20 日取得。
ディ・コスモ、ロベルト。ダノス、ヴィンセント (1992)。線形ロジック入門書。
ディ・コスモ、ロベルト、ミラー、デール（2023年9月16日）。「線形論理」。ザルタ、エドワード・N（編）。スタンフォード哲学百科事典（2023年秋版）。ISSN 1095-5054。OCLC 429049174。
ジラール、ジャン＝イヴ；ラフォン、イヴ；テイラー、ポール（1989）。証明と型。ケンブリッジ大学出版局。 2016年7月4日時点のオリジナルよりアーカイブ。
Hoare, CAR (1985). Communicating Sequential Processes . Prentice-Hall International. ISBN 0-13-153271-5。
ラフォン、イヴ（1993）。「線形論理入門」。TEMPUSコンピュータサイエンスにおける代数的および圏論的手法に関するサマースクール（講義ノート）。チェコ共和国、ブルノ。
リンカーン、パトリック。「線形論理入門」（ポストスクリプト）。
ミラー、デール（2004）。「線形論理プログラミングの概要」。Ehrhard、Girard、Ruet、Scott（編）『コンピュータサイエンスにおける線形論理（PDF）』所収。ロンドン数学会講義ノート、第 316巻。ケンブリッジ大学出版局。
Troelstra, AS (1992).線形論理に関する講義. CSLI 講義ノート. 第 29 巻. スタンフォード: CSLI 出版. ISBN 978-0937073773。
Troelstra, AS ; Schwichtenberg, H. (2000) [1996]. Basic Proof Theory . Cambridge Tracts in Theoretical Computer Science. Vol. 43 (2nd ed.). Cambridge: Cambridge University Press. pp. XII, 417. doi : 10.1017/CBO9781139168717 . ISBN 9780521779111OCLC 951181823
ワドラー、フィリップ。「線形論理の味」。

外部リンク

ウィキメディア・コモンズにある線形論理に関連するメディア
線形論理証明器 (llprover) 2016年4月4日にWayback Machineにアーカイブされ、オンラインで使用可能。作成者: 田村直之 / 神戸大学コンピュータサイエンス学科 / 日本
クリック＆コレクト方式の対話型線形論理証明器（オンラインで利用可能）
ロペス、アデル（2020年6月7日）。「ビジュアル・リニア・ロジック」。 —線形論理における命題と演繹のための視覚的計算

[FOOTNOTEGirard1987-1] ジラール 1987。

[FOOTNOTEBaezStay2008-2] Baez & Stay 2008 .

[FOOTNOTEDe_PaivaVan_GenabithRitter1999-3] デ・パイバ、ヴァン・ジェナビス、リッター、1999 年。

[:0-4] 1 2 Paoli, Francesco (2002). "部分構造論理入門" . Trends in Logic . 13 : 42. doi : 10.1007/978-94-017-3179-9 . ISBN 978-90-481-6014-3ISSN 1572-6126

[:1-5] 1 2 Jean-Yves, Girard. "線形論理: その構文と意味論" (PDF) .線形論理: その構文と意味論: 42.

[6] Troelstra, AS (Anne Sjerp) (1992).線形論理に関する講義. インターネットアーカイブ. スタンフォード、カリフォルニア州: 言語情報研究センター. ISBN 978-0-937073-78-0。

[7] レスタル、グレッグ（2000）。『部分構造論理入門』サイコロジー・プレス。ISBN 978-0-415-21534-3。

[FOOTNOTEGirard1987p.22,_Def.1.15-8] ジラール 1987、p.22、定義1.15。

[FOOTNOTEGirard1987p.25-26,_Def.1.21-9] ジラール 1987、p.25-26、定義1.21。

[FOOTNOTECockettSeely1997-10] コケット＆シーリー 1997。

[FOOTNOTEDi_Cosmo1996-11] ディ・コスモ 1996 .

[12] ブルート、リチャード。エアハルト、トーマス。タッソン、クリスティーン（2011年1月13日）。「便利な微分カテゴリ」(PDF)。{{cite journal}}:ジャーナルを引用するには|journal=（ヘルプ）

[13] Andreas Blass: 「線形論理のためのゲーム意味論」、 Annals of Pure and Applied Logic、第56巻183～ 220ページ。

[14] ディ・コスモ、ロベルト；ミラー、デール（2023）「線形論理」、ザルタ、エドワード・N；ノーデルマン、ウリ（編）『スタンフォード哲学百科事典』（2023年秋版）、形而上学研究室、スタンフォード大学、 2025年9月20日取得

[15] Crouch, Dick; van Genabith, Josef (2000年6月20日). "Linear Logic for Linguists" (PDF) . p. 8.

[FOOTNOTECrouchvan_Genabith200015-16] 1 2 Crouch & van Genabith 2000、p. 15。

[FOOTNOTECrouchvan_Genabith200060–61-17] Crouch & van Genabith 2000、pp. 60–61。

[Lincoln+92-18] 1 2この結果および以下の断片の一部についての議論については、 Lincoln et al. (1992)を参照してください。

[FOOTNOTEKanovich1992-19] カノヴィッチ 1992。

[FOOTNOTELincolnWinkler1994-20] リンカーン＆ウィンクラー 1994。

[FOOTNOTEGunterGehlot1989-21] グンター＆ゲロット 1989。

[FOOTNOTEBimbó2015-22] ビンボ 2015。

[FOOTNOTEStraßburger2019-23] Straßburger 2019 .

[FOOTNOTEKopylov1995-24] コピロフ 1995。

[

[

3

[ 8 ]

[ 9 ]

[ 10 ]

[ 11 ]

[

[ 13 ]

[ 14 ]

[ 15 ]

[

[ 17 ]

CLLの断片

[

[

[ 21 ]

[ 22 ]

[ 23 ]

[ 24 ]