  In some theory development tasks, a problem is satisfactorily solved once it
is shown that a theorem (conjecture) is derivable from the background theory
(premises). Depending on one's motivations, the details of the derivation of
the conjecture from the premises may or may not be important. In some contexts,
though, one wants more from theory development than simply derivability of the
target theorems from the background theory. One may want to know which premises
of the background theory were used in the course of a proof output by an
automated theorem prover (when a proof is available), whether they are all, in
suitable senses, necessary (and why), whether alternative proofs can be found,
and so forth. The problem, then, is to support proof analysis in theory
development; the tool described in this paper, Tipi, aims to provide precisely
that.
