DreamGroup/MRG → Automatheo 2010

Automatheo 2010

The 2010 Workshop on Automated Mathematical Theory Exploration
14-15 July 2010, Edinburgh, UK, a FLoC 2010 affiliated workshop of IJCAR and ITP.

Venue: ICMS at 14 India Street

Call for Participation and registration


Automated mathematical theory exploration is an exciting emerging research topic for mathematicians, developers of formalised mathematics, and those working on verified software. This topic concerns the theory and practice of developing software systems that support the automated development of mathematical theories, including the invention of definitions, theorems, conjectures, problems, examples and algorithms. The workshop aims to highlight the research area and foster collaboration amongst those working in software verification, formalised mathematics, and mathematical research, as well as help provide a shared understanding of the theory and tools for automated invention and discovery of mathematical theories.

Invited Speakers:

John Harrison: Challenges in formalizing geometric theorems
Dana S. Scott: Theory Exploration and Duality in Geometry


Some pictures of the event are available here.

Draft Programme

(Show only the programme) (Programme with abstracts and travel information)

First Day: Wed 14 July 2010

09:15 - 09:45 TEA & REGISTRATION
09:45 - 10:00 Welcome and opening remarks
10:00 - 11:00 Theory Exploration and Duality in Geometry Dana S. Scott
11:00 - 11:15 TEA & CHAT
11:15 - 11:45 The role of axiomatisation in mathematical discovery Alison Pease
11:45 - 12:15 Theory Formation with HR and GC John Charnley and Simon Colton
12:15 - 14:00 LUNCH
14:00 - 14:30 An Automated Confluence Proof for an Infinite Rewrite System via a Groebner Basis Computation [pdf of paper] Loredana Tec
14:30 - 15:00 Rewriting Completion Methods for Graphical Calculi Lucas Dixon
15:00 - 15:30 Automating quantum interactions Bob Coecke
15:30 - 16:00 TEA & CHAT
16:00 - 16:30 Theory exploration for working agebraists [extended abstract] David Stanovsky
16:30 - 17:00 Dimensions and Challenges Panel discussion
17:00 - late DRINKS & CHAT & FOOD

Second Day: Thu 15 July 2010

09:30 - 10:00 TEA & REGISTRATION
10:00 - 11:00 Challenges in formalizing geometric theorems John Harrison
11:00 - 11:15 TEA & CHAT
11:15 - 11:45 The Theory behind TheoryMine [pdf of paper] Alan Bundy, Flaminia Cavallo, Lucas Dixon, Moa Johansson and Roy McCasland
11:45 - 12:15 Formalising Term Synthesis for IsaCoSy [pdf of paper] Moa Johansson, Lucas Dixon and Alan Bundy
12:15 - 14:00 LUNCH
14:00 - 14:30 Proof assistants in mathematics Bogdan Grechuk
14:30 - 15:00 Scheme-based Definition and Conjecture Synthesis for Inductive Theories [extended abstract] Omar Montano Rivas, Roy McCasland, Lucas Dixon and Alan Bundy
15:00 - 15:30 TEA & CHAT
15:30 - 16:00 Generating Examples Roy McCasland
16:00 - 16:30 Dreams and Applications Panel discussion
16:30 - 17:00 TEA & CHAT
17:00 - 17:30 Business meeting

Important Dates:

Extended abstract and demo submission deadline:Wed. 5 May 2010
Acceptance notification:Wed. 2 June 2010
Early registration for attendance:until June 30
Final version of extended abstracts due:Wed. 30 June 2010
Workshop: 14-15 July 2010

Call for submissions and participation:

We invite proposals to give a talk and/or to provide a demo. Topics and demonstrations of interest include all aspects of mathematical theory exploration, especially the invention and discovery steps in the development of mathematical theories. This includes position statements, descriptions of important features, formalised accounts, descriptions and demos of systems that implement theory exploration, or other related work on theory exploration. We also welcome contributions on the application of theory exploration to other parts of mathematics, computer science and software engineering, as well as to other sciences such as physics and biology.

Currently, we encourage proposals for talks, by giving title and short abstract to Automatheo easychair site.

Support for student attendance:

Some support for student attendance can be requested through the AISB student travel awards, as well as from FLoC.


Registration is separate from the FLoC procedure; registration for Automatheo does not automatically entitle you to attend other FLoC workshop (and visa versa) - you need to register for those separately. Note also that Automatheo is happening at a different site, so if you are registered, and plan to go between workshops, you need to leave approx 30 minutes to walk, or 10 minutes by bus.

Go to the Automatheo-2010 registration page

Early registration is until June 30, 2010, and costs £75 (£35 for students).
Later registration costs: £95 (£55 for students).

Due to the size of the venue, the workshop will to be limitted to 35 participants.

Other Information:

Programme Committee:


The programme chairs are Lucas Dixon, Roy McCasland, Alan Smaill.


Automatheo 2009, at the RISC institute, Johannes Kepler University Linz, Austria.