自動定理発見問題とは, 自動定理発見の一般的な方法を求めるという問題である.
自動定理発見問題を解決するために強相関論理に基づく前向き推論を用いた自動定理発見の論理的基礎および方法が提案された
(以下, 前向き推論法). 前向き推論法の試行を支援するためにいくつかの支援ツールや手法が提案・開発されている.しかし,
これらの支援ツールや手法は互いに連携しておらず独立しているため, 前向き推論法の試行を簡単に実施できる環境は実現されていなかった.
開発した新たな支援環境を利用することで,
試行にかかる時間が減少し,試行者の負担を減らすことができた.