Maude ITP

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


ITP tutorial

ITP tool

Powerlist case study

Fischer-Ladner Prefix Sum Simple Example

Note that ITP requires a proper installation of Maude 2.4, available at


Joe Hendrix
José Meseguer
Ralf Sasse

Copyright © 2008, University of Illinois
All rights reserved.

Last modified: Mon Mar 16 13:16:33 CET 2009