Mathematics – Logic
Scientific paper
2012-04-04
Mathematics
Logic
10 pages, 3 tables. Submitted to ATX 2012 (Automated Theory Exploration, http://dream.inf.ed.ac.uk/events/atx2012/)
Scientific paper
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.
No associations
LandOfFree
Tipi: A TPTP-based theory development environment emphasizing proof analysis does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with Tipi: A TPTP-based theory development environment emphasizing proof analysis, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Tipi: A TPTP-based theory development environment emphasizing proof analysis will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-31866