Objectives

• Promote AR tools to a wider audience.
• Maintain a web resource of successful and open challenges.
• Provide support for AR applications

Description of work

Automated reasoning has had a number of successes in proving open results of interest to mathematicians. For example, the long standing Robbins problem---are all Robbins algebras Boolean?--- was proved automatically by EQP, a theorem proving program developed at Argonne National Laboratory. As a second example, Slaney, Fujita, and others have proved a number of open results about the existence and nonexistence of quasigroups with particular properties. More such results could be obtained if mathematicians were more aware of the AR tools available to help them solve problems, and if researchers in AR were more aware of mathematical problems that might be tackled using their tools. The aim of this workpackage is to identify a number of grand challenges for the AR Community, and to promote AR tools to a wider mathematical audience. Communication of these challenges and of successful solutions to these challenges will be via meetings and web resources. Each set of workshops will be held alongside both of an AR event (like CADE, LPAR, ...) and again alongside a more general, mathematical event (e.g the European or International Congress on Mathematics).

Key nodes participating: see Appendix A, addendum.

Deliverables

• Web pages
• Meeting reports of a Grand Challenge (GC) committee
• Workshops on Grand Challenges.

Milestones and expected result

• Months 1-6 First meeting of GC committee, identification of potential application areas.
• Months 7-12 Second meeting of GC committee. First set of Grand Challenges released onto web site.
• Months 13-24 First set of workshops. Feedback from workshops to GC committee. Second set of Grand Challenges released onto web site in response to first workshops.
• Months 25-36 Second set of workshops. Feedback from workshops to GC committee. Final set of Grand Challenges released onto web site.