Automated Proof Compression by Invention of New Definitions

State-of-the-art automated theorem provers (ATPs) are today able to solve relatively complicated mathematical problems. But as ATPs become stronger and more used by mathematicians, the length and human unreadability of the automatically found proofs become a serious problem for the ATP users. One remedy is automated proof compression by invention of new definitions. We propose a new algorithm for automated compression of arbitrary sets of terms (like mathematical proofs) by invention of new definitions, using a heuristics based on substitution trees. The algorithm has been implemented and tested on a number of automatically found proofs. The results of the tests are included.

• Type: Journal
• Year: 2010
• Where: LPAR
• Authors: Jirí Vyskocil, David Stanovský, Josef Urban
• Keywords: Automated, Automated Reasoning, LPAR 2010, Mathematical Proofs, Proof Compression