Supporting user-friendliness in the mathematical software system Theorema

Authors Koji Nakagawa
Title Supporting user-friendliness in the mathematical software system Theorema
Type PhD thesis
Address Linz, Austria
School Johannes Kepler University
Month April
Year 2002
SCCH ID# 229

The computer-support of the process of doing mathematics has significantly increased in the past few decades. And in the past few years it became clear that a next level of sophistication will be necessary and seems to be achievable that goes beyond the capabilities of current systems in a number of directions. In this thesis, we contribute to the one of such directions, the user-interfaces for such systems, i.e. we present various techniques that can contribute to making it easier and more attractive for the user of current and future mathematical software systems. The techniques that we propose in this thesis are:- the generation of natural language explanatory texts for theorem proving system,- tools for making it possible to generate spoken versions of mathematical formulae,- the technique of logicographic symbols, i.e. symbols that, at the same time, are completely formal and convey graphical intuition,- the communication of formal mathematical texts between various software systems.We implemented these various techniques in the frame of the Theorema system whose main goal is to provide a comprehensive frame for the entire process of doing mathematics.