Hand Made Tatami Demos Homepage

The proofs linked to this page are "demos" in the sense that they illustrate the functionality of a system that is only partially built. These examples have been hand built to show what it is like to browse tatami proofs, though not what it is like to build them using the Kumo tool. For that, see the Kumo homepage and (to a lesser extent) the Kumo generated demo webpages. 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:
To the Links Project homepage.
For information on the CafeOBJ project, of which this is part.
To the UCSD Meaning and Computation Lab homepage.
3 May 1998