- 著者
-
亀山 幸義
- 雑誌
- 全国大会講演論文集
- 巻号頁・発行日
- vol.42, pp.47-48, 1991-02-25
我々の目的は、洗錬された論理体系に基づき、数学の定理やプログラムの性質の証明を計算機上で実行できる環境を構築し、ひとつのシステムの中で、定理証明やプログラムの合成、変換等を行うことである。ここで、基礎とする論理体系は構成的(直観主義的)なので、証明された定理に含まれるアルゴリズムを、プログラムの形で自動的に抽出することができる。従って、このシステムの中では、証明の作成作業はプログラミングと同一視できることになる。構成的数学の体系は、近年、プログラムのための論理として活発に研究されており、計算機上の実現の例も、Maztin-Lofの型理論に基づいたConstableらのNuprl[1]や、FefermanのT0に基づいた林のPX[2]などがある。また、我々も、上記の目的のために、体系SSTと関数型言語Aを用いたシステムを提案している[3]。本研究の主な特徴は、・論理体系に含まれるプログラム言語を用いて、証明システムを実現したため、システムの性質をそれ自身の中で論じることができる。・扱う対象は、普通の数学の定理だけでなく、超数学(証明論)の定理を自然に形式化し、証明することを含んでいる。という2点である。これらの騎徴を示す例として、Aの項に対するChuzh=Rosserの定理の証明をあげる。また、その他の超数学の定理の形式化について簡単にのべる。