Skip to main content
  • Conference proceedings
  • © 2011

Intelligent Computer Mathematics

18th Symposium, Calculemus 2011, and 10th International Conference, MKM 2011, Bertinoro, Italy, July 18-23, 2011, Proceedings

  • Up-to-date results
  • Fast-track conference proceedings
  • State-of-the-art research

Part of the book series: Lecture Notes in Computer Science (LNCS, volume 6824)

Part of the book sub series: Lecture Notes in Artificial Intelligence (LNAI)

Conference series link(s): CICM: International Conference on Intelligent Computer Mathematics

Conference proceedings info: CICM 2011.

Buy it now

Buying options

eBook USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Other ways to access

This is a preview of subscription content, log in via an institution to check for access.

Table of contents (30 papers)

  1. Front Matter

  2. Calculemus 2011

    1. Enumeration of AG-Groupoids

      • Andreas Distler, Muhammad Shah, Volker Sorge
      Pages 1-14
    2. Incidence Simplicial Matrices Formalized in Coq/SSReflect

      • Jónathan Heras, María Poza, Maxime Dénès, Laurence Rideau
      Pages 30-44
    3. Proof Assistant Decision Procedures for Formalizing Origami

      • Cezary Kaliszyk, Tetsuo Ida
      Pages 45-57
    4. Using Theorema in the Formalization of Theoretical Economics

      • Manfred Kerber, Colin Rowat, Wolfgang Windsteiger
      Pages 58-73
    5. View of Computer Algebra Data from Coq

      • Vladimir Komendantsky, Alexander Konovalov, Steve Linton
      Pages 74-89
    6. Computer Certified Efficient Exact Reals in Coq

      • Robbert Krebbers, Bas Spitters
      Pages 90-106
    7. A Foundational View on Integration Problems

      • Florian Rabe, Michael Kohlhase, Claudio Sacerdoti Coen
      Pages 107-122
    8. Efficient Formal Verification of Bounds of Linear Programs

      • Alexey Solovyev, Thomas C. Hales
      Pages 123-132
  3. Mathematical Knowledge Management 2011

    1. Large Formal Wikis: Issues and Solutions

      • Jesse Alama, Kasper Brink, Lionel Mamane, Josef Urban
      Pages 133-148
    2. Licensing the Mizar Mathematical Library

      • Jesse Alama, Michael Kohlhase, Lionel Mamane, Adam Naumowicz, Piotr Rudnicki, Josef Urban
      Pages 149-163
    3. Workflows for the Management of Change in Science, Technologies, Engineering and Mathematics

      • Serge Autexier, Catalin David, Dominik Dietrich, Michael Kohlhase, Vyacheslav Zholudev
      Pages 164-179
    4. Parsing and Disambiguation of Symbolic Mathematics in the Naproche System

      • Marcos Cramer, Peter Koepke, Bernhard Schröder
      Pages 180-195
    5. Interleaving Strategies

      • Bastiaan Heeren, Johan Jeuring
      Pages 196-211
    6. Combining Source, Content, Presentation, Narration, and Relational Representation

      • Fulya Horozal, Alin Iacob, Constantin Jucovschi, Michael Kohlhase, Florian Rabe
      Pages 212-227
    7. Indexing and Searching Mathematics in Digital Libraries

      • Petr Sojka, Martin Líška
      Pages 228-243
    8. Isabelle as Document-Oriented Proof Assistant

      • Makarius Wenzel
      Pages 244-259
    9. Towards Formal Proof Script Refactoring

      • Iain Whiteside, David Aspinall, Lucas Dixon, Gudmund Grov
      Pages 260-275

Other Volumes

  1. Intelligent Computer Mathematics

About this book

This book constitutes the joint refereed proceedings of three international events, namely the 18th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning, Calculemus 2011, the 10th International Conference on Mathematical Knowledge Management, MKM 2011, and a new track on Systems and Projects descriptions that span both the Calculemus and MKM topics, all held in Bertinoro, Italy, in July 2011. All 51 submissions passed through a rigorous review process. A total of 15 papers were submitted to Calculemus, of which 9 were accepted. Systems and Projects track 2011 there have been 12 papers selected out of 14 submissions while MKM 2011 received 22 submissions, of which 9 were accepted for presentation and publication. The events focused on the use of AI techniques within symbolic computation and the application of symbolic computation to AI problem solving; the combination of computer algebra systems and automated deduction systems; and mathematical knowledge management, respectively.

Editors and Affiliations

  • Departments of Computer Science and Mathematics Sciences, University of Bath, United Kingdom

    James H. Davenport

  • Department of Computing and Software, McMaster University, Hamilton, Canada

    William M. Farmer

  • Institute for Computing and Information Sciences, Radboud University, Nijmegen, The Netherlands

    Josef Urban

  • Department of Computer Science, Jacobs University Bremen, Bremen, Germany

    Florian Rabe

Bibliographic Information

Buy it now

Buying options

eBook USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Other ways to access