# Extending E Prover with Similarity Based Clause Selection Strategies

arXiv: https://arxiv.org/abs/1606.03888 · HTML: https://mlsanity.com/paper/1606.03888/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 13 Jun 2016.

## Built on by (most cited first, 1 of 1)

- [Learning Theorem Proving Components](https://mlsanity.com/paper/2107.10034/) (2021)

## Abstract (arXiv)

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.