Introducing the ITP Tool: a Tutorial

We present a tutorial of the ITP tool, a rewriting-based theorem prover that can be used to prove inductive properties of membership equational specifications. We also introduce membership equational logic as a formal language particularly adequate for specifying and verifying semantic data structures, such as ordered lists, binary search trees, priority queues, and powerlists. The ITP tool is a Maude program that makes extensive use of the reflective capabilities of this system. In fact, rewritingbased proof simplification steps are directly executed by the powerful underlyingMaude rewriting engine. The ITP tool is currently available as a web-based application that includes a module editor, a formula editor, and a command editor. These editors allow users to create and modify their specifications, to formalize properties about them, and to guide their proofs by filling and submitting web forms.