KUMO(ID:3685/kum001)UCSD 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. Structures: Related languages
Resources
|