7. MKM / 14. Calculemus 2007: Hagenberg, Austria

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