Abstract is missing.
- The Omega Number: Irreducible Complexity in Pure MathGregory J. Chaitin. 1 [doi]
- Roles of Math Search in MathematicsAbdou Youssef. 2-16 [doi]
- Structured Induction Proofs in Isabelle/IsarMakarius Wenzel. 17-30 [doi]
- Interpretation of Locales in Isabelle: Theories and Proof ContextsClemens Ballarin. 31-43 [doi]
- A Dynamic Poincaré PrincipleManfred Kerber. 44-53 [doi]
- A Proof-Theoretic Approach to TacticsKamal Aboul-Hosn. 54-66 [doi]
- A Formal Correspondence Between OMDoc with Alternative Proofs and the lambdaµµ-CalculusSerge Autexier, Claudio Sacerdoti Coen. 67-81 [doi]
- Proof Transformation by CERESMatthias Baaz, Stefan Hetzl, Alexander Leitsch, Clemens Richter, Hendrik Spohr. 82-93 [doi]
- Synthesizing Proof Planning Methods and Omega-Ants Agents from Mathematical KnowledgeSerge Autexier, Dominik Dietrich. 94-109 [doi]
- Verifying and Invalidating Textbook Proofs Using ScunakChad E. Brown. 110-123 [doi]
- Capturing Abstract Matrices from PaperToshihiro Kanahori, Alan P. Sexton, Volker Sorge, Masakazu Suzuki. 124-138 [doi]
- Towards a Parser for Mathematical Formula RecognitionAmar Raja, Matthew Rayner, Alan P. Sexton, Volker Sorge. 139-151 [doi]
- Stochastic Modelling of Scientific Terms Distribution in PublicationsRimantas Rudzkis, Vaidas Balys, Michiel Hazewinkel. 152-164 [doi]
- Capturing the Content of Physics: Systems, Observables, and ExperimentsEberhard R. Hilf, Michael Kohlhase, Heinrich Stamerjohanns. 165-178 [doi]
- Communities of Practice in MKM: An Extensional ModelAndrea Kohlhase, Michael Kohlhase. 179-193 [doi]
- From Notation to Semantics: There and Back AgainLuca Padovani, Stefano Zacchiroli. 194-207 [doi]
- Managing Informal Mathematical Knowledge: Techniques from Informal LogicAndrew Aberdein. 208-221 [doi]
- From Untyped to Polymorphically Typed Objects in Mathematical Web ServicesWilliam Naylor, Julian A. Padget. 222-236 [doi]
- Managing Automatically Formed Mathematical TheoriesSimon Colton, Pedro Torres, Paul A. Cairns, Volker Sorge. 237-250 [doi]
- Authoring LeActiveMath Calculus ContentPaul Libbrecht, Christian Gross. 251-265 [doi]
- Information Retrieval and Rendering withGrzegorz Bancerek. 266-279 [doi]
- Integrating Dynamic Geometry Software, Deduction Systems, and Theorem RepositoriesPedro Quaresma, Predrag Janicic. 280-294 [doi]