Sine qua von for large theory reasoning

Kryštof Hoder; Andrei Voronkov

doi:10.1007/978-3-642-22438-6_23

Sine qua von for large theory reasoning

Kryštof Hoder, Andrei Voronkov

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

Abstract

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 language	English
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.
Publisher	Springer Nature
Pages	299-314
Number of pages	15
Volume	6803
ISBN (Print)	9783642224379
DOIs	https://doi.org/10.1007/978-3-642-22438-6_23
Publication status	Published - 2011
Event	23rd International Conference on Automated Deduction, CADE 23 - Wroclaw Duration: 1 Jul 2011 → …

Conference

Conference	23rd International Conference on Automated Deduction, CADE 23
City	Wroclaw
Period	1/07/11 → …

Access to Document

10.1007/978-3-642-22438-6_23

Cite this

@inproceedings{ce58364c5a1e4597bc1970afc71e8e03,

title = "Sine qua von for large theory reasoning",

abstract = "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. {\textcopyright} 2011 Springer-Verlag Berlin Heidelberg.",

author = "Kry{\v s}tof Hoder and Andrei Voronkov",

year = "2011",

doi = "10.1007/978-3-642-22438-6_23",

language = "English",

isbn = "9783642224379",

volume = "6803",

pages = "299--314",

booktitle = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|Lect. Notes Comput. Sci.",

publisher = "Springer Nature",

address = "United States",

note = "23rd International Conference on Automated Deduction, CADE 23 ; Conference date: 01-07-2011",

}

Hoder, K & Voronkov, A 2011, Sine qua von for large theory reasoning. in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|Lect. Notes Comput. Sci.. vol. 6803, Springer Nature, pp. 299-314, 23rd International Conference on Automated Deduction, CADE 23, Wroclaw, 1/07/11. https://doi.org/10.1007/978-3-642-22438-6_23

Sine qua von for large theory reasoning. / Hoder, Kryštof; Voronkov, Andrei.

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|Lect. Notes Comput. Sci.. Vol. 6803 Springer Nature, 2011. p. 299-314.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Sine qua von for large theory reasoning

AU - Hoder, Kryštof

AU - Voronkov, Andrei

PY - 2011

Y1 - 2011

N2 - 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.

AB - 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.

U2 - 10.1007/978-3-642-22438-6_23

DO - 10.1007/978-3-642-22438-6_23

M3 - Conference contribution

SN - 9783642224379

VL - 6803

SP - 299

EP - 314

BT - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|Lect. Notes Comput. Sci.

PB - Springer Nature

T2 - 23rd International Conference on Automated Deduction, CADE 23

Y2 - 1 July 2011

ER -

Sine qua von for large theory reasoning

Abstract

Conference

Access to Document

Fingerprint

Cite this