The style guidelines below have been developed for the proof websites
generated by Kumo, with the aim of making proofs much easier to understand
than is usual. To clarify the discussion, we distinguish between *abstract
proofwebs* and *display proofwebs*; the first contains only proof
information, while the second also includes display information. We will use
the word *unit* for any block of information of the same kind within a
display proofweb.

- A
*homepage*is provided for each major proof part; these serve to introduce and motivate the problem to be solved and the approach taken to the solution. -
*Tatami pages*are the basic constituents of display proofwebs; each tatami page has one or more*proof units*showing its inference rule applications, interleaved with one or more explanation units; it is feasible to have both on the same web page because there should only be a small number of proof steps per page (about 7 non-automatic rules works well). Tatami pages are also called "proof pages." - The
*explanation units*of tatami pages are prover-supplied informal discussions of proof concepts, strategies, obstacles, etc.; these may contain graphics, applets, and of course text. - Tatami pages can be browsed in an order designed by the prover to be
helpful and interesting to the reader; if possible, these pages should tell a
story about how obstacles were overcome (or still remain); this order will be
called the
*narrative order*. (See*Notes on Narrative*for more information on the theory of narrative used here.) - Major proof parts, including lemmas, have their own subwebsites, each with the same structure as the main proof, including homepage and explanation units. These appear in a separate dedicated persistent popup window.
- Tatami pages also have associated formal proof scores, which appear in another separate popup window when summoned from a tatami page. It is convenient to have a separate window because users usually want to look at the proof and explanation at the same time as the proof score. Readers can also request proof score execution, and the result is then displayed in the same window as the score, so that one can easily alternate between them. (The proof score is sent to an OBJ server and the result is returned for display.)
- Major proof parts can have an optional closing page, to sum up important results and lessons; these appear in the same window as their tatami pages.
- Formal proof steps are automatically linked to pre-existing tutorial background pages; e.g., each application of induction is linked to a webpage that explains the kind of induction used. Tutorial pages have their own dedicated persistent popup window.
- A menu of open subgoals appears on each homepage, and error messages are placed on appropriate pages. In database mode, a summary of this information may be seen in the status window, which is a specialized popup that reports any currently open subgoals.

The above material was taken from the overview paper

To the Tatami project homepage

Last modified: Thu Sep 27 11:24:11 PDT 2001