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.
| John Harrison: | Challenges in formalizing geometric theorems |
| Dana S. Scott: | Theory Exploration and Duality in Geometry |
Some pictures of the event are available
(Show only the programme) (Programme with abstracts and travel information)
| Time | Title | Author(s) |
|---|---|---|
| TEA & REGISTRATION | ||
| Welcome and opening remarks | ||
| Theory Exploration and Duality in Geometry | Dana S. Scott | |
| TEA & CHAT | ||
| The role of axiomatisation in mathematical discovery | Alison Pease | |
| Theory Formation with HR and GC | John Charnley and Simon Colton | |
| LUNCH | ||
| An Automated Confluence Proof for an Infinite Rewrite System via a Groebner Basis Computation [pdf of paper] | Loredana Tec | |
| Rewriting Completion Methods for Graphical Calculi | Lucas Dixon | |
| Automating quantum interactions | Bob Coecke | |
| TEA & CHAT | ||
| Theory exploration for working agebraists [extended abstract] | David Stanovsky | |
| Dimensions and Challenges | Panel discussion | |
| DRINKS & CHAT & FOOD | ||
| Time | Title | Author(s) |
|---|---|---|
| TEA & REGISTRATION | ||
| Challenges in formalizing geometric theorems | John Harrison | |
| TEA & CHAT | ||
| The Theory behind TheoryMine [pdf of paper] | Alan Bundy, Flaminia Cavallo, Lucas Dixon, Moa Johansson and Roy McCasland | |
| Formalising Term Synthesis for IsaCoSy [pdf of paper] | Moa Johansson, Lucas Dixon and Alan Bundy | |
| LUNCH | ||
| Proof assistants in mathematics | Bogdan Grechuk | |
| Scheme-based Definition and Conjecture Synthesis for Inductive Theories [extended abstract] | Omar Montano Rivas, Roy McCasland, Lucas Dixon and Alan Bundy | |
| TEA & CHAT | ||
| Generating Examples | Roy McCasland | |
| Dreams and Applications | Panel discussion | |
| TEA & CHAT | ||
| Business meeting | ||
| 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 |
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.
Some support for student attendance can be requested through the AISB student travel awards, as well as from FLoC.
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.
Note that this is not the same location as other FLoC events, and it takes about 30 minutes to walk (or 10 minutes by bus) between sites.
Note that this is not the same location as other FLoC events, and it takes about 30 minutes to walk (or 10 minutes by bus) between sites.
the Lothian bus route map is not very good, but is still the best overview of busses in Edinburgh.
from Appleton Tower and the Informatics Forum: The bus number 42 passes along Buccleuch Street, right by the Informatics Forum and Appleton tower, but only runs every 30 minutes. See the google map with stops and live bus tracker for the bus number 42.
You can also catch the number 29, from Nicholson Street, which runs every 15 minutes. See the google map with stops and live bus tracker for the bus number 29.
For either bus, one should get off just past Herriot Row, then walk west along Herriot Row for one block -- India Street will be the first right. They can have a look at the ICMS web page map
A Taxi from Appleton Tower will cost around 7 pounds.
Automatheo 2009, at the RISC institute, Johannes Kepler University Linz, Austria.