Automated theorem provers: a practical tool for the working mathematician?

作者：Bundy Alan^*

来源：Annals of Mathematics and Artificial Intelligence, 2011, 61(1): 3-14.

DOI：10.1007/s10472-011-9248-8

• Automated theorem proving
• Mathematician's assistant
• Very large proofs
• Proof understanding

In contrast to the widespread use of computer algebra systems in mathematics automated theorem provers have largely met with indifference. There are signs that this is at last beginning to change. We argue that it is inevitable that automated provers will be adopted as a practical tool for the working mathematician. Mathematical applications of automated provers raises profound challenges for their developers.

• 出版日期2011-1