2025-11-23T13:43:17.173951

Admissibility of Substitution Rule in Cyclic-Proof Systems

Saotome, Nakazawa
This paper investigates the admissibility of the substitution rule in cyclic-proof systems. The substitution rule complicates theoretical case analysis and increases computational cost in proof search since every sequent can be a conclusion of an instance of the substitution rule; hence, admissibility is desirable on both fronts. While admissibility is often shown by local proof transformations in non-cyclic systems, such transformations may disrupt cyclic structure and do not readily apply. Prior remarks suggested that the substitution rule is likely nonadmissible in the cyclic-proof system CLKID^omega for first-order logic with inductive predicates. In this paper, we prove admissibility in CLKID^omega, assuming the presence of the cut rule. Our approach unfolds a cyclic proof into an infinitary form, lifts the substitution rules, and places back edges to construct a cyclic proof without the substitution rule. If we restrict substitutions to exclude function symbols, the result extends to a broader class of systems, including cut-free CLKID^omega and cyclic-proof systems for the separation logic.
academic

循環証明システムにおける置換規則の許容性

基本情報

  • 論文ID: 2510.14749
  • タイトル: Admissibility of Substitution Rule in Cyclic-Proof Systems
  • 著者: 佐音賢二、中澤浩二（名古屋大学）
  • 分類: cs.LO（論理学）
  • 発表日: 2025年10月16日
  • 論文リンク: https://arxiv.org/abs/2510.14749

要旨

本論文は循環証明システムにおける置換規則の許容性問題を研究する。置換規則は理論分析を複雑化させ、証明探索の計算コストを増加させる。なぜなら、各シーケントが置換規則インスタンスの結論となる可能性があるためである。したがって、許容性は理論的にも実践的にも望ましい。非循環システムでは、許容性は通常局所的な証明変換によって証明されるが、このような変換は循環構造を破壊する可能性があり、直接適用することはできない。先行研究は、置換規則が帰納述語を伴う一階論理循環証明システムCLKIDωにおいて許容でない可能性が高いことを示唆している。本論文は、カット規則が存在する場合、CLKIDωにおける置換規則が許容であることを証明する。我々のアプローチは、循環証明を無限形式に展開し、置換規則を持ち上げ、その後辺を戻して置換規則を含まない循環証明を構築することである。置換が関数記号を導入しないという制限の下では、この結果は、カット無しのCLKIDωおよび分離論理の循環証明システムを含む、より広いシステムのクラスに拡張できる。

研究背景と動機

問題定義

循環証明は従来の証明木の拡張であり、循環構造を導入することで帰納的に定義された述語について推論する。置換規則 Γ⊢ΔΓ[θ]⊢Δ[θ]\frac{\Gamma \vdash \Delta}{\Gamma[\theta] \vdash \Delta[\theta]} (Subst) は多くの循環証明システムに導入され、循環構造の構築を支援するために使用される。

問題の重要性

  1. 理論的観点：置換規則は常に適用可能であり、証明分析を複雑にする
  2. 実践的観点：無制限に置換規則を適用すると、各ステップで多くの置換が適用可能であるため、計算コストが増加する

既存方法の限界

非循環証明システムでは、置換規則の許容性は通常2つの段階で実現される：

  1. 持ち上げ段階：置換規則を上方に移動
  2. 消去段階：公理で置換規則を消去

しかし循環証明システムでは、この方法は根本的な困難に直面する：

  • 持ち上げ段階は芽-伴侶関係（bud-companion relationship）を破壊する可能性がある
  • 消去段階は芽で置換規則を消去できない

研究動機

Brotherston 1 はCLKIDωにおいて置換規則が許容であるかどうかという問題を提起し、少なくともカット無し設定では、一般的には許容でない可能性が高いことを示唆している。本論文はこの未解決問題を解決することを目指している。

核心的貢献

  1. 主要な理論的結果：カット規則が存在する場合、CLKIDωにおける置換規則が許容であることを証明
  2. 拡張結果：置換を原子置換（正項数関数記号を導入しない）に限定する場合、結果はカット無しCLKIDωに拡張される
  3. 応用の一般化：この結果は分離論理の循環証明システムなど他の証明システムに適用可能
  4. 新規方法：無限展開、置換の持ち上げ、循環再構成による3段階消去戦略を提案

方法の詳細

タスク定義

CLKIDωにおける置換規則を含む証明Pr+が与えられたとき、同じシーケントを証明する置換規則を含まない証明Pr-を構築する。

コア方法アーキテクチャ

本論文の消去プロセスは2つの主要段階に分かれている：

1. 複合置換の消去

定義：

  • 原子置換：変数と定数のみを含む置換
  • 複合置換：正項数関数記号を含む項を含む置換

方法：以下の変換を通じて複合置換を消去：

Γ ⊢ Δ
────────────────────────── (Subst)
Γ[x₁:=t₁,...,xₙ:=tₙ] ⊢ Δ[x₁:=t₁,...,xₙ:=tₙ]

カット規則、等式規則、存在量化子規則の組み合わせを使用する変換に変換し、最終的に原子置換のみを保持する。

2. 原子置換の消去

これはコアイノベーションであり、3つのステップを含む：

ステップ1：循環展開

  • 循環証明Pr_var+を無限証明Pr^ωに展開
  • マッピングf^ω：Seq(Pr^ω) → Seq(Pr_var+)を定義してシーケント出現を関連付ける

ステップ2：置換の持ち上げ

  • 深さdで置換規則を含まないLKIDω証明Pr^ω_dを再帰的に構築
  • 置換適用性質（substitution-application property）を使用

ステップ3：循環再構成

  • Pr^ω_dからCLKIDω前証明Pr-を構築
  • 芽と伴侶を選択し、グローバルトレース条件を確保

