自動定理証明の目的は、与えられた予想（目標定理）と既知の事実の知識ベースを用いて、形式言語で証明を自動生成することです。この技術は、ソフトウェアやハードウェアシステムの検証や合成など、様々な分野で重要な応用を持っています。