Andrew A. Adams (auth.), Andrea Asperti, Bruno Buchberger, James Harold Davenport (eds.)3540005684, 9783540005681
The 16 revised full papers presented together with an invited paper were carefully reviewed and selected for presentation. Among the topics addressed are digitization, representation, formalization, proof assistants, distributed libraries of mathematics, NAG library, LaTeX, MathML, mathematics markup, theorem description, query languages for mathematical metadata, mathematical information retrieval, XML-based mathematical knowledge processing, semantic Web, mathematical content management, formalized mathematics repositories, theorem proving, and proof theory.
Table of contents :
Digitisation, Representation, and Formalisation Digital Libraries of Mathematics….Pages 1-16
MKM from Book to Computer: A Case Study….Pages 17-29
From Proof-Assistants to Distributed Libraries of Mathematics: Tips and Pitfalls….Pages 30-44
Managing Digital Mathematical Discourse….Pages 45-55
NAG Library Documentation….Pages 56-65
On the Roles of LATEX and MathML in Encoding and Processing Mathematical Expressions….Pages 66-79
Problems and Solutions for Markup for Mathematical Examples and Exercises….Pages 80-92
An Annotated Corpus and a Grammar Model of Theorem Description….Pages 93-104
A Query Language for a Metadata Framework about Mathematical Resources….Pages 105-118
Information Retrieval in MML….Pages 119-132
An Expert System for the Flexible Processing of X ML -Based Mathematical Knowledge in a P ROLOG —Environment….Pages 133-146
Towards Collaborative Content Management and Version Control for Structured Mathematical Knowledge….Pages 147-161
On the Integrity of a Repository of Formalized Mathematics….Pages 162-174
A Theoretical Analysis of Hierarchical Proofs….Pages 175-187
Comparing Mathematical Provers….Pages 188-202
Translating Mizar for First Order Theorem Provers….Pages 203-215
The Mathematical Semantic Web….Pages 216-223
Reviews
There are no reviews yet.