EQP とは

Equational Proverの略語であるEQPは、Argonne National Laboratoryの数学およびコンピュータサイエンス部門によって開発された等式論理のための自動定理証明プログラムです。これは、Herbert Robbinsによって提起された長年にわたる問題、すなわちすべてのRobbins代数がブール代数であるかどうかを解決するために使用された証明者の1人でした。