Different Proofs are Good Proofs
Abstract
In order to compare the quality of proofs, it is necessary to measure
artifacts of the proofs, and evaluate the measurements to
determine differences between the proofs.
This paper discounts the approach of ranking proofs by their measured
proof artifacts, and takes the position that different proofs are good
proofs.
The position is based on proofs in the TSTP solution library, which are
generated by Automated Theorem Proving (ATP) systems applied to first-order
logic problems in the TPTP problem library.