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.
References in zbMATH (referenced in 6 articles )
Showing results 1 to 6 of 6.
- Seino, Takahiro; Ogata, Kazuhiro; Futatsugi, Kokichi: A toolkit for generating and displaying proof scores in the OTS/CafeOBJ method. (2006)
- Ogata, Kazuhiro; Futatsugi, Kokichi: Rewriting-based verification of authentication protocols (2004)
- Goguen, Joseph A.; Lin, Kai: Web-based support for cooperative software engineering (2001)
- Buss, Samuel R.; Rosu, Grigore: Incompleteness of behavioral logics. (2000)
- Goguen, Joseph: Tossing algebraic flowers down the great divide (1999)
- Goguen, Joseph A.; Malcolm, Grant: Hidden coinduction: Behavioural correctness proofs for objects (1999)