自動定理発見問題は自動定理発見の一般的な方法を求めるという問題である。自動定理発見問題を解決するために強相関論理に基づく前向き推論を用いた自動定理発見法が提案された。提案手法に基づき、公理的集合論の一種である NBG 集合論による自動定理発見の試行が行われ、いくつかの既知の定理を再発見することができた。再発見とは提案手法で既知の定理が導出されることである。一方、提案手法で再発見できていない既知の定理があり、それらの既知の定理を再発見するために提案手法を改善する必要がある。そこで本研究では項書き換え処理を自動定理発見手法に実装を行った。そして新たに既知の定理の再発見を行うことができた。