Extending E Prover with Similarity Based Clause Selection Strategies

TL;DR

This paper enhances the E prover by integrating new clause selection strategies based on clause-conjecture similarity, aiming to improve proof search efficiency in first-order logic with equality.

Contribution

The paper introduces and implements novel similarity-based clause selection strategies for E prover, expanding its capabilities and potentially increasing proof search effectiveness.

Findings

Similarity-based strategies improve proof search efficiency.

Preferred clauses are more related to the conjecture.

Evaluation shows effectiveness on extensive benchmarks.

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.