Kumo Generated Proof Websites

The proof websites listed below were all generated by Kumo; more are gradually being added. You can browse these proofs with any recent generation web browser, but you cannot build proofs in this mode. Also, you should develop some familiarity with order sorted algebra, OBJ, hidden algebra, and BOBJ; background on the first two topics can be found in the following: Detailed information on hidden algebra and BOBJ can be found in the following: The most recent description of Kumo may be found in The examples below are chosen and ordered to form a tutorial on Kumo and its underlying mathematics, so it is best to read them in the given order, and to read all of the explanations that go with each one:
  1. An inductive proof that 1+...+ n = n(n+1) / 2. This will give you a chance to explore Kumo's navigation and display conventions on a simple example. (Click on the "question mark" icon for navigation instructions.)
  2. A coinductive proof of a behavioral property of a simple flag object. This illustrates some basics of the hidden algebra approach on a very simple example; it includes an especially clear explanation of the need for behavioral properties.
  3. Two proofwebs for some familiar inductive properties of lists. The first was generated by a duck score written at the beginning of this effort; it is striking that the lemmas needed to complete the proof can be deduced from the way that successive proof attempts fail. The second proofweb succeeds, and was generated by a duck score derived from the first just by reordering its goals so that the lemmas that were found necessary are proved first.
    1. This early attempt at proving that the reverse of the reverse of a list is the original list, takes a direct approach, and its explanations emphasize the way that the two lemmas that are needed to complete the proof can be deduced from the output produced by unsuccessful proof attempts; one of these lemmas is the associativity of append.
    2. Here are the complete proofs for all three inductive properties of lists, including the two lemmas needed to establish the main goal.
  4. A coinductive proof of the behavioral correctness of the array-with-pointer implementation of stack. This behavioral refinement proof requires introducing a non-trivial lemma, which can also be inferred from a prior proof attempt that fails without it.
  5. A behavioral refinement proof of the correctness of implementing sets with lists, using attribute coinduction.
  6. A simple inductive proof of a formula for the sum of the squares of the first n natural numbers. This example is deliberately very spare, and in particular has no explanations, in order to illustrate the default conventions that Kumo uses when a user supplies only the absolute minimum input.
  7. A detailed proof that the square root of 2 is irrational, illustrating the first order capabilities of Kumo. Note that this uses and proves many auxiliary lemmas; see the directory listing. Note: no explanations have as yet been provided for any of these proofs.
We hope you will enjoy this experience. Your feedback is very welcome: please send comments on the implementation to the implementer, Kai Lin, and comments on the explanations and the theory to Joseph Goguen. For more on Kumo, see the Kumo homepage.
To the Kumo homepage.
To the Tatami Project homepage.
To the UCSD Meaning and Computation Lab homepage.
Maintained by Joseph Goguen
Last modified: Wed Jan 2 21:06:43 PST 2002