Proof Simplification and Automated Theorem Proving
arXiv:1808.04251 · doi:10.1098/rsta.2018.0034
Abstract
The proofs first generated by automated theorem provers are far from optimal by any measure of simplicity. In this paper I describe a technique for simplifying automated proofs. Hopefully this discussion will stimulate interest in the larger, still open, question of what reasonable measures of proof simplicity might be.