Mathematical Knowledge Management 4th International Conference, MKM 2005, Bremen, Germany, July 15-17, 2005, Revised Selected Papers /

This volume contains the proceedings of the Fourth International Conference on Mathematical Knowledge Management MKM 2005 held July 15–17, 2005 at - ternational University Bremen, Germany. Previous conferences have been at the Research Institute for Symbolic Computation (RISC) Linz, Austria (Septemb...

Πλήρης περιγραφή

Λεπτομέρειες βιβλιογραφικής εγγραφής
Συγγραφή απο Οργανισμό/Αρχή: SpringerLink (Online service)
Άλλοι συγγραφείς: Kohlhase, Michael (Επιμελητής έκδοσης)
Μορφή: Ηλεκτρονική πηγή Ηλ. βιβλίο
Γλώσσα:English
Έκδοση: Berlin, Heidelberg : Springer Berlin Heidelberg, 2006.
Σειρά:Lecture Notes in Computer Science, 3863
Θέματα:
Διαθέσιμο Online:Full Text via HEAL-Link
Πίνακας περιεχομένων:
  • Session I: Foundations
  • A Proof-Theoretic Approach to Hierarchical Math Library Organization
  • An Exploration in the Space of Mathematical Knowledge
  • Session II: Authoring
  • Authoring Presentation for openmath
  • Translating Mathematical Vernacular into Knowledge Repositories
  • Assisted Proof Document Authoring
  • Session III: Representations
  • A Tough Nut for Mathematical Knowledge Management
  • Textbook Proofs Meet Formal Logic – The Problem of Underspecification and Granularity
  • Processing Textbook-Style Matrices
  • Session IV: Proving
  • A Generic Modular Data Structure for Proof Attempts Alternating on Ideas and Granularity
  • Impasse-Driven Reasoning in Proof Planning
  • Literate Proving: Presenting and Documenting Formal Proofs
  • Session V: MKManagement Tools
  • Semantic Matching for Mathematical Services
  • Mathematical Knowledge Browser with Automatic Hyperlink Detection
  • A Database of Glyphs for OCR of Mathematical Documents
  • Session VI: Documents
  • Toward an Object-Oriented Structure for Mathematical Text
  • Explanation in Natural Language of ?????-Terms
  • Engineering Mathematical Knowledge
  • Session VII: MKM Case Studies
  • Computational Origami of a Morley’s Triangle
  • Designing Diagrammatic Catalogues of Types of Basic Interval Equation: A Case Study
  • Gröbner Bases — Theory Refinement in the Mizar System
  • Session VIII: Course Materials
  • An Interactive Algebra Course with Formalised Proofs and Definitions
  • Interactive Learning and Mathematical Calculus
  • Session IX: Migration
  • XML-izing Mizar: Making Semantic Processing and Presentation of MML Easy
  • Determining Empirical Characteristics of Mathematical Expression Use
  • Transformations of MML Database’s Elements
  • Translating a Fragment of Weak Type Theory into Type Theory with Open Terms.