User Interface

The effective use of an interactive theorem proving system depends not least on the capabilities of its user interface. A major problem is the adequate access to the overwhelming amount of information manipulated by these systems. This requires structure-oriented overview facilities, and selective and precise content-oriented display. Some design principles for graphical user interfaces of semiautomated theorem provers:

Multi-Modal Visualization: In any proof state the system should display the proof information to the user at different levels of abstraction and detail and furthermore in different modes (e.g.\ as the graphical representation of a proof tree, as a linearized proof, or in verbalization mode).
LOUI provides different and complementary views of a proof such as a graphical display or a linearized proof. The traditional graphical tree representation of the proof is enhanced by dedicated browsers for selected textual information and intensive use is made of hypertext techniques in order to illustrate connections between physically distant, but logically related portions of proofs in both the text-based and the graphical modes.
To add a natural language view of proofs, LOUI calls the proof presentation system that structures and verbalizes proofs in natural language.
Lean Processing: The interface should work reasonably fast, and its installation in other environments should be possible with minimal effort and storage requirements.
This has led to a distributed system architecture of LOUI/OMEGA, where LOUI is realized as an autonomous software agent in MathWeb, which can be sent over the Internet as an applet while the OMEGA server resides on a dedicated host. Since LOUI is an autonomous agent, it maintains its own representation of the proof state and autonomously computes the visualization information by using local computational resources, thus reducing the communication bandwidth to a minimum. Thus the architecture inherits the advantage from two kinds of setup: From one, where the whole deduction system is installed locally on the client machine (local computation) as well as from one, where the logical and graphical computations are centralized on a server the user communicates with, say, by a remote X connection. This enables the realization of the concept of direct manipulatio, which allows for immediate feed-back and a minimal time a user has to wait until an action takes effect. Direct manipulation is supported since LOUI can react to many forms of user interaction immediately by manipulating its internal representation of the proof state rather than calling the server.
Anticipation: The system should minimize the necessary interaction with the user by suggesting commands and parameters at each proof step. Optimally, the system should be able to do the straightforward steps autonomously.
Anticipation to minimize user interaction, has always been a concern of interactive systems, for instance by disabling commands that are nonsensical (i.e. pre-selecting legal actions) or generating lists of commands that are advisable in a current situation. In LOUI's internal representation of the proof state, many interface-related reasoning tasks can be performed without the help of the underlying proof system. For example, LOUI supports and complements the agent-based command suggestion mechanism provided by its host system OMEGA.

See also the homepage of the LOUI project.