Proof Simplification and Automated Theorem Proving

08/09/2018

∙

by   Michael Kinyon, et al.

∙

0

∙

share

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.