Focus Windows: A New Technique for Proof Presentation
Bruno Buchberger
Proceedings of the Rhine Workshop on Computer Algebra, Mannheim, March 15,
41 pages.
ABSTRACT:
We first summarize our view of symbolic computation as a magma of provers, solvers,
and simplifiers (computers) w.r.t. various mathematical theories.
Then we concentrate on the technical and didactic aspect of presenting proofs
generated by (automated) provers in a form suitable for the check by human readers.
For this, we describe the technique of focus windows which we introduced in 2000
and which was recently implemented in our Theorema system by Florina Piroi.
By the focus window technique, in each step of a proof, the reader obtains
window that contains exactly those formulae that are relevent in this step. In more,
detail, in each step we first display an "attention window" that displays the current
proof goal and all the relevant formulae from the knowledge base that are used in
this proof step and, then, we display a "transformation window" that, in addition,
shows the new formulae generated in this step.
We illustrate the focus window technique by displaying a proof on equivalence relations
and partitions generated by the Theorema set theory prover both in the ordinary linear
representation and in the focus windows representation.
We conclude by sketching future improvements on the focus windows technique and some
theoretical implications.