情報処理学会 第80回全国大会講演要旨

自動定理発見は計算機に定理を自動的に証明させるのではなく、計算機に未知の定理を自動的に発見させることである。自動定理発見のためのインフラストラクチャとして理論グリッドおよびその理論的基礎が提案された。理論グリッドはさまざまな論理体系に基づく、さまざまな形式理論の部分集合を組織化し、管理する環境である。しかし、理論グリッドは未だ構築されていない。本研究ではデータをWeb上で相互にリンク付けして公開できる仕組みであるLinked Dataを用いた理論グリッドの構築法を提案した。また、公理的集合論の形式理論の部分集合を格納する理論グリッドのプロトタイプを構築した。