SPECIAL ISSUE IN THE JOURNAL OF APPLIED LOGIC

Guest Editor: Christoph Benzmüller, Saarland University, Saarbrücken, Germany

Date of Appearance: presumably still in 2005

Content of the Special Issue

Please see the editorial for this special for an overview on the articles.

About This Special Issue

The year 2004 marks the fiftieth birthday of the first computer generated proof of a mathematical theorem: “the sum of two even numbers is again an even number” (with Martin Davis' implementation of Presburger Arithmetic in 1954).

While Martin Davis and later the research community of automated deduction used machine oriented calculi to find the proof for a theorem by automatic means, the Automath project of N.G. de Bruijn – more modest in its aims with respect to automation – showed in the late 1960s and early 70s that a complete mathematical textbook could be encoded and proof-checked by a computer.

Modern interactive proof assistants divide the task of proving a theorem between the human and the computer, and they have been developed for applications in formal methods and mathematics. While these systems are very successful in formal methods, actual pragmatics of mathematics is unfortunately still to be characterized as mainly pen and paper based. A new generation of mathematical software systems is thus required to improve the situation. These systems shall provide integrated computer-based support for most working tasks of a mathematician – including computation, reasoning, mathematical knowledge representation and management, and publication – as well as for formal methods in computer science.

In contrast to the paradigm of classical, fully automated theorem proving, mathematics assistance systems (MAs) aim at a fruitful teamwork between the mathematician and the computer by providing adequate interaction languages and means. They do not want to replace the mathematician but to support him in various aspects:

• MAs should be capable of tackling minor, simple subtasks fully automatically such that the mathematician can better concentrate on major, non-trivial tasks requiring creativity and ingenuity;
• therefore MAs should integrate a wide range of specialized mathematical support tools (including classical automated theorem provers, computer algebra systems, model generators, constraint solvers, etc.) and best provide uniform interfaces to them;
• MAs should ideally be coupled with publication oriented mathematical editing tools such that the developments in an MA can be easily turned into proper mathematical publications;
• moreover MAs should support the formal verification of mathematical texts;
• MAs should be linked with structured mathematical knowledge repositories (which are probably distributed in the Internet) and provide sophisticated mechanisms for the retrieval and management of mathematical knowledge;
• MAs should be coupled with mathematical e-learning environments;
• etc.

This special issue aims to provide an overview on the methodology, the design, and the achievements of today's leading mathematics assistance systems. It also wants to provide short outlooks to the future of these systems and stimulate a discussion on how their acceptance in practice of mathematics can be improved.

The Journal of Applied Logic

The Journal of Applied Logic publishes papers in areas of logic which can be applied in other disciplines as well as application papers in those disciplines, the unifying theme being logics arising from modeling the human agent.

About This Document

This document has been created with TeXmacs which is a powerful WYSIWYG mathematical text-editor meanwhile used also as an interface to MAs (e.g. by OMEGA and Coq). TeXmacs supports translation into HTML, PDF, PS, XML, LaTeX, etc. and this feature has been employed to generate different CfP-documents based on a single source file.