Mathematical Knowledge Management: Second International Conference, MKM 2003 Bertinoro, Italy, February 16–18, 2003 Proceedings

This document was uploaded by one of our users. The uploader already confirmed that they had the permission to publish it. If you are author/publisher or own the copyright of this documents, please report to us by using this DMCA report form.

Simply click on the Download Book button.

Yes, Book downloads on Ebookily are 100% Free.

Sometimes the book is free on Amazon As well, so go ahead and hit "Search on Amazon"

This book constitutes the refereed proceedings of the Second International Conference on Mathematical Knowledge Management, MKM 2003, held in Betinoro, Italy, in February 2003.

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.

Author(s): Andrew A. Adams (auth.), Andrea Asperti, Bruno Buchberger, James Harold Davenport (eds.)
Series: Lecture Notes in Computer Science 2594
Edition: 1
Publisher: Springer-Verlag Berlin Heidelberg
Year: 2003

Language: English
Pages: 230
Tags: Information Storage and Retrieval; Mathematical Logic and Formal Languages; Symbolic and Algebraic Manipulation; Database Management; Artificial Intelligence (incl. Robotics); Computational Mathematics and Numerical Analysis

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