Efficient Semantic Features for Automated Reasoning over Large Theories
The result's identifiers
Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F68407700%3A21730%2F15%3A00235217" target="_blank" >RIV/68407700:21730/15:00235217 - isvavai.cz</a>
Result on the web
<a href="http://ijcai.org/papers15/Papers/IJCAI15-435.pdf" target="_blank" >http://ijcai.org/papers15/Papers/IJCAI15-435.pdf</a>
DOI - Digital Object Identifier
—
Alternative languages
Result language
angličtina
Original language name
Efficient Semantic Features for Automated Reasoning over Large Theories
Original language description
Large formal mathematical knowledge bases encode considerable parts of advanced mathematics and exact science, allowing deep semantic computer assistance and verification of complicated theories down to the atomic logical rules. An essential part of automated reasoning over such large theories are methods learning selection of relevant knowledge from the thousands of proofs in the corpora. Such methods in turn rely on efficiently computable features characterizing the highly structured and inter-relatedmathematical statements. In this work we (i) propose novel semantic features characterizing the statements in such large semantic knowledge bases, (ii) propose and carry out their efficient implementation using deductive-AI data-structures such as substitution trees and discrimination nets, and (iii) show that they significantly improve the strength of existing knowledge selection methods and automated reasoning methods over the large formal knowledge bases. In particular, on a standard
Czech name
—
Czech description
—
Classification
Type
D - Article in proceedings
CEP classification
JD - Use of computers, robotics and its application
OECD FORD branch
—
Result continuities
Project
—
Continuities
I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace
Others
Publication year
2015
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
Article name in the collection
Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence
ISBN
978-1-57735-738-4
ISSN
1045-0823
e-ISSN
—
Number of pages
7
Pages from-to
3084-3090
Publisher name
AAAI Press
Place of publication
Menlo Park, California
Event location
Buenos Aires
Event date
Jul 25, 2015
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
—