数学的構造を反映させた定理証明系の試み

スポンサーリンク

概要

論文の詳細を見る
既存の証明論に基づいて構築された自動証明系は,一般に大きな知識ベースを必用とし,また式が大きくなるに連れて組み合わせ論的な爆発により手に負えなくなりやすい。実際の理論はある種の領域を意識して作られており,多くの場合ある種の群,環,束など構造のはっきりわかっているより抽象的な構造と同型や準同型で関係付けられている。この同型,準同型に付随して,1つの領域上の元,関数,関係を他の領域上で表現する表現定理がある。実際の数学的思考に際しては,この表現定理を使ってよりやさしい領域に移して問題を考えることが多い。ここでは,理論ごとにこの表現定理をメタ知識として用意しておき,よりやさしい理論の上に翻訳して問題を解き,元に戻すという方法を組み込んだ自動証明系を紹介し,この方法の有効性を述べる。
1988-09-12

著者

関連論文

もっと見る

スポンサーリンク