Focus Windows:
A New Technique for Presenting Mathematical Proofs
(in Automated Theorem Proving Systems)

Bruno Buchberger

Theorema Technical Report, 2000-01-30, Research Institute for Symbolic
Computation, Johannes Kepler University, A4040 Linz, Austria, 19 pages.



ABSTRACT:

We describe a new technique for presenting proofs, in particular proofs generated by 
automated theorem proving systems like THEOREMA". We call this technique 
"focus windows" technique because with this technique, in each proof step, all the relevant
formulae are collected in one window (the "focus window") so that the reader can focus 
on them. The sequence of focus windows alternates between "attention windows" and 
"transformation windows". In an attention window, exactly those formulae are displayed - 
and highlighted - that  are relevant for the next proof step. In the subsequent transformation 
window, in addition to the highlighted formulae, the formulae are displayed that are added 
as a goal or additional knowledge. Also, a standard natural language text is presented that 
briefly characterizes the proof technique used.  

Although the paper presents the idea in terms of THEOREMA", the presentation method 
is applicable to arbitrary automated theorem proving systems that produce proofs as 
sequences of proof situations consisting of "goals" and "available knowledge".