default search action
6th MKM / 14th Calculemus 2007: Hagenberg, Austria
- Manuel Kauers, Manfred Kerber, Robert Miner, Wolfgang Windsteiger:
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
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.