Abstract
In this paper, we report results of an experiment to use the mutual information criterion to automatically select formulas to guide the search for proofs using McCune’s Prover9 system. The formulas were selected from the TPTP library of problems for theorem-provers.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Church, K.W., Hanks, P.: Word Association Norms, Mutual Information, and Lexicography. Computational Linguistics 16(1)
Draeger, J.: Acquisition of Useful Lemma-Knowledge in Automated Reasoning. In: Giunchiglia, F. (ed.) AIMSA 1998. LNCS (LNAI), vol. 1480, pp. 230–239. Springer, Heidelberg (1998)
Draeger, J., Schulz, S., et al.: Improving the performance of automated theorem provers by redundancy-free lemmatization. In: Proceedings of the 14th Florida Artificial Intelligence Research Symposium, pp. 345–349 (2001)
McCune, W.: OTTER: 3.0 Reference Manual and Guide, Technical Report ANL-94/6. Argonne National Laboratory, Argonne, Illinois (1994)
McCune, W.: Prover9 Manual (2006), http://www.cs.unm.edu/mccune/prover9/manual
Schulz, S.: Information-based selection of abstraction levels. In: Proc. of the 14th FLAIRS, Key West, pp. 402–406 (2001)
Shannon, C., Weaver, E.: The Mathematical Theory of Communication. University of Chicago Press, Chicago (1949)
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)
Veroff, R.: Using hints to increase the effectiveness of an automated reasoning program: Case studies. J. Automated Reason. 16(3), 223–239 (1996)
Wren, J.: Extending the Mutual Information Measure to Rank Inferred Literature Relationships. BMC Bioinformatics 5 (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Ernst, Z., Kurtenbach, S. (2013). Toward a Procedure for Data Mining Proofs. In: Bonacina, M.P., Stickel, M.E. (eds) Automated Reasoning and Mathematics. Lecture Notes in Computer Science(), vol 7788. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-36675-8_12
Download citation
DOI: https://doi.org/10.1007/978-3-642-36675-8_12
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-36674-1
Online ISBN: 978-3-642-36675-8
eBook Packages: Computer ScienceComputer Science (R0)