7. MKM / 14. Calculemus 2007:
Hagenberg,
Austria
Manuel Kauers, Manfred Kerber, Robert Miner, Wolfgang Windsteiger (Eds.):
Towards Mechanized Mathematical Assistants, 14th Symposium, Calculemus 2007, 6th International Conference, MKM 2007, Hagenberg, Austria, June 27-30, 2007, Proceedings.
Lecture Notes in Computer Science 4573 Springer 2007, ISBN 978-3-540-73083-5
Contributions to Calculemus 2007
- Mirian Andrés, Laureano Lambán, Julio Rubio:
Executing in Common Lisp, Proving in ACL2.
1-12
- Jacques Carette, William M. Farmer, Volker Sorge:
A Rational Reconstruction of a System for Experimental Mathematics.
13-26
- Amine Chaieb, Makarius Wenzel:
Context Aware Calculation and Deduction.
27-39
- Thierry Coquand, Arnaud Spiwack:
Towards Constructive Homological Algebra in Type Theory.
40-54
- James H. Davenport:
What Might "Understand a Function" Mean?
55-65
- William M. Farmer:
Biform Theories in Chiron.
66-79
- Predrag Janicic, Alan Bundy:
Automatic Synthesis of Decision Procedures: A Case Study of Ground and Linear Arithmetic.
80-93
- Cezary Kaliszyk, Freek Wiedijk:
Certified Computer Algebra on Top of an Interactive Theorem Prover.
94-105
- Elena Kartashova, Scott McCallum:
Quantifier Elimination for Approximate Factorization of Linear Partial Differential Operators.
106-115
- Songxin Liang, David J. Jeffrey:
Rule-Based Simplification in Vector-Product Spaces.
116-127
Contributions to MKM 2007
- Peter Murray-Rust:
Mathematics and Scientific Markup.
128-129
- Neil J. A. Sloane:
The On-Line Encyclopedia of Integer Sequences.
130
- Miguel A. Abánades, Jesús Escribano, Francisco Botana:
First Steps on Using OpenMath to Add Proving Capabilities to Standard Dynamic Geometry Systems.
131-145
- Andrea Asperti, Enrico Tassi:
Higher order Proof Reconstruction from Paramodulation-Based Refutations: The Unit Equality Case.
146-160
- David Aspinall, Christoph Lüth, Daniel Winterstein:
A Framework for Interactive Proof.
161-175
- Serge Autexier, Armin Fiedler, Thomas Neumann, Marc Wagner:
Supporting User-Defined Notations When Integrating Scientific Text-Editors with Proof Assistance Systems.
176-190
- Ewa Borak, Anna Zalewska:
Mizar Course in Logic and Set Theory.
191-204
- Simon Colton, Daniel Wagner:
Using Formal Concept Analysis in Mathematical Discovery.
205-220
- Pierre Corbineau, Cezary Kaliszyk:
Cooperative Repositories for Formal Proofs.
221-234
- Adam Grabowski, Christoph Schwarzweller:
Revisions as an Essential Tool to Maintain Mathematical Repositories.
235-249
- Klaus Grue:
The Layers of Logiweb.
250-264
- Feryal Fulya Horozal, Chad E. Brown:
Formal Representation of Mathematics in a Dependently Typed Set Theory.
265-279
- Fairouz Kamareddine, Robert Lamar, Manuel Maarek, J. B. Wells:
Restoring Natural Language as a Computerised Mathematics Input Method.
280-295
- Fairouz Kamareddine, Manuel Maarek, Krzysztof Retel, J. B. Wells:
Narrative Structure of Mathematical Texts.
296-312
- Andrea Kohlhase, Michael Kohlhase:
Re examining the MKM Value Proposition: From Math Web Search to Math Web Re Search.
313-326
- Gilbert Lee, Piotr Rudnicki:
Alternative Aggregates in Mizar.
327-341
- Robert Miner, Rajesh Munavalli:
An Approach to Mathematical Search Through Query Formulation and Data Normalization.
342-355
- Immanuel Normann, Michael Kohlhase:
Extended Formula Normalization for epsilon -Retrieval and Sharing of Mathematical Knowledge.
356-370
- Agnieszka Rowinska-Schwarzweller, Christoph Schwarzweller:
Towards Mathematical Knowledge Management for Electrical Engineering.
371-380
- Claudio Sacerdoti Coen, Stefano Zacchiroli:
Spurious Disambiguation Error Detection.
381-392
- Abdou Youssef:
Methods of Relevance Ranking and Hit-content Generation in Math Search.
393-406
Last update Tue Feb 14 04:07:46 2012
CET by the DBLP Team —
Data released under the ODC-BY 1.0 license — See also our legal information page