等式証明器

EQP ( Equational prover ) は、アルゴンヌ国立研究所の数学およびコンピュータサイエンス部門によって開発された、等式論理の定理を自動証明するプログラムです。これは、ハーバート・ロビンズが提起した長年の問題、つまり、すべてのロビンズ代数はブール代数であるかどうかという問題を解決するために使用された証明器の 1つでした。

• EQPプロジェクト。
• ロビンズ代数はブール代数です。
• アルゴンヌ国立研究所、数学およびコンピューター科学部門。