2026/07/29 by Stephan Schulz
Computer Science · #cs.LO #cs.SC
arxiv created 2026/07/29 · arxiv updated 2026/07/31
In saturation-based theorem proving, selecting the next clause for processing is a major concern. Twee has successfully applied the idea of preferring clauses that share terms with the conjecture by adding equational definitions to transform the problem. In this paper, we apply the idea to the full first-order case, and offer an alternative implementation based on shared terms that shows very promising results.