One possible way to deal with large theories is to have a good selection method for relevant axioms. This is confirmed by the fact that the largest available first-order knowledge base (the Open CYC) contains over 3 million axioms, while answering queries to it usually requires not more than a few dozen axioms. A method for axiom selection has been proposed by the first author in the Sumo INference Engine (SInE) system. SInE has won the large theory division of CASC in 2008. The method turned out to be so successful that the next two years it was used by the winner as well as by several other competing systems. This paper contains the presentation of the method and describes experiments with it in the theorem prover Vampire. © 2011 Springer-Verlag Berlin Heidelberg.
|Title of host publication||Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|Lect. Notes Comput. Sci.|
|Number of pages||15|
|Publication status||Published - 2011|
|Event||23rd International Conference on Automated Deduction, CADE 23 - Wroclaw|
Duration: 1 Jul 2011 → …
|Conference||23rd International Conference on Automated Deduction, CADE 23|
|Period||1/07/11 → …|