Automated Proof Compression by Invention of New Definitions
Automated Proof Compression by Invention of New Definitions
复制标题
通过新定义的发明实现自动证明压缩
DOI：
--
复制
发表时间：
2010
期刊：
影响因子：
--
通讯作者：
J. Urban
中科院分区：
文献类型：
--
作者：
J. Vyskočil;D. Stanovský;J. Urban
当今最先进的自动定理证明器（atp）能够解决相对复杂的数学问题。但是，随着ATP越来越强大，越来越多地被数学家使用，自动发现的证明的长度和人类的不可读性成为ATP用户面临的一个严重问题。一种补救办法是通过发明新的定义来自动压缩证明。
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.