Automated Theorem Discovery

点击翻译按钮获取中文摘要

This project represents the second stage of a multi-stage project, the long-term goal of which is to emulate a large portion of the human mathematical discovery process. The focus of this particular stage is on fully developing and deploying an Automated Theorem Discovery (ATD) system. By ATD system we mean a system that automatically generates, proves and identifies a significant number of mathematical results which mathematicians are likely to recognize as Theorems, Lemmas, Corollaries, etc. (as opposed to the sorts of results which, true though they might be, would probably not be deemed worthy of recording).Generations of mathematicians have appreciated the benefits of building a mathematical knowledge base bit by bit, Theorem by Theorem, in that previously discovered results often prove quite useful -- perhaps even necessary -- in the discovery and the proof of subsequent results. Moreover, since the advent of the modern computer, it has become increasingly apparent that automated reasoning (AR) systems can likewise benefit from a similar incremental build-up of Theorems. This is especially true for certain formal verification problems, in which state-of-the-art automated theorem provers can dispatch some -- but not all -- of the generated proof obligations. The remaining proofs can only be achieved once certain Lemmas have been discovered; at present, this discovery must be done by hand.We therefore anticipate that an effective and practical ATD system would be very useful, not only to mathematicians, but to computer scientists as well -- particularly those who work in formal verification. Indeed, in the latter case, we have supporting evidence (in the form of letters of support) that the potential payoff for such a system is huge.