Workshop Programme
The workshop will be a one day workshop, organized as follows:
- 09:00-10:00 - Invited talk with DML
- CEDRICS: When CEDRAM Meets Tralics
Thierry Bouche
- CEDRICS: When CEDRAM Meets Tralics
- 10:00-10:30 - Break
- 10:30-11:30 - Invited talk
- Reasoning in Equational Logic with Waldmeister
Thomas Hillenbrand
- Reasoning in Equational Logic with Waldmeister
- 11:30-11:35 - Caffeine transfer break
- 11:35-12:35 - Systems Papers
- Applications of a Global Workspace Framework to Mathematical Discovery
John Charnley and Simon Colton - Proof Analysis with HLK, CERES and ProofTool: Current Status and Future Directions
Stefan Hetzl, Alexander Leitsch, Daniel Weller and Bruno Woltzenlogel Paleo
- Applications of a Global Workspace Framework to Mathematical Discovery
- 12:35-14:00 - Lunch
- 14:00-15:00 - Invited talk
- Title TBA
Georges Gonthier
- Title TBA
- 15:00-15:30 - Break
- 15:30-17:00 - Applications Papers
- Automated Parameterisation of Finite Algebras
Simon Colton and Volker Sorge - Automated Theorem Proving in Loop Theory
David Stanovsky and J.D. Phillips - Generating Loops with the Inverse Property
John Slaney and Asif Ali
- Automated Parameterisation of Finite Algebras
- 17:00-19:00 - System demonstrations with MathUI