Core Concepts
本論文では、焦点化された直観主義線形論理(LJF)のための新しいスコーレム化手順を提案し、その手順が正しく完全であることを示す。これにより、量化子の順序を解決する際のバックトラックが排除される。
Abstract
本論文は、直観主義線形論理(LJF)のためのスコーレム化手順を提案している。
まず、スコーレム化された直観主義線形論理(SLJF)を定義する。SLJFでは、量化子ルールの適用順序に関する制約を明示的な置換として表現する。これにより、LJFでの量化子レベルのバックトラックを回避できる。
スコーレム化手順は、LJFの導出をSLJFの導出に変換する。この変換は正しく完全である。つまり、LJFの導出はSLJFの導出に変換できるし、逆も成り立つ。
具体的には以下の手順を経る:
- LJFの判断式Γ; Δ⊢Fを、Γ', Δ', Fの各々をスコーレム化して(Γ'; σΓ'), (Δ'; σΔ'), (K; σK)を得る。
- 置換τ = σΓ', σΔ', σKを定義する。
- 正の文脈Γ'と線形文脈Δ'から、neg(Γ'); Δ' ⊢K; σ, τ, σ'が導出できることを示す。
この結果、LJFの導出をSLJFの導出に変換できることが分かる。一方、SLJFの導出からLJFの導出を再構築できることも示される。
Stats
量化子ルールの適用順序に関する制約は、明示的な置換として表現される。
置換σは、導出の再構築時に満たすべき条件(admissibility)を持つ。
Quotes
"焦点化は、導出の数を減らしつつ導出可能性を保つ既知の手法である。"
"スコーレム化は、バックトラックの数を減らすことで証明探索を改善する別の手法である。"
"直観主義線形論理のための実用的なスコーレム化手順は、これまで明らかではなかった。"