Inhaltsverzeichnis
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.