Editorial
Authors: Backhouse Roland 
Published: August 2002

Thirty years ago, at the time that the development of theorem proving software
first began, computer technology was far less advanced than it is now. It was
still not unknown, for example, for computer programs to be prepared on paper
tape, punch cards being the preserve of the more affluent establishments. It is not
surprising, therefore, that the early computer systems were for expert users only,
and systems offering support for theorem proving (and automating mathematics
in general) paid no attention to the interface with the human user.

The technological advances that have been made since then are mind-boggling. Most recently, the technology of human-computer interactions has progressed in leaps and bounds, bringing everyday computer usage at long last to the man on the street. Software for theorem proving has also made substantial progress, but the interfaces with the user have not kept pace and are most often still based on teletype technology. Thanks to the Internet, the world may be at your feet, but ergonomic interaction with automated mathematics is still way up in the clouds!

A series of workshops on User Interfaces and Theorem Provers was begun in 1995 in recognition of the fact that the difficulty in using powerful theorem proving software frequently lies with a poor user interface. The workshop has now been held on four successive occasions, at the University of Glasgow, at the University of York, at INRIA Sophia Antipolis and at Eindhoven University of Technology.

The goal of these workshops was to stimulate discussion on the design of user interfaces for theorem provers based on actual experimentation with real-life systems and to feed that discussion back into further development.

The current collection of papers is intended to be representative of the lasting achievements brought about by these workshops. Although but a small sample (six papers out of approximately fifty presented at the workshops) the papers span a great diversity of issues. What is immediately evident, when reading through them, is that recognition of the paramount need for good user interfaces for theorem provers (so aptly expressed in the title of the 1992 paper by Thiery, Bertot and Kahn –“Real Theorem Provers Deserve Real User-Interfaces”) is now widespread. What is also evident, however, is that a consensus on good design principles is still a long way off. Should we, to take just one example, strive for a minimalist interface that promotes a simple user's mental model as advocated by Bornat and Sufrin, or is multi-modal visualization of proof states desirable, as advocated by Siekmann et al.?

This collection of papers will, I sincerely hope, provide a stimulating and informative basis for further discussion of the many issues involved. There remains much to be done before automated theorem proving can truly claim to have made the transition from the problem space to the solution space, and the user interface is (in my view, at least) the key to doing so!

I would like to conclude by extending my thanks to those who preceded me in organising the UITP workshops: Phil Gray, Tom Melham, Muffy Thomas and Stuart Aitken, who organised the very first workshop, Nick Merriam, Michael Harrison, Andy Dearden and Yves Bertot, who organised the subsequent two workshops. My thanks also to the referees for their cooperation and willingness to work to tight deadlines.