=ADD=
=reftype=
14
=number=
02-01
=url=
ftp://ftp.risc.uni-linz.ac.at/pub/techreports/2002/02-01.ps.gz
=year=
2002
=month=
01
=author=
Nakagawa; Koji
=title=
Supporting User-Friendliness in the Mathematical Software System Theorema
=abstract=
This doctoral thesis with the short title "Mathematics as Pictures" (and the
long title "Supporting User-Friendliness in the Mathematical Software System
Theorema") builds on ideas and was written under the guidance of Professor
Bruno Buchberger at the Research Institute for Symbolic Computation (RISC),
Johannes Kepler University of Linz, Austria.

For many people, mathematics is nothing than horrifying "formulae rubbish"
although many people like to play with mathematical objects, figures, pictures
etc. Also, many people understand well the essence of mathematical problems
and their solutions when presented in graphical form and, then, also appreciate
the importance of the solutions provided by mathematics. For example, it is
clear that one must carefully analyze the possible configurations of robots
and the configurations of objects to be manipulated by robots in order to be
able to develop methods by which robots can be controlled in such a way that
they do what we want them to do. "A picture says more than 1000 words" and, in
fact, often "a picture says more than 1000 formulae".

Well chosen pictures make it easy to understand and grasp the essence of even
complicated situations. On the other hand, unfortunately, pictures can only
illustrate individual concrete situations while the mechanical treatment of
all possible situations by a computer program, internally, can only be
described by formulae (laws, rules) that contain "variables" as placeholders
for concrete objects. In other words, computers cannot compute with "pictures".


In this thesis, for the first time, methods are presented and developed in
detail by which arbitrary mathematical situations can be represented in a kind
of pictorial language rather than by formulae. The methods presented in the
thesis are such that, on the one hand, the users can think and speak in the
pictorial language while, on the other hand, internally the computer can work
with the translations of the pictorial language to the usual mathematical
language of formulae. The methods were realized in the frame of a new
mathematical software system, "Theorema", which is currently developed by the
Theorema Working Group at RISC. This system, in addition to being able to
compute with formulae, can also prove and simplify formulae automatically.

The pictorial language presented in this thesis, in a certain sense, further
develops the old hieroglyphic languages like the Japanese kanji system and
combines them with modern logic languages. It is to be expected that this new
pictorial language will significantly change the way how mathematics can be
taught, learned and understood.
=note=
PhD Thesis
=sponsor=
RISC PhD program, RISC FWF SFB F013, Software Competence Hagenberg (SCCH)
=keywords=
integrated mathematical system, automated theorem proving, Theorema,
user-friendliness, proof presentation in natural languages, inventing new
notation, logicographic symbol, external interface