Proof Browsing
The structure of the proposed proof format admits the possibility of
proof browsing to increase readability.
A large proof containing many subproofs can appear daunting to a reader.
Rather than presenting the whole proof at once,
it can be initially presented with all its subproofs hidden.
If the reader is interested in a subproof, they can select the comment
that describes it.
The first layer of that subproof will then be revealed.
In this way the reader can see not only the individual steps of a proof,
but also the structure of the proof as a whole.
Furthermore, the reader need only reveal as much of the proof as is
necessary for them to be convinced of its validity.
The proof that k3 + k is even from
the section describing the structured proof format
is not large enough to require browsing;
nevertheless, we can use it to illustrate the concept.
The proof is presented again below, only now, the details of the subproof
it contains are hidden.
If you are interested in seeing the details of this subproof, you can
click on the comment that describes it
(the one that says `Simplify the right disjunct.').
Go ahead and try it out!
(When you click on the comment, the window will scroll so that the
first line of the subproof appears near the top of the screen.)
|
= |
{Extract the common factor.} |
|
= |
{Distribute even over ·.} |
|
|
even k \/
 even(k2 + 1)
|
|
= |
{Simplify the right disjunct.} |
 |
even(k2 + 1) |
|
= |
{Since even(i + 1) is ¬(even i).} |
|
= |
{The definition of square.} |
|
= |
{Distribute even over ·.} |
|
= |
{Disjunction is idempotent.} |
|
|
even k \/  ¬(even k)
|
|
= |
{The law of the excluded middle.} |
By clicking on the dot that marks the beginning of the subproof,
you can collapse its presentation and return to the original view.
A prototype tool has been built for creating web-browsable proofs like
the one above.
The input to the prototype is a single document which may contain several
proofs with accompanying text and graphics.
The output is a browsable document which may be viewed on the world web
web by an ordinary web browser (supporting Level 3.2 HTML).
By following the links in the web document,
the reader is able to browse the structure of the proofs it contains.
The mark-up language used to describe documents on the world wide web
does not currently support standard mathematical notation,
but future versions are expected to do so.
A Browsable Format for Proof Presentation: Proof Browsing /
Jim Grundy