Copyright Issues for MKM.- Efficient Retrieval of Mathematical Statements.- Formalizing Set Theory as it Is Actually Used.- Integrated Semantic Browsing of the Mizar Mathematical Library for Authoring Mizar Articles.- Informalising Formal Mathematics: Searching the Mizar Library with Latent Semantics.- Mathematical Service Matching Using Description Logic and OWL.- C-CoRN, the Constructive Coq Repository at Nijmegen.- Classifying Differential Equations on the Web.- Managing Heterogeneous Theories within a Mathematical Knowledge Repository.- Rough Concept Analysis - Theory Development in the Mizar System.- A Path to Faithful Formalizations of Mathematics.- Flexible Encoding of Mathematics on the Computer.- CPoint: Dissolving the Author's Dilemma.- On Diagrammatic Representation of Mathematical Knowledge.- Predicate Logic with Sequence Variables and Sequence Function Symbols.- A Graph-Based Approach Towards Discerning Inherent Structures in a Digital Library of Formal Mathematics.- Theorem Proving and Proof Verification in the System SAD.- Adaptive Access to a Proof Planner.- Modeling Interactivity for Mathematics Learning by Demonstration.- Extraction of Logical Structure from Articles in Mathematics.- Improving Mizar Texts with Properties and Requirements.- An Investigation on the Dynamics of Direct-Manipulation Editors for Mathematics.- Intuitive and Formal Representations: The Case of Matrices.- Mathematical Libraries as Proof Assistant Environments.- Efficient Ambiguous Parsing of Mathematical Formulae.- An Architecture for Distributed Mathematical Web Services.- The Categorial Type of OpenMath Objects.
