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...
Συγγραφή απο Οργανισμό/Αρχή: | |
---|---|
Άλλοι συγγραφείς: | |
Μορφή: | Ηλεκτρονική πηγή Ηλ. βιβλίο |
Γλώσσα: | 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.