Kumo Generated Tatami Demos Homepage

The proofs linked to this page were all automatically generated by an early prototype of the Kumo system. They allow you to browse tatami proofs, but not to build them with Kumo; for more on Kumo, see the Kumo homepage.
Note: "Tatami" are natural fiber mats used in traditional Japanese homes. The size of a room is measured by the number of tatami on its floor, where each tatami is a rectangle, about 5 by 3 feet. Thus a 2 tatami room, like a 2 tatami proof, is pretty small, an 8 tatami room (or proof) is ok, but a 12 tatami room (or proof) is getting large, and should probably be subdivided.

Tatami are cool, refreshing and aromatic; we hope you find the tatami backgrounds helpful while browsing our proofs.

These demos assume familiarity with many (order) sorted algebra and with OBJ; without this background, you will not be able to understand the proofs. Suitable material can be found in the following two books: The coinduction proofs will also require familiarity with hidden (order) sorted algebra. See:

The following examples are currently available for browsing:
1. An inductive proof that 1+...+ n = n(n+1) / 2.
2. A coinductive proof of a behavioral property of a simple flag object.
3. A proof of behavioral correctness of array-with-pointer implementation of stack, using coinduction.
4. An inductive proof for lists that the reverse of the reverse of a list is the list, plus some lemmas, including that append is associative.
5. A behavioral refinement proof of the correctness of implementing sets with lists, using attribute coinduction.
6. An inductive proof of a formula for the sum of the squares of the first n natural numbers.
7. A coinductive correctness proof for the tatami protocol, which maintains the consistency of distributed cooperative proofs that are built using the tatami system.
Note: At this moment, examples 4, 6 and 7 are still in a preliminary form; in particular, we have not yet installed their homepages. Also, example 6 was produced by a now obsolete version of Kumo and therefore has somewhat different formats from the other examples.