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. © Springer-Verlag Berlin Heidelberg 2013.
Cite
CITATION STYLE
Urban, J., & Vyskočil, J. (2013). Theorem proving in large formal mathematics as an emerging AI Field. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 7788, 240–257. https://doi.org/10.1007/978-3-642-36675-8_13
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
