TL;DR
公理から推論規則で新しい命題を導き、定理を証明すること。計算機による定理証明は、ハードウェアやソフトウェアの検証に使われる。
仕組み
Wikipedia によると、計算機による定理証明には 2 つの方式がある。自動定理証明では、プログラムが自分で証明を探す。対話的定理証明では、人が証明支援系（proof assistant）にヒントを与えながら証明を進める。証明支援系には、人が与えた完全な証明を確かめるだけの証明検査器から、作業の大部分を自動化するものまである。難しい問題には、たいてい熟練したユーザが必要になる。
モデル検査は別の方法を取り、最も単純な形では状態を網羅的に列挙して確かめる。モデル検査を推論規則の 1 つとして証明に組み込む仕組みもある。
例
商用では、集積回路の設計と検証に最もよく使われている。ソフトウェアの検証にも早くから使われ、Pascal や Ada のプログラムの正しさを一階述語論理の証明器で確かめた。
注意点
命題論理は決定可能だが co-NP 完全なので、一般には指数時間がかかると考えられている。一階述語論理は半決定可能で、正しい論理式は十分な資源があれば必ず証明できるが、正しくない論理式を常に見分けられるわけではない。