自動定理証明

自動定理証明（Automated Theorem Proving、ATP）とは、自動推論(AR) の中でも最も成功している分野であり、コンピュータプログラムによって数学的定理を証明すること。ベースとなる論理によって、定理の妥当性を決定する問題は簡単なものから不可能なものまで様々である。