直観主義線形論理のためのスコーレム化

Centrala begrepp

本論文では、焦点化された直観主義線形論理(LJF)のための新しいスコーレム化手順を提案し、その手順が正しく完全であることを示す。これにより、量化子の順序を解決する際のバックトラックが排除される。

Sammanfattning

本論文は、直観主義線形論理(LJF)のためのスコーレム化手順を提案している。

まず、スコーレム化された直観主義線形論理(SLJF)を定義する。SLJFでは、量化子ルールの適用順序に関する制約を明示的な置換として表現する。これにより、LJFでの量化子レベルのバックトラックを回避できる。

スコーレム化手順は、LJFの導出をSLJFの導出に変換する。この変換は正しく完全である。つまり、LJFの導出はSLJFの導出に変換できるし、逆も成り立つ。

具体的には以下の手順を経る:

1. LJFの判断式Γ; Δ⊢Fを、Γ', Δ', Fの各々をスコーレム化して(Γ'; σΓ'), (Δ'; σΔ'), (K; σK)を得る。
2. 置換τ = σΓ', σΔ', σKを定義する。
3. 正の文脈Γ'と線形文脈Δ'から、neg(Γ'); Δ' ⊢K; σ, τ, σ'が導出できることを示す。

この結果、LJFの導出をSLJFの導出に変換できることが分かる。一方、SLJFの導出からLJFの導出を再構築できることも示される。

Statistik

量化子ルールの適用順序に関する制約は、明示的な置換として表現される。
置換σは、導出の再構築時に満たすべき条件(admissibility)を持つ。

Citat

"焦点化は、導出の数を減らしつつ導出可能性を保つ既知の手法である。"
"スコーレム化は、バックトラックの数を減らすことで証明探索を改善する別の手法である。"
"直観主義線形論理のための実用的なスコーレム化手順は、これまで明らかではなかった。"

Viktiga insikter från

Skolemisation for Intuitionistic Linear Logic

by Ales... på arxiv.org 05-03-2024

https://arxiv.org/pdf/2405.01375.pdf

Djupare frågor

直観主義線形論理以外の論理体系(古典論理、モーダル論理など)でもスコーレム化が可能か検討する必要がある。

スコーレム化は、直観主義線形論理に限らず、古典論理やモーダル論理など他の論理体系でも適用可能です。スコーレム化は、証明探索における量化子の順序に関する制約を明示的に表現する手法であり、これらの制約が存在する限り、他の論理体系でもスコーレム化を利用してバックトラックを回避することができます。ただし、各論理体系の特性やルールに合わせてスコーレム化手法を適切に適用する必要があります。