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

Contributions to Calculemus 2007
Executing in Common Lisp, Proving in ACL2   Mirian Andres   Laureano Lamban   Julio Rubio     1
A Rational Reconstruction of a System for Experimental Mathematics   Jacques Carette   William M. Farmer   Volker Sorge     13
Context Aware Calculation and Deduction   Amine Chaieb   Makarius Wenzel     27
Towards Constructive Homological Algebra in Type Theory   Thierry Coquand and Arnaud Spiwack     40
What Might "Understand a Function" Mean?   James H. Davenport     55
Biform Theories in Chiron   William M. Farmer     66
Automatic Synthesis of Decision Procedures: A Case Study of Ground and Linear Arithmetic   Predrag Janicic   Alan Bundy     80
Certified Computer Algebra on Top of an Interactive Theorem Prover   Cezary Kaliszyk   Freek Wiedijk     94
Quantifier Elimination for Approximate Factorization of Linear Partial Differential Operators   Elena Kartashova   Scott McCallum     106
Rule-Based Simplification in Vector-Product Spaces   Songxin Liang   David J. Jeffrey     116
Contributions to MKM 2007
Mathematics and Scientific Markup   Peter Murray Rust     128
The On-Line Encyclopedia of Integer Sequences   Neil J.A. Sloane     130
First Steps on Using OpenMath to Add Proving Capabilities to Standard Dynamic Geometry Systems   Miguel A. Abanades   Jesus Escribano   Francisco Botana     131
Higher Order Proof Reconstruction from Paramodulation-Based Refutations: The Unit Equality Case   Andrea Asperti   Enrico Tassi     146
A Framework for Interactive Proof   David Aspinall   Christoph Luth   Daniel Winterstein     161
Supporting User-Defined Notations When Integrating Scientific Text-Editors with Proof Assistance Systems   Serge Autexier   Armin Fiedler   Thomas Neumann   Marc Wagner     176
Mizar Course in Logic and Set Theory   Ewa Borak   Anna Zalewska     191
Using Formal Concept Analysis in Mathematical Discovery   Simon Colton   Daniel Wagner     205
Cooperative Repositories for Formal Proofs   Pierre Corbineau   Cezary Kaliszyk     221
Revisions as an Essential Tool to Maintain Mathematical Repositories   Adam Grabowski   Christoph Schwarzweller     235
The Layers of Logiweb   Klaus Grue     250
Formal Representation of Mathematics in a Dependently Typed Set Theory   Feryal Fulya Horozal   Chad E. Brown     265
Restoring Natural Language as a Computerised Mathematics Input Method   Fairouz Kamareddine   Robert Lamar   Manuel Maarek   J.B. Wells     280
Narrative Structure of Mathematical Texts   Fairouz Kamareddine   Manuel Maarek   Krzysztof Retel   J.B. Wells     296
Reexamining the MKM Value Proposition: From Math Web Search to Math Web ReSearch   Andrea Kohlhase   Michael Kohlhase     313
Alternative Aggregates in Mizar   Gilbert Lee   Piotr Rudnicki     327
An Approach to Mathematical Search Through Query Formulation and Data Normalization   Robert Miner   Rajesh Munavalli     342
Extended Formula Normalization for [epsilon]-Retrieval and Sharing of Mathematical Knowledge   Immanuel Normann   Michael Kohlhase     356
Towards Mathematical Knowledge Management for Electrical Engineering   Agnieszka Rowinska-Schwarzweller   Christoph Schwarzweller     371
Spurious Disambiguation Error Detection   Claudio Sacerdoti Coen   Stefano Zacchiroli     381
Methods of Relevance Ranking and Hit-Content Generation in Math Search   Abdou S. Youssef      393
Author Index     407