This article is concerned with interactive support for "declarative theorem proving". After introducing declarative theorem proving, both in geneal and as implemented in the DECLARE system, we outline the requirements of an interactive system in this context. We describe IDECLARE, the interactive environment for DECLARE, and in particular its support for visualisation, logical navigation and debugging. We argue why declarative proof is particularly suited to interactive support, in contrast to general tactic proof, especially because it allows logical navigation without having to discharge proof obligations or execute user-defined tactics along the way. We informally evaluate IDECLARE with respect to a number of tasks and discuss several plausible extensions to the proposed mechanisms.

PostScript file

File

Details