Abstract is missing.
- A Proof-Theoretic Approach to Hierarchical Math Library OrganizationKamal Aboul-Hosn, Terese Andersen. 1-16 [doi]
- An Exploration in the Space of Mathematical KnowledgeAndrea Kohlhase, Michael Kohlhase. 17-32 [doi]
- Authoring Presentation for OpenMathShahid Manzoor, Paul Libbrecht, Carsten Ullrich, Erica Melis. 33-48 [doi]
- Translating Mathematical Vernacular into Knowledge RepositoriesAdam Grabowski, Christoph Schwarzweller. 49-64 [doi]
- Assisted Proof Document AuthoringDavid Aspinall, Christoph Lüth, Burkhart Wolff. 65-80 [doi]
- A Tough Nut for Mathematical Knowledge ManagementManfred Kerber, Martin Pollet. 81-95 [doi]
- Textbook Proofs Meet Formal Logic - The Problem of Underspecification and GranularitySerge Autexier, Armin Fiedler. 96-110 [doi]
- Processing Textbook-Style MatricesAlan P. Sexton, Volker Sorge. 111-125 [doi]
- A Generic Modular Data Structure for Proof Attempts Alternating on Ideas and GranularitySerge Autexier, Christoph Benzmüller, Dominik Dietrich, Andreas Meier, Claus-Peter Wirth. 126-142 [doi]
- Impasse-Driven Reasoning in Proof PlanningAndreas Meier, Erica Melis. 143-158 [doi]
- Literate Proving: Presenting and Documenting Formal ProofsPaul A. Cairns, Jeremy Gow. 159-173 [doi]
- Semantic Matching for Mathematical ServicesWilliam Naylor, Julian A. Padget. 174-189 [doi]
- Mathematical Knowledge Browser with Automatic Hyperlink DetectionKoji Nakagawa, Masakazu Suzuki. 190-202 [doi]
- A Database of Glyphs for OCR of Mathematical DocumentsAlan P. Sexton, Volker Sorge. 203-216 [doi]
- Toward an Object-Oriented Structure for Mathematical TextFairouz Kamareddine, Manuel Maarek, J. B. Wells. 217-233 [doi]
- Explanation in Natural Language of lamda-µµ-TermsClaudio Sacerdoti Coen. 234-249 [doi]
- Engineering Mathematical KnowledgeAchim Mahnke, Jan Scheffczyk. 250-266 [doi]
- Computational Origami of a Morley s TriangleTetsuo Ida, Hidekazu Takahashi, Mircea Marin. 267-282 [doi]
- Designing Diagrammatic Catalogues of Types of Basic Interval Equation: A Case StudyZenon Kulpa. 283-298 [doi]
- Gröbner Bases - Theory Refinement in the Mizar SystemChristoph Schwarzweller. 299-314 [doi]
- An Interactive Algebra Course with Formalised Proofs and DefinitionsAndrea Asperti, Herman Geuvers, Iris Loeb, Lionel Elie Mamane, Claudio Sacerdoti Coen. 315-329 [doi]
- Interactive Learning and Mathematical CalculusArjeh M. Cohen, Hans Cuypers, Dorina Jibetean, Mark Spanbroek. 330-345 [doi]
- XML-izing Mizar: Making Semantic Processing and Presentation of MML EasyJosef Urban. 346-360 [doi]
- Determining Empirical Characteristics of Mathematical Expression UseClare M. So, Stephen M. Watt. 361-375 [doi]
- Transformations of MML Database s ElementsRobert Milewski. 376-388 [doi]
- Translating a Fragment of Weak Type Theory into Type Theory with Open TermsGueorgui I. Jojgov. 389-403 [doi]