Kumo is a web-based proof assistant, having the following novel features:

• Kumo assists with proofs in first order hidden logic, using OBJ3 as a reduction engine. The most important inference rules in first order logic and hidden equational logic are implemented, including induction and coinduction.

• Kumo generates proof documentation for the web, combining proof browsing with background tutorials and explanantions, to improve the understandability of proofs.

• Kumo supports distributed cooperative proving. Users can send proof parts to the other members in the same group, and receive proof parts from them. All proof parts are saved in a distributed database, the consistency of which is maintained by Kumo.

To try Kumo in browser mode, click here.

History of Kumo

The development of Kumo is led by Professor Joseph Goguen, and has been helped by many people, including Dr. Akira Mori, Grigore Rosu, Bogdan Warinschi and Akiyoshi Sato. The implementation and much of the design have been done by Kai Lin.

The first prototype of Kumo was finished in 1997, and was used to generate several web based proofs, including design verification by coinductive refinement. The second version was developed in 1998; it implemented the Tatami protocol for supporting distributed cooperative proving. Also a primitive version of the proof script language Duck was introduced.

The third version is still under construction; an early prototype can be found in the download page of this site, or used interactively in browser mode over the web. Compared to previous versions, this has made the following improvements: A parser and code generator for the BOBJ language are implemented, the Duck langage is redesigned, and the automatic capability proof is much enhanced. Inside Kumo, XML proof presentations are first generated, then the HTML files are created using XSL style sheets. Therefore proof websites can be easily reconfigured by changing the XSL style sheets.

A more detailed overview with some references is available at here.

Who Are We ?

We are the Meaning and Computational Lab, in the Department of Computer Science and Engineering at the Univeristy of California at San Diego. Currently the lab has the following members:

• Joseph Goguen, Professor of Computer Science & Engineering, UCSD. Project leader.
• Kai Lin, PhD Student. Implementing the Kumo system
• Grigore Rosu, PhD Student. Working on specification and verification of the tatami protocol, higher order views and modules, and theory of hidden algebra.
• Bogdan Warinschi, PhD Student. Working on concurrency in hidden algebra

More information about research in our lab is available at the lab homepage.

We appreciate your comments to help us to improve Kumo, and we will try to answer your questions. Please send questions about using Kumo to klin@ucsd.edu, and more general questions to goguen@cs.ucsd.edu.

17 November 1999