自動帰納法を用いた定理証明は、コンピュータサイエンスにおける重要な課題です。本記事では、Isabelle/HOLにおける帰納法による証明の最近の進展をまとめた後、ユナイテッド・リーズニングという新たなアプローチを提案します。このアプローチは、帰納的・演繹的推論を統合し、難解な帰納的問題を自動的に証明することを目指しています。成功すれば、ユナイテッド・リーズニングは三つの推論方法から最良の部分を取り入れ、証明の自動化を一層進めることができます。本研究は、第34回日本人工知能学会年会で発表された短論文のプレプリントです。