(go back to the Automatheo homepage)
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 |