類推における証明項の変換について
スポンサーリンク
概要
- 論文の詳細を見る
類推の枠組みを、置き換え規則の自然な拡張である文脈スキーマによって定式化する。類推の帰結は一般には一意に定まらず、これは類推の観点(類似性のとらえ方)に依存すると考え、スキーマにおける制約で表現する。また、文脈で類推において保存される部分(2つの対象間で同型対応の部分)を表す。制約を論理的帰結にとり、定理証明の問題において、論理式間の類似性をそのスキーマとのパターンマッチング可能性で定義する。類推を用いて証明をする際に証明可能性を保持しながら、証明したい論理式を単純な論理式に分解して既に得られている証明を再利用する。さらに、カリー・ハワード同型により類推による定理証明が証明項の変換として定式化され、論理式間の類似性を表現しているスキーマによって、この変換規則(類推)を得ることができる。
- 社団法人電子情報通信学会の論文
- 1994-07-07
著者
関連論文
- λμ計算のモデルについて
- 構成的プログラミング
- 古典的証明に基づく関数型言語の構築
- 古典的証明に基づく値呼びプログラミング言語の型推論アルゴリズムについて
- An Injective CPS-translation for the Extensional λ-calculus
- 安全な動的型と分散プロクラミング
- 部分型推論の困難さに関する一考察
- Domain-Free $\lambda\mu$-Calculus for Polymorphism and Call-by-Value (Languages, Algebra and Computer Systems)
- μ-Head Form Proofs with at Most Two Formulas in the Succedent
- μ冠頭形証明とそのプログラミングへの応用に関する一考察
- Martin-Lofの型理論に基づくプログラム支援システムの構築
- 類推における証明項の変換について
- Bengt Nordstrom, Kent Petersson and Jan M. Smith : Programming in Martin-Lof's Type Theory, An Introduction, Clarendon Press (1990). ISBN 0-19-853814-6
- Parallel Computation and Synchronized Term Rewriting Systems : Extended Abstract (Algebraic Semigroups, Formal Languages and Computation)
- $\gamma$-Calculus with Lazy Lists : Extended abstract (Algorithms in Algebraic Systems and Computation Theory)
- Multiple-Conclusion System as Communication Calculus : Informal meaning of proofs as communication terms (Algebraic Systems, Formal Languages and Computations)