Theorem Proving in Large Formal Mathematics as an Emerging AI Field
Artificial Intelligence
2012-12-18 v2 Digital Libraries
Abstract
In the recent years, we have linked a large corpus of formal mathematics with automated theorem proving (ATP) tools, and started to develop combined AI/ATP systems working in this setting. In this paper we first relate this project to the earlier large-scale automated developments done by Quaife with McCune's Otter system, and to the discussions of the QED project about formalizing a significant part of mathematics. Then we summarize our adventure so far, argue that the QED dreams were right in anticipating the creation of a very interesting semantic AI field, and discuss its further research directions.
Keywords
Cite
@article{arxiv.1209.3914,
title = {Theorem Proving in Large Formal Mathematics as an Emerging AI Field},
author = {Josef Urban and Jiri Vyskocil},
journal= {arXiv preprint arXiv:1209.3914},
year = {2012}
}