Proof Simplification and Automated Theorem Proving

TL;DR

This paper introduces a technique for simplifying proofs generated by automated theorem provers, aiming to improve their simplicity and stimulate discussion on defining proof simplicity.

Contribution

The paper presents a novel proof simplification method and encourages exploration of measures for proof simplicity in automated theorem proving.

Findings

Proofs can be effectively simplified using the proposed technique.

Simplified proofs are closer to human-readable and understandable forms.

The work opens new questions on how to measure proof simplicity.

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.