構成的数学体系RPTに基づく超数学の定理の形式化
スポンサーリンク
概要
- 論文の詳細を見る
我々の目的は、洗錬された論理体系に基づき、数学の定理やプログラムの性質の証明を計算機上で実行できる環境を構築し、ひとつのシステムの中で、定理証明やプログラムの合成、変換等を行うことである。ここで、基礎とする論理体系は構成的(直観主義的)なので、証明された定理に含まれるアルゴリズムを、プログラムの形で自動的に抽出することができる。従って、このシステムの中では、証明の作成作業はプログラミングと同一視できることになる。構成的数学の体系は、近年、プログラムのための論理として活発に研究されており、計算機上の実現の例も、Maztin-Lofの型理論に基づいたConstableらのNuprl[1]や、FefermanのT0に基づいた林のPX[2]などがある。また、我々も、上記の目的のために、体系SSTと関数型言語Aを用いたシステムを提案している[3]。本研究の主な特徴は、・論理体系に含まれるプログラム言語を用いて、証明システムを実現したため、システムの性質をそれ自身の中で論じることができる。・扱う対象は、普通の数学の定理だけでなく、超数学(証明論)の定理を自然に形式化し、証明することを含んでいる。という2点である。これらの騎徴を示す例として、Aの項に対するChuzh=Rosserの定理の証明をあげる。また、その他の超数学の定理の形式化について簡単にのべる。
- 一般社団法人情報処理学会の論文
- 1991-02-25
著者
関連論文
- 二階文脈計算(プログラミング及びプログラミング言語)
- 定理証明システムCoq上でのPre Logical Relationを用いた詳細化の正しさの証明
- 自己反映的証明体系RPTの理論と実現
- 抽象化と精密化による実時間モデル検査の改善
- 多値モデル検査を利用したモデル化の誤りの発見
- 限定継続に基づくスケーラブルなウェブアプリケーション構築手法
- 1Q-5 マルチステージプログラミングのための計算体系の実装(プログラミング言語・実装・支援,学生セッション,ソフトウェア科学・工学)
- 動的環境と限定継続を持つプログラム言語の意味論と実装
- オブジェクト指向言語に対するメタプログラミング言語の設計と実装
- 階層化コントロールオペレータに対する型システムの構築
- 構成的数学体系RPTに基づく超数学の定理の形式化
- 日本ネットワークインフォメーションセンターJNICの活動(学術コンピュータネットワーク)
- 学術研究大学間ネットワークJAIN(学術コンピュータネットワーク)
- 結果型を変更可能な限定継続の模倣