Sine qua von for large theory reasoning

Kryštof Hoder, Andrei Voronkov

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review


    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.
    Original languageEnglish
    Title of host publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|Lect. Notes Comput. Sci.
    PublisherSpringer Nature
    Number of pages15
    ISBN (Print)9783642224379
    Publication statusPublished - 2011
    Event23rd International Conference on Automated Deduction, CADE 23 - Wroclaw
    Duration: 1 Jul 2011 → …


    Conference23rd International Conference on Automated Deduction, CADE 23
    Period1/07/11 → …


    Dive into the research topics of 'Sine qua von for large theory reasoning'. Together they form a unique fingerprint.

    Cite this