Library Home || Full Table of Contents || Library Help
|Joseph Goguen et al.; University of California at San Diego.|
|A Web-based proof assistant that 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 and supports distributed cooperative proving.|
|Resource Types:||Topic Tools Miscellaneous, Web Interactive/Java|
© 1994- The Math Forum at NCTM. All rights reserved.