This webpage describes the Maude Inductive Theorem Prover (ITP) and gives instructions for its use as well as a case study.
The most complete documentation of the tool, as well as the power list case study can be found in Joe Hendrix's thesis [1]. A shorter guide for the tool only is also available as a download below.
[1] J. Hendrix. Decision Procedures for Equationally Based Reasoning.
PhD thesis. Technical Report: UIUCDCS-R-2008-2999.
Download:
UIUC Technical Report
or PDF
Fischer-Ladner Prefix Sum Simple Example
Note that ITP requires a proper installation of Maude 2.4, available at maude.cs.uiuc.edu.
Copyright © 2008, University of Illinois
All rights reserved.