Task 3.1 in the Calculemus Project: Automated Support to Writing Mathematical Publications

Task Description

Task 3.1 runs from month 12 till month 48. Goal of task 3.1 is to support the writing of mathematical publications.

Milestone 3.1 (month 24): Report on experiments on using the prototype systems as support for writing a mathematical subject.
Milestone 3.2 (month 42): Report and demo on experiments on using the prototype systems as support for writing a mathematical subject..

Partners and Involved Researchers

RISC: Task force leader

Bruno Buchberger (Project leader)
Tudor Jebelean (Co-investigator)
Wolfgang Windsteiger (Co-investigator)

USAAR: University of Saarbrücken

UWB: University of Bialystok

Young Researcher Active in Task 3.1

Adrian Craciun (RISC): pre-doctoral researcher at RISC from 09/2001 until 08/2002.
Josef Urban (Charles University) pre-doctoral resaercher at UWB from 02/2002 until 08/2002

Overview on the Task

The general goal in the frame of Task 3.1 is to design software systems to support the process of mathematical publications. Typically, a mathematical publication contains the following ingredients:

natural language text,
mathematical formulae,
formal text, i.e. definitions and theorems,
proofs,
examples, typically with computations,
graphics, tables, drawings, sketches, etc.

In the optimal case, a software system for supporting mathematical publications would support all the facets of mathematical publications listed above. The ratio, by which the individual ingredients contribute to a complete publication, depends of course on the content.

Presentations given at the Genova Meeting

Markus Moschner (USAAR)

OMDoc is a description language tailored for purposes appearing in symbolic sciences as logics, mathematics, computer science etc. Its specification aims not only for use in type setting, yet a substantial part supports automated data exchange by automated services like theorem provers and computer algebra systems. This comes along with a distinction between formal and informal content. OMDoc format is a specialized XML-format, thus making it well treatable for Internet users.

MBase is a knowledge management tool for mathematical content encoded in OMDoc format. Requests from automated services are supported via standardized interfaces (XMLRPC protocol).

With respect to Task 3.1 MBase and OMDoc may be used

as (distributed) repositories for mathematical knowledge which are used by an author for storing and retrieving publications; one is not restricted to a single MBase;
for unifying representation of different texts - this means presentation and code (only partially overlap with point 1); this can also mean a (parametrized) variation of proof granularity;
as tools for automated detection of proof obligations (projected with the integration of the Development Graph) - permitting support for elimination of gaps in publications.

For more detailed descriptions see MBase/OMDoc, MBase, and MathWeb.

Andrzej Trybulec (UWB)

UwB's contribution to the task consists in maintaining the technology adopted for publishing Mizar articles. The automated support for writing and publishing Mizar articles consists of:

The software used for writing and checking the correctness of Mizar articles (http://mizar.org/system/).
The software used for automatic translation and typesetting; the exportable parts of Mizar articles are automatically translated from Mizar into English and organized as a Latex source.

The resulting papers are first published electronically (http://mizar.org/JFM/), and then the paper edition follows (Formalized Mathematics, ISSN 0777-4028, published since 1990).

The plan for the future:

Both parts of the software provided are still evolving. The first part (the system for checking of Mizar articles) in the nearest future will be made stronger. That will enable writing proofs with the length closer to the length of proofs in informal mathematical publications. Nowadays, the de Bruijn factor is between 3 and 4. The second part still needs a lot of work. Particularly:

Better description of the environment in which the articles have been written.
Publication of proofs, probably after compression.

Wolfgang Windsteiger (RISC): Theorema as a Tool for Supporting Mathematical Publications

In the frame of the Theorema project, the Theorema software system is heavily used for formalizing mathematical subjects. The main work packages are:

the formal build-up of the theory of Hilbert spaces (work in progress) and
the book on Gröbner bases (started).

Furthermore, the Theorema system is also used for supporting mathematical lectures including the preparation of lecture notes. The main fields of application are:

lecture notes for "Algorithmic Methods" (emphasis on Theorema's computation capabilities) and
lecture notes for "Predicate Logic as a working language (emphasis on Theorema's proving capabilities).

Systems

Theorema, Mizar, OMDoc, MBase, MathWeb.

Industry Contacts

Wolfram Research.
Through close contact the Theorema group is influencing the development of the Mathematica software in order to include facilities which are useful for automatic reasoning, improved graphical interface, mathematical training, etc. RISC is official beta testers of versions 4 and 5 and also accredited Mathematica developers (access to the Mathematica Developers Kit).

Publications

B.Buchberger.

Logicographic symbols: A New Feature in Theorema.
In Symbolic Computation - New Horizons (Proceedings of the 4th International Mathematica Symposium, pages 23-30, Tokyo Denki University, Chiba Campus, Japan, June 25-27 2001. Tokyo Denki University Press.
ISBN 4-501-73020-X C3041.

F.Piroi and T.Jebelean.

Advanced Proof Presentation in Theorema.
Technical Report 01-20, RISC, RISC, Linz, Austria, 2001.
Presented at SYNASC 01: 3rd International Workshop on Symbolic and Numeric Algorithms for Scientific Computing, Timisoara, Romania, October 2-5, 2001.

A.Trybulec.
Formalized Mathematics.
ISSN 0777-4028, published since 1990.

W.Windsteiger.
Algorithmische Methoden 1.
Lecture Notes for lecture held in winter term 2001/02 at the University of Linz. To appear as RISC Report.

Talks

B.Buchberger, T.Jebelean
Predicate Logic as a Working Language Using Theorema.
Blocked course (12 hours), University of the West, Timisoara, Romania.

B.Buchberger.
The Didactics of Computer Mathematics.
Short course for high school students and teachers, Konan High School, Kobe, 2001.

B.Buchberger.
Mathematical Knowledge Management in Theorema.
1st International Workshop on Mathematical Knowledge Management, RISC, Johannes Kepler Universitaet, Schloss Hagenberg, 2001.

B.Buchberger, W.Windsteiger
Organized a training week on "Computer Supported Mathematical Proving" for high school teachers (October 8-12, 2001).