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".