Mathematical Knowledge Management: Second International Conference, MKM 2003 Bertinoro, Italy, February 16-18, 2003 (Lecture Notes in Computer Science, 2594)

This Volume Contains The Proceedings Of Thesecondinternationalconferenceon Mathematicalknowledgemanagement (mkm 2003), Held 16–18 February 2003 In Bertinoro, Italy. Mathematical Knowledge Management Is An Exciting New ?eld At The Int- Section Between Mathematics And Computer Science. We Need E?cient, New Te- Niques, Based On Sophisticated Formal Mathematics And Software Technology, To Exploit The Enormous Knowledge Available In Current Mathematical Sources And To Organize Mathematical Knowledge In A New Way. On The Other Side, Due To Its Verynature,therealmofmathematicalinformationlookslikethebestcandidate For Testing Innovative Theoretical And Technological Solutions For Content-based Systems, Interoperability, Management Of Machine-understandable Information, And The Semantic Web. The Organizers Are Grateful To Dana Scott And Massimo Marchiori For Agr- Ing To Give Invited Talks At Mkm 2003.^ November 2002 Andreaasperti Brunobuchberger Jamesdavenport Conference Organization Andrea Asperti (program Chair) Luca Padovani (organizing Chair) Program Commitee A. Asperti (bologna) P. D. F. Ion (michigan) B. Buchberger (risc Linz) Z. Luo (durham) J. Caldwell (wyoming) R. Nederpelt (eindhoven) O. Caprotti (risc Linz) M. Sofroniou (wolfram Research Inc. ) J. Davenport (bath) N. Soi?er (wolfram Research Inc. ) W. M. Farmer (mcmaster Univ. ) M. Suzuki (kyushu) H. Geuvers (nijmegen) N. Takayama (kobe) T. Hardin (paris 6) A. Trybulec (bialystok) M. Hazewinkel (cwi Amsterdam) S. M. Watt (uwo) M. Kohlhase (cmu) B. Wegner (berlin) Invited Speakers Massimo Marchiori (w3c, University Of Venezia) Dana Scott (cmu) Additional Referees G. Bancerek R. Gamboa G. Jojgov P. Callaghan B. Han V. Prevosto D. Doligez Table Of Contents Regular Contributions Digitisation,representation,andformalisation (digitallibrariesofmathematics) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .^ 1 Andrew A. Adams Mkmfrombooktocomputer:acasestudy . . . . . . . . . . . . . . . . . . . . . . . Regular Contributions -- Digitisation, Representation, And Formalisation Digital Libraries Of Mathematics -- Mkm From Book To Computer: A Case Study -- From Proof-assistants To Distributed Libraries Of Mathematics: Tips And Pitfalls -- Managing Digital Mathematical Discourse -- Nag Library Documentation -- On The Roles Of Latex And Mathml In Encoding And Processing Mathematical Expressions -- Problems And Solutions For Markup For Mathematical Examples And Exercises -- An Annotated Corpus And A Grammar Model Of Theorem Description -- A Query Language For A Metadata Framework About Mathematical Resources -- Information Retrieval In Mml -- An Expert System For The Flexible Processing Of Xml -based Mathematical Knowledge In A Prolog—environment -- Towards Collaborative Content Management And Version Control For Structured Mathematical Knowledge -- On The Integrity Of A Repository Of Formalized Mathematics -- A Theoretical Analysis Of Hierarchical Proofs -- Comparing Mathematical Provers -- Translating Mizar For First Order Theorem Provers -- Invited Talk -- The Mathematical Semantic Web. Andrea Asperti, Bruno Buchberger, James H. Davenport (eds.). Includes Bibliographical References And Index. Cover Title page Copyright page Preface Table of Contents Digitisation, Representation, and Formalisation Digital Libraries of Mathematics 1 Introduction 2 Digitisation 3 Representation 3.1 Representation from Digital Encoding 3.2 Representation in the Primary Source 3.3 Representation and Explanation 3.4 Maintenance of Archives of Represented Material 4 Formalisation 4.1 Representation Languages and Formats 5 Information Dissemination 5.1 Different Users and Their Needs 5.2 From Caxton to CERN 5.3 Copyright, Corporate Publishing, and Quality Concerns 5.4 Meta-information 6 Prior Art: Previous and Current Projects of Relevance to MKM 7 Conclusions References MKM from Book to Computer: A Case Study 1 Introduction 2 The “Elementary Transcendental Functions” 3 Codifying ln 4 Other Inverse Functions 5 The Case for ATAN2 6 Multivalued Functions 7 Couthness 8 Conclusion From Proof-Assistants to Distributed Libraries of Mathematics: Tips and Pitfalls 1 Introduction 2 Tips and Pitfalls 3 Further Discussion and Future Work 4 Conclusions Managing Digital Mathematical Discourse 1 MKM’s Intellectual Pedigree 2 Ontology Definition 3 The Digital Discourse 4 Ontology Development for Digital Mathematical Discourse 5 The Emkara Project 6 Conclusion and Future Work NAG Library Documentation 1 The NAG Library Documentation 2 Mathematical Fragments in SGML Documents 3 Classifying Mathematical Expressions 4 Classifying Function Arguments 5 Conclusions On the Roles of LATEX and MathML in Encodingand Processing Mathematical Expressions 1 Introduction 2 Syntax 3 Semantics 4 Formatting Quality 5 Macros and Transformations 6 Conclusions References Problems and Solutions for Markup forMathematical Examples and Exercises 1 Motivation 2 Preliminaries 3 Experiences with Representing Mathematical Documents 4 Conclusion An Annotated Corpus and a Grammar Model of Theorem Description 1 Introduction 2 Building a Corpus 3 Extraction of Grammar 4 Experiment 5 The Corpus Operation System 6 Conclusion A Query Language for a Metadata Framework about Mathematical Resources 1 Introduction 2 MathQL Level 1 3 Implementation and Testing References Information Retrieval in MML 1 Introduction 2 Mizar Articles and the Structure of MML 3 html Based Browsing 4 TextBased Searching 5 Semantics Based Retrieval 6 Conclusions References An Expert System for the Flexible Processing ofXml–Based Mathematical Knowledge in a Prolog–Environment 1 Introduction 2 Xml–Based Mathematical Knowledge 3 Xml and Prolog 4 Applications in an Expert System 5 Conclusions References Appendix Towards Collaborative Content Managementand Version Control for StructuredMathematical Knowledge 1 Introduction 2 An Infrastructure for Managing DistributedMathematical Knowledge Cooperatively 3 Computing Differences and Managing Change 4 Conclusion References On the Integrity of a Repository of FormalizedMathematics 1 Introduction 2 Lexical Integrity 3 Syntactic Integrity 4 Integrity of Notions 5 Formulating Theorems 6 Various Rough Edges 7 Conclusions References A Theoretical Analysis of Hierarchical Proofs 1 Introduction 2 Hierarchical Proofs 3 Initial Experiments 4 An Analysis over Cognitive Dimensions 5 Conclusions and Future Work References Comparing Mathematical Provers 1 Introduction 2 From Alfa to Ωmega: The Fifteen Provers of the World 3 Files Containing Mathematics 4 Differences in Logical Strength 5 Proof Checking or Theorem Proving 6 A Rather Subjective Two-Dimensional Diagram 7 Future Work References Translating Mizar for First Order TheoremProvers 1 Introduction, Previous Work 2 General Descriptions 3 Translation of Mizar Definitions 4 Redefinitions 5 Unimplemented Features of Mizar 6 Related and Future Work References The Mathematical Semantic Web 1 Introduction 2 RDF 3 OWL 4 XML Schema 5 Functions and Operators 6 XMLQuery 7 Success? References Author Index 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.