Proof Simplification and Automated Theorem Proving
Logic in Computer Science
2021-01-19 v1 Logic
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.
Cite
@article{arxiv.1808.04251,
title = {Proof Simplification and Automated Theorem Proving},
author = {Michael Kinyon},
journal= {arXiv preprint arXiv:1808.04251},
year = {2021}
}