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:
- Homepage for hidden (order)
sorted algebra, which includes links to many relevant papers, such as Circular Coinductive
Rewriting, Behavioral
and Coinductive Rewriting, Circular Coinduction, A Protocol for Distributed Cooperative
Work, and Hiding More of
Hidden Algebra.
- Homepage for the BOBJ behavioral specification
language and rewriting system, which Kumo uses for both behavioral
specification and computation.
- On-line tutorial on hidden algebra,
induction, first order logic, etc. - however, this is now rather out of
date.
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:
- 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.)
- 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.
- 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.
- 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
.
- Here are the complete proofs for all three
inductive properties of lists, including the two lemmas needed to establish
the main goal.
- 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.
- A behavioral refinement proof of the correctness of
implementing sets with lists, using attribute coinduction.
- 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.
- 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