Mechanical proofs of the Levi commutator problem
Maria Paola Bonacina · 1998
. This note presents purely mechanical proofs of the Levi commutator problem in group theory. The problem was solved first by using the theorem prover EQP, developed by William McCune at the Argonne National Laboratory. The fastest proof was found by using Peers-mcd, the Clause-Diffusion parallelization of EQP, developed by the author at the University of Iowa. 1 The Levi commutator problem The Levi commutator problem is an equational problem in group theory. Given the axioms for a group with product and identity e e x ' x x \\Gamma1 x ' e (x y) z ' x (y z) the commutator is a binary operator [ ; ] defined by: [x; y] ' x \\Gamma1 y \\Gamma1 x y: The Levi commutator problem consists in proving that x [y; z] ' [y; z] x , [[x; y]; z] ' [x; [y; z]] that is, x [y; z] ' [y; z] x holds if an only if the commutator is associative. A textbook proof of this theorem can be found in [10]. In the input to the theorem provers, the group axioms and the commutator definition are...