技術的イノベーション

1. 部分置換閉包（Partial-substitution Closure）

定義10：置換集合Θと変数集合Xが与えられたとき、部分置換閉包Cps(Θ,X)は以下の条件を満たす最小集合である：

  • Θ ⊆ Cps(Θ,X)
  • θ∈Cps(Θ,X)およびx,y∈Xに対して：θx→y ∈ Cps(Θ,X)
  • θ₁,θ₂∈Cps(Θ,X)に対して：θ₁θ₂ ∈ Cps(Θ,X)

重要性質：原子置換に限定する場合、部分置換閉包は有限である。

2. 置換適用性質（Substitution-application Property）

定義11：規則(R)が置換適用性質を満たすのは、任意の規則インスタンスと原子置換θに対して、対応する置換適用インスタンスが存在し、トレースを保持する場合である。

補題4：CLKIDωおよびLKIDωは置換適用性質を満たす。

3. グローバルトレース条件の保持

対応パスの概念を通じて、再構成された証明がグローバルトレース条件を満たすことを確保：

定義12：Pr-のパス(eᵢ)に対して、Pr_var+における対応パス(e'ⱼ)を定義し、各無限進行トレースが保持されるようにする。

実験設定

本論文は純粋な理論研究であり、従来の意味での実験はない。検証は以下の方法で行われる：

理論的検証

  1. 構成的証明：明示的なアルゴリズム構成を通じて許容性を証明
  2. 反例分析：制限条件下で許容性を満たさない場合を分析
  3. システム拡張：他のシステムでの結果の適用可能性を検証

例示分析

論文は具体的な証明変換例を提供：

  • 図1：置換規則を含む循環証明
  • 図3：展開後の無限証明
  • N(x) ⊢ E(x)∨O(x)の循環証明から置換規則を消去する方法を示す

実験結果

主要な理論的結果

定理2（CLKIDωにおける置換規則の許容性）： Γ ⊢ ΔがCLKIDωで証明可能ならば、(Subst)を含まないCLKIDωでも証明可能である。

定理3（原子置換の強結果）： PrがCLKIDωにおけるΓ ⊢ Δの証明であり、Θ(Pr)が原子置換のみを含む場合、(Subst)を含まない証明が存在し、Prに出現する規則のみを含む。

拡張結果

定理4（カット無しシステムにおける許容性）： CLKIDω^-（カット無しCLKIDω）において、原子置換規則は許容である。

定理5（分離論理への応用）： 置換規則はCSLωおよびCSLω^-の両方で許容である。

理論的発見

  1. カット規則の重要な役割：複合置換の消去にはカット規則が必要
  2. 原子置換の普遍性：原子置換の消去はより広いシステムのクラスに適用可能
  3. 関数記号の制限性：関数記号の存在は許容性の重要な障害

関連研究

主要な研究方向

  1. 循環証明理論：Brotherstonら1,4,6の先駆的研究
  2. 証明探索：ヒューリスティック帰納仮説探索を回避する研究2,3,5,11,12
  3. 分離論理：分離論理における循環証明の応用2,7,9

本論文と関連研究の関係

  • Brotherston 1が提起した未解決問題を解決
  • Kimuraら7の研究をより一般的な設定に拡張
  • 証明探索に理論的基礎を提供

本論文の利点

  1. 初の証明：CLKIDωにおける置換規則の許容性を初めて厳密に証明
  2. 方法的イノベーション：循環構造に適用可能な新しい消去技術を提案
  3. 広い適用性：複数の関連システムに適用可能な結果

結論と考察

主要な結論

  1. カット規則が存在するCLKIDωにおいて、置換規則は許容である
  2. 原子置換に限定する場合、結果はカット無しシステムに拡張される
  3. この結果は分離論理など他の重要なシステムに適用可能

制限事項

  1. カット規則への依存：複合置換の消去にはカット規則が必要
  2. 関数記号の制限：完全に一般的な結果には関数記号の排除が必要
  3. 構成の複雑性：証明構成プロセスは相対的に複雑

今後の方向性

  1. 最小規則集合：関数記号が存在する場合でも置換規則消去を許可する最小規則集合の研究
  2. カット消去：追加規則の導入を通じた循環証明システムのカット消去性質の研究
  3. 計算複雑性：置換規則消去の計算複雑性の分析

深い評価

利点

  1. 理論的重要性：この分野の重要な未解決問題を解決
  2. 方法的イノベーション：循環構造に適用可能な新技術を提案
  3. 厳密性：証明は厳密かつ構成的
  4. 広い適用性：複数の関連システムに適用可能な結果
  5. 明確な表述：技術的詳細は明確に表述され、理解しやすい

不足点

  1. 実用性の制限：カット規則への依存が実際の応用を制限
  2. 複雑性：証明変換プロセスは相対的に複雑
  3. 完全性：カット無し設定ではまだ制限がある

影響力

  1. 理論的貢献：循環証明理論に重要な理論的基礎を提供
  2. 実用的価値：証明探索実装にさらなる柔軟性を提供
  3. 拡張可能性：方法は他の関連システムに適用可能である可能性

適用シナリオ

  1. 自動定理証明：循環証明探索の効率を向上
  2. プログラム検証：分離論理などの検証フレームワークでの応用
  3. 理論研究：循環証明理論のさらなる研究の基礎を提供

参考文献

論文は19篇の関連文献を引用しており、主に以下を含む：

  1. Brotherstonの循環証明に関する先駆的研究
  2. 分離論理における循環証明応用の研究
  3. 自動証明探索に関する関連研究
  4. カット消去と証明論の基礎研究

本論文は循環証明理論において重要な貢献を行い、革新的な技術手段を通じて重要な未解決問題を解決し、この分野のさらなる発展の基礎を築いている。