ICMS 2014 Session: Software for Mathematical Theory Exploration

@ ICMS 2014

Organizers

Organizer:: Bruno Buchberger, (www)
Co-Organizer:: 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

new features and techniques in existing systems for mathematical theory exploration,
new systems for mathematical theory exploration, or
major case studies in mathematical theory exploration and its applications.

Examples of topics from these categories are

applications of theory exploration in mathematics education,
development and assessment of tools for structuring large theories,
graphical and organizational tools for visualization of theories and their dependencies,
application of theory exploration in semantic web technologies,
application of theory exploration in mathematical finance and economy,
application of theory exploration in medical information systems,
implications of theory exploration for the future of mathematical publishing,
implications of theory exploration for archiving and quality control in mathematics,
special reasoning techniques for special mathematical theories (e.g. inductive theories, set theory, computer algebra algorithms),
application of theory exploration in software science (e.g. algorithm verification and/or synthesis),
application of theory exploration for abstract sytate machine analysis,
application of theory exploration in model checking,
application of theory exploration in the development of Wolfram-Alpha-like web services,
applications in math text book writing and preparing lecture notes,
etc., etc.

Publication

A short abstract will appear on the permanent conference web page as soon as accepted.
An extended abstract will appear on the permanent conference web page as soon as accepted. It will also appear on the proceedings that will be distributed during the meeting.
A special issue of the Journal of Symbolic Computation (JSC) consisting of full papers will be organized immediately after the meeting.

Submission

If you would like to give a talk at ICMS, you need to submit first a short abstract and then later an extended abstract. See the guideline for the details.
After the meeting, the submission guidelines for a journal special issue will be communicated to you by the session organizers.

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]