Automatheo 2010

First Day: Wed 14 July 2010

Time	Title	Author(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

Time	Title	Author(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