EQP, an abreviation 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>