自動定理証明
一階述語論理の定理証明は自動定理証明の中でも最も研究が進んでいる。この論理は適度に自然で直感的な方法で様々な問題を記述できる程度に表現豊かである。一方、半決定的で健全で完全な計算方法が開発されており、完全自動システムを構築することが可能である。さらに表現力のある論理(高階述語論理や様相論理)は、さらに様々な問題を記述可能だが、それらの定理証明は一階述語論理ほど開発が進んでいない。
定理証明とそれ以外の区別の観点として、公理から出発して推論規則に従って推論を行い、いわゆる証明を行うものを定理証明と呼ぶ。モデル検査などのそれ以外の技術では、考えられる全ての状態を列挙するようなものである(モデル検査の実装ではもう少し賢さが必要であるが、それで力づくの手法でなくなるわけではない)。
モデル検査的手法を推論規則として利用するハイブリッド型の定理証明システムも存在する。また、特定の定理を証明するために書かれたプログラムも存在し、プログラムがある結果を返して終了したときに定理が真であることが証明される。そのようなプログラムの好例として四色定理の計算機支援証明がある。人間の手では証明できなかった問題を証明したことで物議をかもしたそのプログラムは、非常に複雑で検証不可能と言われた。他の例として重力付き四目並べゲームで先手が必ず勝つことを証明したことが挙げられる。