Theorem Proving in Large Formal Mathematics as an Emerging AI Field
The result's identifiers
Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F68407700%3A21230%2F13%3A00214589" target="_blank" >RIV/68407700:21230/13:00214589 - isvavai.cz</a>
Result on the web
<a href="http://link.springer.com/chapter/10.1007%2F978-3-642-36675-8_13" target="_blank" >http://link.springer.com/chapter/10.1007%2F978-3-642-36675-8_13</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1007/978-3-642-36675-8_13" target="_blank" >10.1007/978-3-642-36675-8_13</a>
Alternative languages
Result language
angličtina
Original language name
Theorem Proving in Large Formal Mathematics as an Emerging AI Field
Original language description
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´sOtter 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 direction.
Czech name
—
Czech description
—
Classification
Type
J<sub>x</sub> - Unclassified - Peer-reviewed scientific article (Jimp, Jsc and Jost)
CEP classification
JC - Computer hardware and software
OECD FORD branch
—
Result continuities
Project
<a href="/en/project/GAP103%2F12%2F1994" target="_blank" >GAP103/12/1994: Adaptive scheduling and Optimization algorithms for distributed Real-time Embeddes Systems</a><br>
Continuities
Z - Vyzkumny zamer (s odkazem do CEZ)
Others
Publication year
2013
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Name of the periodical
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
ISSN
0302-9743
e-ISSN
—
Volume of the periodical
7788
Issue of the periodical within the volume
—
Country of publishing house
DE - GERMANY
Number of pages
18
Pages from-to
240-257
UT code for WoS article
—
EID of the result in the Scopus database
—