DreamGroup/MRGAutomatheo 2010 → Programme

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

(go back to the Automatheo homepage)

Draft Programme

First Day: Wed 14 July 2010

TimeTitleAuthor(s)
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

TimeTitleAuthor(s)
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