EQP
|
|
EQP, an abbreviation for Equational Prover is an automated theorem-proving program for first-order equational logic, developed by the Mathematics and Computer Science Division (http://www-fp.mcs.anl.gov/division/welcome/default.asp) of the Argonne National Laboratory and among other used for solving the problem proposed by Herbert Robbins whether all Robbins algebras are Boolean, the problem arised from the Huntington's equation from 1933:
- <math> n(n(x) + y) + n(n(x) + n(y)) = x \; . <math>
External links
- EQP project: http://www-unix.mcs.anl.gov/AR/eqp/
- Robbins Algebras Are Boolean: http://www-unix.mcs.anl.gov/~mccune/papers/robbins/