I offer the following challenge taken from abstract algebra. In an earlier column I presented a related problem, which may have offered some difficulty. This may offer more.
A group is a nonempty set with an operation f, called multiplication or addition. With respect to that operation, the set (typically) admits a two-sided identity e, two-sided inverse (with respect to the identity) i, and associativity. (Other definitions exist.) A group of exponent n is a group in which, for all elements x, xn=e.
Many years ago, William McCune (author of OTTER) and I collaborated on a study with the goal of using automated reasoning (also called automated deduction) to find single axioms in various areas. We asked OTTER first to find candidate single axioms and then to prove that the candidates were in fact single axioms. OTTER succeeded, finding single axioms (some with the identity given explicitly and others without) for groups of exponents 3, 5, and 7. We then studied cases for single axioms for groups of odd exponent, up to and including exponent 19. OTTER again succeeded.
And now, here is the challenge. You are asked to prove that the following equation is a single axiom for groups of exponent 19:
(f(x,f(x,f(x,f(x,f(x,f(x,f(x,f(x,f(x,f(f(x,f(x,f(x,f(x,f(x,f(x,f(x,f(x,f(x,f(f(x,y),z)))))))))),
f(e,f(z,f(z,f(z,f(z,f(z,f(z,f(z,f(z,f(z,f(z,f(z,f(z,f(z,f(z,f(z,f(z,f(z,z))))))))))))))))))
)))))))))) = y).
The following correspond to the targets.
(f(e,a) != a) | $ANS(lid). (f(a,e) != a) | $ANS(rid). (f(f(a,b),c) != f(a,f(b,c))) | $ANS(assoc). (f(a,f(a,f(a,f(a,f(a,f(a,f(a,f(a,f(a,f(a,f(a,f(a,f(a,f(a,f(a,f(a,f(a,f(a,a)))))))))))))))))) != e) | $ANS(exp19).
Of course, you might choose to rely on paramodulation with various strategies, or perhaps on a Knuth-Bendix approach. I generally avoid Knuth-Bendix because all actions taken by a program are far more transparent when demodulation is not applied automatically.
Exponent 19 is the largest exponent problem in group theory I have ever studied. I would be interested to learn of successes with greater exponents.
in recognition of his ground-breaking research on the design and use of well-founded orderings in term rewriting and automated deduction.
The Award will be presented at CADE 2011, the 23rd International Conference on Automated Deduction, on August 2, 2011.
Dear Member of the Association for Automated Reasoning,
Nominations for two CADE trustee positions are being sought, in preparation for the elections to be held after CADE-23.
The current members of the board of trustees are (in alphabetical order):
The terms of Christoph Benzmüller and Reiner Hähnle expire. Christoph Benzmüller is eligible to be nominated for a second term. Reiner Hähnle has served two successive elected terms, and is therefore not eligible to be nominated for a third.
The terms of office of Nikolaj Bjørner and Viorica Sofronie-Stokkermans as CADE-23 program co-chairs also end. As outgoing ex-officio trustees, they are eligible to be nominated as elected trustees.
In summary, we are seeking to elect two trustees.
Nominations can be made by any AAR member, either by e-mail or in person at the CADE business meeting at CADE-23. Two members, a principal nominator and a second, are required to make a nomination, and it is their responsibility to ask people's permission before nominating them. A member may nominate or second only one candidate. Nominees must be AAR members. For further details please see the CADE Inc. bylaws at the CADE Web site.
E-mail nominations are to be sent to Franz Baader, CADE President (baader (at) tcs (dot) inf (dot) tu-dresden (dot) de) and Martin Giese, CADE Secretary (martingi (at) ifi (dot) uio (dot) de), up to the upcoming CADE business meeting (to be held on August 3, at CADE-23), or otherwise during the CADE business meeting.
The 23rd Conference on Automated Deduction, CADE-23, will take place in Wroclaw on 31 July to 5 August 2011. CADE is the major forum for the presentation of research in all aspects of automated deduction. The conference programme will include invited talks, paper presentations, system descriptions, workshops, tutorials, and system competitions.
Early registration is still open until June 18.
Refer to the CADE-23 web page for full information.
The 20th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods will take place in Bern, Switzerland on July 4–8, 2011. The conference brings together researchers interested in all aspects of the mechanisation of reasoning with tableaux and related methods.
Early registration is closed, but regular registration is still possible at the conference web page.
The 23rd International Conference on Computer Aided Verification, CAV 2011, will be held in Cliff Lodge, Snowbird, Utah on July 14–20, 2011. The CAV conference series is dedicated to the advancement of the theory and practice of computer-aided formal analysis methods for hardware and software systems.
Early registration ends on June 20, but special rate hotel rooms are likely to be exhausted earlier.
Refer to the CAV website for registration instructions.
The Eighth International Workshop on First-Order Theorem Proving will take place in Bern, Switzerland on July 4, 2011, co-locating with Tableaux 2011. The series of FTP workshops focusses on all aspects of theorem proving in first-order logic. It aims to be a forum for the presentation of original work, and for the discussion of work in progress.
Refer to the workshop web page for details about the registration procedure.