方程式証明器
EQP（方程式証明器）は、アルゴンヌ国立研究所の数学・コンピュータサイエンス部門によって開発された、方程式論理の定理を自動証明するプログラムです。これは、ハーバート・ロビンズが提起した長年の問題、「すべてのロビンズ代数はブール代数であるかどうか」を解くために使用された証明器の一つでした。EQPの簡略化された証明は、後にベルント・ダーンによって公開されました。[1]
参考文献
外部リンク
- EQP プロジェクト。
- ロビンズ代数はブール代数です。
- アルゴンヌ国立研究所、数学およびコンピューター科学部門。
