zbMATH — the first resource for mathematics

Premise selection in the Naproche system. (English) Zbl 1291.68336
Giesl, Jürgen (ed.) et al., Automated reasoning. 5th international joint conference, IJCAR 2010, Edinburgh, UK, July 16–19, 2010. Proceedings. Berlin: Springer (ISBN 978-3-642-14202-4/pbk). Lecture Notes in Computer Science 6173. Lecture Notes in Artificial Intelligence, 434-440 (2010).
Summary: Automated theorem provers (ATPs) struggle to solve problems with large sets of possibly superfluous axiom. Several algorithms have been developed to reduce the number of axioms, optimally only selecting the necessary axioms. However, most of these algorithms consider only single problems. In this paper, we describe an axiom selection method for series of related problems that is based on logical and textual proximity and tries to mimic a human way of understanding mathematical texts. We present first results that indicate that this approach is indeed useful.
For the entire collection see [Zbl 1195.68005].

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
Full Text: DOI