Tipi: A TPTP-based theory development environment emphasizing proof analysis
From MaRDI portal
Publication:6232086
arXiv1204.0901MaRDI QIDQ6232086FDOQ6232086
Publication date: 4 April 2012
Abstract: 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.
This page was built for publication: Tipi: A TPTP-based theory development environment emphasizing proof analysis
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6232086)
