A case study in automated theorem proving: A difficult problem about commutators
IL (United States) Argonne National Lab., W McCune, USDOE, Washington, DC (United States) (US) · 1995
This paper shows how the automated deduction system OTTER. was used to prove the group theory theorem {chi}{sup 3} = e {implies} [[[y, z], u], v] = e, where e is the identity, and [XI Y] is the commutator {chi}{prime}y{prime}{chi}y. This is a difficult problem for automated provers, and several lengthy searches were run before a proof was found. Problem formulation and search strategy played a key role in the success. I believe that ours is the first automated proof of the theorem.