| Time | Details |
|---|---|
| 08:30-09:00 | Registration |
| 09:00-09:10 | Welcome |
| 09:10-10:00 |
Session I: Invited Talk
GregChaitin Irreducible complexity in pure math |
| 10:00-10:30 | Coffee Break |
| 10:30-12:35 |
Session II: Proof Representations
Wenzel: Structured Induction Proofs inIsabelle/Isar Ballarin: Interpretation of Locales inIsabelle: Theories and Proof Contexts Kerber: A Dynamic Poincare Principle Aboul-Hosn: A Proof-Theoretic Approachto Tactics Autexier/Sacerdoti-Coen: A FormalCorrespondence 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 ProofPlanning 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 forMathematical Formula Recognition Balys et al : Stochastic Modeling ofScientific 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 ofPhysics: Systems, Observables, and Experiments Kohlhase/Kohlhase: Communities of Practice inMKM; An extensional Model Padovani/Zacchiroli: From Notation toSemantics: There and Back Again Aberdein: Managing Informal MathematicalKnowledge: Techniques from Informal Logic Naylor/Padget: From Untyped to PolymorphicallyTyped 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 |