Abstract
E prover is a state-of-the-art theorem prover for first-order logic with equality. E prover is built around a saturation loop, where new clauses are derived by inference rules from previously derived clauses. Selection of clauses for the inference provides the main source of non-determinism and an important choice-point of the loop where the right choice can dramatically influence the proof search. In this work we extend E Prover with several new clause selection strategies based on similarity of a clause with the conjecture. In particular, clauses which are more related to the conjecture are preferred. We implement different strategies that define the relationship with a conjecture in different ways. We provide an implementation of the proposed selection strategies and we evaluate their efficiency on an extensive benchmark set.
J. Jakubův and J. Urban—Supported by the ERC Consolidator grant nr. 649043 AI4REASON.
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
Similar content being viewed by others
References
Alama, J., et al.: Premise selection for mathematics by corpus analysis and kernel methods. J. Autom. Reason. 52(2), 191–213 (2014)
Kaliszyk, C., Urban, J., Vyskocil, J.: Efficient semantic features for automated reasoning over large theories. In: IJCAI, vol. 15 (2015)
Leskovec, J., Rajaraman, A., Ullman, J.D.: Mining of Massive Datasets, 2nd edn. Cambridge University Press, Cambridge (2014)
Levenshtein, V.I.: Binary codes capable of correcting deletions, insertions and reversals. Sov. Phys. Dokl. 10, 707 (1966)
McCune, W.W.: Otter 3.0 Reference Manual and Guide, vol. 9700. Argonne National Laboratory, Argonne (1994)
Schulz, S.: E - a brainiac theorem prover. AI Commun. 15(2), 111–126 (2002)
Urban, J.: BliStr: the blind strategymaker. In: Global Conference on Artificial Intelligence, GCAI 2015, vol. 36, pp. 312–319. EasyChair (2015)
Zhang, K., Shasha, D.: Simple fast algorithms for the editing distance between trees and related problems. SIAM J. Comput. 18(6), 1245–1262 (1989)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing Switzerland
About this paper
Cite this paper
Jakubův, J., Urban, J. (2016). Extending E Prover with Similarity Based Clause Selection Strategies. In: Kohlhase, M., Johansson, M., Miller, B., de Moura, L., Tompa, F. (eds) Intelligent Computer Mathematics. CICM 2016. Lecture Notes in Computer Science(), vol 9791. Springer, Cham. https://doi.org/10.1007/978-3-319-42547-4_11
Download citation
DOI: https://doi.org/10.1007/978-3-319-42547-4_11
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-42546-7
Online ISBN: 978-3-319-42547-4
eBook Packages: Computer ScienceComputer Science (R0)