The ITP Tool
An Inductive Theorem Prover Tool for Maude Membership Equational Specifications

The ITP tool is an inductive theorem prover for proving properties of Maude functional modules, i.e., specifications in membership equational logic with an initial algebra semantics.
The ITP tool has been written entirely in Maude and is in fact an executable specification in rewriting logic of the formal inference system that it implements. This document presents the main features of the ITP tool and describes how to obtain and install it, and how to use it effectively.

Maude Specifications and Samples

• Getting the ITP Tool

  Download and unpack itp-tool.tar.gz.. The tar file contains the following:
  • README file;
  • Changes index with latest changes;
  • itp-tool Maude module, implementing the ITP tool;
  • itp-tool-aux Maude module, imported by itp-tool
  • itp-tactics Maude module, imported by itp-tool
  • meta-prelude Maude module, imported by itp-tactics
  • itp-rules Maude module, implementing the ITP inference system
  • examples/ subdirectory, containing the proof examples;
  • docs/ subdirectory, containing the files needed to create a a version of this manual;

  An online reference manual, the compressed tar file of the ITP sources, related files, updates and patches are also posted on the ITP server at http://sophia.unav.es/~clavel/itp/.





• Requirements

  The ITP tool is written entirely in Maude. To use ITP you need Maude version 1.0.3 or later.




• Instructions

  Load full-maude.maude and then itp-tool. Then start the loop (loop init .). The tool is now ready for entering examples. For more details see the ITP Manual.

• The postscript version of the manual is available at itp-manual.ps. By Manuel Clavel. Department of Philosophy. University of Navarre. August 2000.
  An online online reference manual with installation info, a tutorial, and grammar definition is available on the ITP webpage in Spain.