Invited Talks |
The Omega Number: Irreducible Complexity in Pure Math / Gregory J. Chaitin |
Roles of Math Search in Mathematics / Abdou Youssef |
Contributed Papers |
Structured Induction Proofs in Isabelle/Isar / Makarius Wenzel |
Interpretation of Locales in Isabelle: Theories and Proof Contexts / Clemens Ballarin |
A Dynamic Poincare Principle / Manfred Kerber |
A Proof-Theoretic Approach to Tactics / Kamal Aboul-Hosn |
A Formal Correspondence Between OMDoc with Alternative Proofs and the [Characters not reproducible]-Calculus / Serge Autexier ; Claudio Sacerdoti-Coen |
Proof Transformation by Ceres / Matthias Baaz ; Stefan Hetzl ; Alexander Leitsch ; Clemens Richter ; Hendrik Spohr |
Synthesizing Proof Planning Methods and [Omega]-Ants Agents from Mathematical Knowledge / Dominik Dietrich |
Verifying and Invalidating Textbook Proofs Using Scunak / Chad E. Brown |
Capturing Abstract Matrices from Paper / Toshihiro Kanahori ; Alan Sexton ; Volker Sorge ; Masakazu Suzuki |
Towards a Parser for Mathematical Formula Recognition / Amar Raja ; Matthew Rayner |
Stochastic Modelling of Scientific Terms Distribution in Publications / Rimantas Rudzkis ; Vaidas Balys ; Michiel Hazewinkel |
Capturing the Content of Physics: Systems, Observables, and Experiments / Eberhard R. Hilf ; Michael Kohlhase ; Heinrich Stamerjohanns |
Communities of Practice in MKM: An Extensional Model / Andrea Kohlhase |
From Notation to Semantics: There and Back Again / Luca Padovani ; Stefano Zacchiroli |
Managing Informal Mathematical Knowledge: Techniques from Informal Logic / Andrew Aberdein |
From Untyped to Polymorphically Typed Objects in Mathematical Web Services / William Naylor ; Julian Padget |
Managing Automatically Formed Mathematical Theories / Simon Colton ; Pedro Torres ; Paul Cairns |
Authoring LeActiveMath Calculus Content / Paul Libbrecht ; Christian Gross |
Information Retrieval and Rendering with MML Query / Grzegorz Bancerek |
Integrating Dynamic Geometry Software, Deduction Systems, and Theorem Repositories / Pedro Quaresma ; Predrag Janicic |
Author Index |
Invited Talks |
The Omega Number: Irreducible Complexity in Pure Math / Gregory J. Chaitin |
Roles of Math Search in Mathematics / Abdou Youssef |
Contributed Papers |
Structured Induction Proofs in Isabelle/Isar / Makarius Wenzel |
Interpretation of Locales in Isabelle: Theories and Proof Contexts / Clemens Ballarin |