Towards Mechanized Mathematical Assistants 14th Symposium, Calculemus 2007, 6th International Conference, MKM 2007, Hagenberg, Austria, June 27-30, 2007. Proceedings /

• Corporate Author: SpringerLink (Online service)
• Other Authors: Kauers, Manuel (Editor), Kerber, Manfred (Editor), Miner, Robert (Editor), Windsteiger, Wolfgang (Editor)
• Format: Electronic eBook
• Language: English
• Published: Berlin, Heidelberg : Springer Berlin Heidelberg, 2007.
• Series: Lecture Notes in Computer Science, 4573
• Subjects: Mathematics.; Computer communication systems.; Database management.; Data mining.; Artificial intelligence.; Algebra.; Artificial Intelligence (incl. Robotics).; Data Mining and Knowledge Discovery.; Information Systems Applications (incl. Internet).; Database Management.; Computer Communication Networks.

This volume contains the collected contributions of two conferences, Calcu- mus2007andMKM2007.Calculemus2007wasthe14thinaseriesofconferences dedicated to the integration of computer algebra systems (CAS) and automated deduction systems (ADS). MKM 2007 was the sixth International Conference on Mathem...

Table of Contents:

• Contributions to Calculemus 2007
• Executing in Common Lisp, Proving in ACL2
• A Rational Reconstruction of a System for Experimental Mathematics
• Context Aware Calculation and Deduction
• Towards Constructive Homological Algebra in Type Theory
• What Might “Understand a Function” Mean?
• Biform Theories in Chiron
• Automatic Synthesis of Decision Procedures: A Case Study of Ground and Linear Arithmetic
• Certified Computer Algebra on Top of an Interactive Theorem Prover
• Quantifier Elimination for Approximate Factorization of Linear Partial Differential Operators
• Rule-Based Simplification in Vector-Product Spaces
• Contributions to MKM 2007
• Mathematics and Scientific Markup
• The On-Line Encyclopedia of Integer Sequences
• First Steps on Using OpenMath to Add Proving Capabilities to Standard Dynamic Geometry Systems
• Higher order Proof Reconstruction from Paramodulation-Based Refutations: The Unit Equality Case
• A Framework for Interactive Proof
• Supporting User-Defined Notations When Integrating Scientific Text-Editors with Proof Assistance Systems
• Mizar Course in Logic and Set Theory
• Using Formal Concept Analysis in Mathematical Discovery
• Cooperative Repositories for Formal Proofs
• Revisions as an Essential Tool to Maintain Mathematical Repositories
• The Layers of Logiweb
• Formal Representation of Mathematics in a Dependently Typed Set Theory
• Restoring Natural Language as a Computerised Mathematics Input Method
• Narrative Structure of Mathematical Texts
• Reexamining the MKM Value Proposition: From Math Web Search to Math Web ReSearch
• Alternative Aggregates in Mizar
• An Approach to Mathematical Search Through Query Formulation and Data Normalization
• Extended Formula Normalization for ?-Retrieval and Sharing of Mathematical Knowledge
• Towards Mathematical Knowledge Management for Electrical Engineering
• Spurious Disambiguation Error Detection
• Methods of Relevance Ranking and Hit-content Generation in Math Search.