Abstract is missing.
- Copyright Issues for MKMAndrew A. Adams, James H. Davenport. 1-16 [doi]
- Efficient Retrieval of Mathematical StatementsAndrea Asperti, Matteo Selmi. 17-31 [doi]
- Formalizing Set Theory as it Is Actually UsedArnon Avron. 32-43 [doi]
- Integrated Semantic Browsing of the Mizar Mathematical Library for Authoring Mizar ArticlesGrzegorz Bancerek, Josef Urban. 44-57 [doi]
- Informalising Formal Mathematics: Searching the Mizar Library with Latent SemanticsPaul A. Cairns. 58-72 [doi]
- Mathematical Service Matching Using Description Logic and OWLOlga Caprotti, Mike Dewar, Daniele Turi. 73-87 [doi]
- C-CoRN, the Constructive Coq Repository at NijmegenLuís Cruz-Filipe, Herman Geuvers, Freek Wiedijk. 88-103 [doi]
- Classifying Differential Equations on the WebDirk Draheim, Winfried Neun, Dima Suliman. 104-115 [doi]
- Managing Heterogeneous Theories within a Mathematical Knowledge RepositoryAdam Grabowski, Markus Moschner. 116-129 [doi]
- Rough Concept Analysis - Theory Development in the Mizar SystemAdam Grabowski, Christoph Schwarzweller. 130-144 [doi]
- A Path to Faithful Formalizations of MathematicsGueorgui I. Jojgov, Rob Nederpelt. 145-159 [doi]
- Flexible Encoding of Mathematics on the ComputerFairouz Kamareddine, Manuel Maarek, J. B. Wells. 160-174 [doi]
- CPoint: Dissolving the Author s DilemmaAndrea Kohlhase, Michael Kohlhase. 175-189 [doi]
- On Diagrammatic Representation of Mathematical KnowledgeZenon Kulpa. 190-204 [doi]
- Predicate Logic with Sequence Variables and Sequence Function SymbolsTemur Kutsia, Bruno Buchberger. 205-219 [doi]
- A Graph-Based Approach Towards Discerning Inherent Structures in a Digital Library of Formal MathematicsLori Lorigo, Jon M. Kleinberg, Richard Eaton, Robert L. Constable. 220-235 [doi]
- Theorem Proving and Proof Verification in the System SADAlexander V. Lyaletski, Andrey Paskevich, Konstantin Verchinine. 236-250 [doi]
- Adaptive Access to a Proof PlannerErica Melis, Andreas Meier, Martin Pollet. 251-264 [doi]
- Modeling Interactivity for Mathematics Learning by DemonstrationMiguel Angel Mora, Roberto Moriyón, Francisco Saiz. 265-275 [doi]
- Extraction of Logical Structure from Articles in MathematicsKoji Nakagawa, Akihiro Nomura, Masakazu Suzuki. 276-289 [doi]
- Improving Mizar Texts with Properties and RequirementsAdam Naumowicz, Czeslaw Bylinski. 290-301 [doi]
- An Investigation on the Dynamics of Direct-Manipulation Editors for MathematicsLuca Padovani, Riccardo Solmi. 302-316 [doi]
- Intuitive and Formal Representations: The Case of MatricesMartin Pollet, Volker Sorge, Manfred Kerber. 317-331 [doi]
- Mathematical Libraries as Proof Assistant EnvironmentsClaudio Sacerdoti Coen. 332-346 [doi]
- Efficient Ambiguous Parsing of Mathematical FormulaeClaudio Sacerdoti Coen, Stefano Zacchiroli. 347-362 [doi]
- An Architecture for Distributed Mathematical Web ServicesElena S. Smirnova, Clare M. So, Stephen M. Watt. 363-377 [doi]
- The Categorial Type of OpenMath ObjectsAndreas Strotmann. 378-392 [doi]