5. MKM 2006: Wokingham, UK

Invited Talks

• Gregory J. Chaitin:
  The Omega Number: Irreducible Complexity in Pure Math. 1
  
• Abdou Youssef:
  Roles of Math Search in Mathematics. 2-16
  

Contributed Papers

• Makarius Wenzel:
  Structured Induction Proofs in Isabelle/Isar. 17-30
  
• Clemens Ballarin:
  Interpretation of Locales in Isabelle: Theories and Proof Contexts. 31-43
  
• Manfred Kerber:
  A Dynamic Poincaré Principle. 44-53
  
• Kamal Aboul-Hosn:
  A Proof-Theoretic Approach to Tactics. 54-66
  
• Serge Autexier, Claudio Sacerdoti Coen:
  A Formal Correspondence Between OMDoc with Alternative Proofs and the lambdaµµ-Calculus. 67-81
  
• Matthias Baaz, Stefan Hetzl, Alexander Leitsch, Clemens Richter, Hendrik Spohr:
  Proof Transformation by CERES. 82-93
  
• Serge Autexier, Dominik Dietrich:
  Synthesizing Proof Planning Methods and Omega-Ants Agents from Mathematical Knowledge. 94-109
  
• Chad E. Brown:
  Verifying and Invalidating Textbook Proofs Using Scunak. 110-123
  
• Toshihiro Kanahori, Alan P. Sexton, Volker Sorge, Masakazu Suzuki:
  Capturing Abstract Matrices from Paper. 124-138
  
• Amar Raja, Matthew Rayner, Alan P. Sexton, Volker Sorge:
  Towards a Parser for Mathematical Formula Recognition. 139-151
  
• Rimantas Rudzkis, Vaidas Balys, Michiel Hazewinkel:
  Stochastic Modelling of Scientific Terms Distribution in Publications. 152-164
  
• Eberhard R. Hilf, Michael Kohlhase, Heinrich Stamerjohanns:
  Capturing the Content of Physics: Systems, Observables, and Experiments. 165-178
  
• Andrea Kohlhase, Michael Kohlhase:
  Communities of Practice in MKM: An Extensional Model. 179-193
  
• Luca Padovani, Stefano Zacchiroli:
  From Notation to Semantics: There and Back Again. 194-207
  
• Andrew Aberdein:
  Managing Informal Mathematical Knowledge: Techniques from Informal Logic. 208-221
  
• William Naylor, Julian A. Padget:
  From Untyped to Polymorphically Typed Objects in Mathematical Web Services. 222-236
  
• Simon Colton, Pedro Torres, Paul A. Cairns, Volker Sorge:
  Managing Automatically Formed Mathematical Theories. 237-250
  
• Paul Libbrecht, Christian Gross:
  Authoring LeActiveMath Calculus Content. 251-265
  
• Grzegorz Bancerek:
  Information Retrieval and Rendering with. 266-279
  
• Pedro Quaresma, Predrag Janicic:
  Integrating Dynamic Geometry Software, Deduction Systems, and Theorem Repositories. 280-294