×

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

MSC:

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

References:

[1] Barker-Plummer, D., Gazing: An Approach to the Problem of Definition and Lemma Use, J. Autom. Reasoning, 8, 3, 311-344 (1992) · Zbl 0825.68583 · doi:10.1007/BF02341853
[2] Benzmüller, C.; Schiller, M.; Siekmann, J.; Crocker, M.; Siekmann, J., Resource-bounded modelling and analysis of human-level interactive proofs, Resource Adaptive Cognitive Processes (2010), Heidelberg: Springer, Heidelberg
[3] Cramer, M., Fisseni, B., Koepke, P., Kühlwein, D., Schröder, B., Veldman, J.: The Naproche Project: Controlled Natural Language Proof Checking of Mathematical Texts. In: Fuchs, N.E. (ed.) CNL 2009 Workshop. LNCS, vol. 5972, pp. 170-186. Springer, Heidelberg (2010)
[4] Cramer, M.: Mathematisch-logische Aspekte von Beweisrepresentationsstrukturen. Master’s thesis, University of Bonn (2009)
[5] Koepke, P., Kühlwein, D., Cramer, M., Schröder, B.: The Naproche System (2009) · Zbl 1291.68336
[6] Ganesalingam, M.: The Language of Mathematics. PhD thesis, University of Cambridge (2009) · Zbl 1271.03004
[7] Heath, T.L., Euclid: The Thirteen Books of Euclid’s Elements, Books 1 and 2. Dover Publications, New York (1956) (Incorporated) · Zbl 0071.24203
[8] Hoder, K.: Automated Reasoning in Large Knowledge Bases. Master’s thesis, Charles University (2008)
[9] Hurd, J.: First-Order Proof Tactics in Higher-Order Logic Theorem Provers. In: Design and Application of Strategies/Tactics in Higher Order Logics, number NASA/CP-2003-212448 in NASA Technical Reports, pp. 56-68 (2003)
[10] Kuehlwein, D.: A Calculus for Proof Representation Structures. Master’s thesis, University of Bonn (2008)
[11] Landau, E.: Grundlagen der Analysis. Chelsea Publishing Company (1930) · JFM 56.0191.01
[12] Matuszewski, R., Rudnicki, P.: Mizar: the first 30 years. Mechanized Mathematics and Its Applications 4 (2005)
[13] Meng, J.; Paulson, L. C., Lightweight relevance filtering for machine-generated resolution problems, J. Applied Logic, 7, 1, 41-57 (2009) · Zbl 1183.68560 · doi:10.1016/j.jal.2007.07.004
[14] Nipkow, T.; Paulson, L. C.; Wenzel, M., Isabelle/HOL (2002), Heidelberg: Springer, Heidelberg · Zbl 1097.68632
[15] Schulz, S., E - A Brainiac Theorem Prover, Journal of AI Communications, 15, 2-3, 111-126 (2002) · Zbl 1020.68084
[16] Sutcliffe, G., The TPTP Problem Library and Associated Infrastructure: The FOF and CNF Parts, v3.5.0, Journal of Automated Reasoning, 43, 4, 337-362 (2009) · Zbl 1185.68636 · doi:10.1007/s10817-009-9143-8
[17] Sutcliffe, G.; Puzis, Y.; Pfenning, F., SRASS - A Semantic Relevance Axiom Selection System, Automated Deduction - CADE-21, 295-310 (2007), Heidelberg: Springer, Heidelberg · Zbl 1213.68575 · doi:10.1007/978-3-540-73595-3_20
[18] Urban, J.; Sutcliffe, G.; Pudlák, P.; Vyskocil, J.; Armando, A.; Baumgartner, P.; Dowek, G., MaLARea SG1- Machine Learner for Automated Reasoning with Semantic Guidance, Automated Reasoning, 441-456 (2008), Heidelberg: Springer, Heidelberg · Zbl 1165.68434 · doi:10.1007/978-3-540-71070-7_37
[19] Verchinine, K.; Lyaletski, A.; Paskevich, A.; Pfenning, F., System for Automated Deduction (SAD): A Tool for Proof Verification, Automated Deduction - CADE-21, 398-403 (2007), Heidelberg: Springer, Heidelberg · Zbl 1213.68576 · doi:10.1007/978-3-540-73595-3_29
[20] Vershinin, K.; Paskevich, A., ForTheL - the language of formal theories, International Journal of Information Theories and Applications, 7, 3, 120-126 (2000)
[21] Wenzel, M.: Isabelle/Isar - a generic framework for human-readable proof documents. Studies in Logic, Grammar and Rhetoric, vol. 10(23). University of Białystok (2007)
[22] Wos, L., The problem of definition expansion and contraction, J. Autom. Reason., 3, 4, 433-435 (1987) · doi:10.1007/BF00247438
[23] Zinn, C.: Understanding Informal Mathematical Discourse. PhD thesis, Friedrich-Alexander-Universitt Erlangen Nürnberg (2004) · Zbl 1101.68836
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.