Output details
11 - Computer Science and Informatics
University of Manchester
Return to search
Output 0 of 0 in the submission
Output title
Sine Qua Non for Large Theory Reasoning
Type
E - Conference contribution
Name of conference/published proceedings
Automated Deduction - CADE-23 - 23rd International Conference on Automated Deduction
Volume number
6803
Issue number
-
First page of article
299
ISSN of proceedings
1611-3349
Year of publication
2011
URL
-
Number of additional authors
1
Additional information
<11> Handling very large theories consisting of hundreds of thousands or millions of axioms is an important emerging area in automated reasoning because such theories appear in formalisations of mathematics and very large ontologies. This paper is significant because it proposed a new family of algorithms (Sine selection) for selecting a subset of axioms relevant to a given query. It made a breakthrough in the area since these algorithms turned out to outperform all previous algorithms by a very large margin. When dealing with large theories, all top theorem provers are now using Sine selection.
Interdisciplinary
-
Cross-referral requested
-
Research group
None
Citation count
5
Proposed double-weighted
No
Double-weighted statement
-
Reserve for a double-weighted output
No
Non-English
No
English abstract
-
