ICMS 2014 Session: Software for Mathematical Theory Exploration

@ ICMS 2014


Bruno Buchberger, (www)
Wolfgang Windsteiger, (www)
Research Institute for Symbolic Computation
Johannes Kepler University
Linz / Schloss Hagenberg, Austria

Aim and Scope

In recent years, research groups all over the world have started to develop software for supporting the process of exploring mathematical theories in a structured way. (Other names for this area are: mathematical knowledge management, formal mathematics.) Progress in this area is based on advances in automated reasoning and improvements in software and web technology.

Research in this area has the potential to revolutionize the way how mathematical research, quality control in mathematics, archiving and dissemination of mathematical knowledge, application of mathematics and education in mathematics will be done in the future.

Topics (including, but not necessarily limited to)

This session is a forum for reporting on Examples of topics from these categories are



Talks and Abstracts

1. Mark Adams (Proof Technologies Ltd., UK)
Flyspecking Flyspeck [abstract]

2. Youngjoo Chung (Gwangju Institute of Science and Technology, Korea)
Symbolic Computing Package for Mathematica for Versatile Manipulation of Mathematical Expressions [abstract]

3. Mihnea Iancu, Michael Kohlhase, Corneliu Prodescu (Jacobs University Bremen, Germany)
Representing and Searching the Space of Mathematical Knowledge [abstract]

4. Patrick D. F. Ion (Mathematical Reviews [AMS] and University of Michigan at Ann Arbor, USA)
Early examples of software in mathematical knowledge management [abstract]

5. Michael Kohlhase (Jacobs University Bremen, Germany)
Discourse-level Parallel Markup and Adopting Meaning in Flexiformal Theory Graphs [abstract]

6. Wolfgang Windsteiger (RISC, JKU Linz, Austria)
Theorema 2.0: A System for Mathematical Theory Exploration [abstract]

7. Alexander Maletzky, Bruno Buchberger (RISC, JKU Linz, Austria)
Complexity Analysis of the Bivariate Buchberger's Algorithm in Theorema [abstract]

8. Wolfgang Windsteiger (RISC, JKU Linz, Austria), Manfred Kerber (University of Birmingham, UK), Colin Rowat (University of Birmingham, UK)
Formalizing a Key Theorem from Auction Theory using the Theorema System (Work in Progress) [abstract]