EQP

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>

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/