自動定理証明(英: automated theorem proving、ATP)とは、自動推論(AR) の中でも最も成功している分野であり、コンピュータプログラムによって数学的定理に対する証明を発見すること。ベースとなる論理によって、定理の妥当性を決定する問題は簡単なものから不可能なものまで様々である。
This content in DBpedia Japanese is extracted from Wikipedia by DBpedia Community and is licensed under a Creative Commons 表示 - 継承 3.0 非移植 License.