EQP
Encyclopedia
EQP, an abbreviation for equational prover, is an automated theorem proving
program for equational logic
, developed by the Mathematics and Computer Science Division of the Argonne National Laboratory
. It was one of the provers used for solving a longstanding problem posed by Herbert Robbins
, namely, whether all Robbins algebra
s are Boolean algebras.
Automated theorem proving
Automated theorem proving or automated deduction, currently the most well-developed subfield of automated reasoning , is the proving of mathematical theorems by a computer program.- Decidability of the problem :...
program for equational logic
Equational logic
First-order equational logic consists of quantifier-free terms of ordinary first-order logic, with equality as the only predicate symbol. The model theory of this logic was developed into Universal algebra by Birkhoff et al. [Birkhoff, Gratzer, Cohn]...
, developed by the Mathematics and Computer Science Division of the Argonne National Laboratory
Argonne National Laboratory
Argonne National Laboratory is the first science and engineering research national laboratory in the United States, receiving this designation on July 1, 1946. It is the largest national laboratory by size and scope in the Midwest...
. It was one of the provers used for solving a longstanding problem posed by Herbert Robbins
Herbert Robbins
Herbert Ellis Robbins was an American mathematician and statistician who did research in topology, measure theory, statistics, and a variety of other fields. He was the co-author, with Richard Courant, of What is Mathematics?, a popularization that is still in print. The Robbins lemma, used in...
, namely, whether all Robbins algebra
Robbins algebra
In abstract algebra, a Robbins algebra is an algebra containing a single binary operation, usually denoted by \lor, and a single unary operation usually denoted by \neg...
s are Boolean algebras.