Sciweavers

JUCS
2006

Introducing the ITP Tool: a Tutorial

13 years 10 months ago
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 underlying Maude 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. Key Words: inductive theorem proving, semantic data structures, membership equational l...
Manuel Clavel, Miguel Palomino, Adrián Ries
Added 13 Dec 2010
Updated 13 Dec 2010
Type Journal
Year 2006
Where JUCS
Authors Manuel Clavel, Miguel Palomino, Adrián Riesco
Comments (0)