The ITP Tool's Manual
Manuel Clavel, Miguel Palomino · 2005
The ITP tool is an experimental inductive theorem prover for proving properties of Maude equational specifications, 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 of the formal inference system that it implements.