H ? « ‹ ← → › »

Language peer sets for KUMO:
United States↑
United States/1997↑
Designed 1997 ↑
1990s languages ↑
Internet↑
New internationlism↑

KUMO(ID:3685/kum001)

alternate simple view
Country: United States
Designed 1997

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
OBJ3 → KUMO   Based on
KUMO → BOBJ   Target language for

Resources
Search in: Google  Google scholar  World Cat  Yahoo  Overture  DBLP  Monash bib  NZ  IEEE  ACM portal  CiteSeer  CSB  ncstrl  jstor  Bookfinder