| Time | Details |
|---|---|
| 08:30-09:00 | Registration |
| 09:00-09:10 | Welcome |
| 09:10-10:00 | Session I: Invited Talk Greg Chaitin Irreducible complexity in pure math |
| 10:00-10:30 | Coffee Break |
| 10:30-12:35 | Session II: Proof Representations Wenzel: Structured Induction Proofs in Isabelle/Isar Ballarin: Interpretation of Locales in Isabelle: Theories and Proof Contexts Kerber: A Dynamic Poincare Principle Aboul-Hosn: A Proof-Theoretic Approach to Tactics Autexier/Sacerdoti-Coen: A Formal Correspondence between OMDoc with Alternative Proofs and the LambdaBarMuMuTilde-Calculus |
| 12:35-14:00 | Lunch |
| 14:00-15:15 | Session III: Proof Processing Baaz et al: Proof Transformation by CERES Autexier/Deitrich: Synthesizing Proof Planning Methods and O-Ants Agents from Mathematical Knowledge Brown: Verifying and Invalidating Textbook Proofs using Scunak |
| 15:15-15:45 | Coffee Break |
| 15:45-17:00 | Session IV: Knowledge Extraction Kanahori et al: Capturing Abstract Matrices from Paper Raja et al: Towards a Parser for Mathematical Formula Recognition Balys et al: Stochastic Modeling of Scientific Terms Distribution in Publications |
| 17:00-18:00 | |
| 18:00-19:00 | MKM Interest Group Business Meeting |
| 19:30-Late | Banquet |
| Time | Details |
|---|---|
| 09:00-09:10 | Welcome |
| 09:10-10:00 | Session V: Invited Talk Abdou Youssef Roles of Math Search in Mathematics |
| 10:00-10:30 | Coffee Break |
| 10:30-12:35 | Session VI: Knowledge Representation Hilf et al: Capturing the Content of Physics: Systems, Observables, and Experiments Kohlhase/Kohlhase: Communities of Practice in MKM; An extensional Model Padovani/Zacchiroli: From Notation to Semantics: There and Back Again Aberdein: Managing Informal Mathematical Knowledge: Techniques from Informal Logic Naylor/Padget: From Untyped to Polymorphically Typed Objects in Mathematical Web Services |
| 12:35-14:00 | Lunch |
| 14:00-15:40 | Session VII: Systems and Tools Colton et al: Managing Automatically Formed Mathematical Theories Libbrecht/Gross: Authoring LeActiveMath Calculus Content Bancarek: Information Retrieval and Rendering with MML Query Quaresma/Janicic: Integrating Dynamic Geometry Tools, Deduction System, and Theorem Repositories (Part 1, Part 2) |
| 15:40-16:15 | Coffee Break |
| 16:15-17:15 | Session VIII: Panel Discussion Gregory Chaitin, Patrick Ion, Michael Kohlhase, Abdou Youssef What are the characteristics of mathematical knowledge that make managing it different from managing other kinds of knowledge? |
| 17:15-17:30 | Closing |