Partial Redundancy in Saturation
Márton Hajdú, Laura Kovács, Андрей Воронков · Lecture notes in computer science · 2025
Abstract Redundancy elimination is one of the crucial ingredients of efficient saturation-based proof search. We strengthen redundancy elimination by introducing a new notion of redundancy, based on partial clauses and redundancy formulas . The new notion allows us to recognize redundant clauses and inferences that cannot be recognized by standard redundancy elimination criteria. In a way, our notion blurs the distinction between redundancy at the level of inferences and redundancy at the level of clauses. We present a superposition calculus PaRC on partial clauses and prove that it is refutationally complete. We discuss the implementation of the calculus in the theorem prover Vampire . Our experiments show the power of the new approach: we were able to solve 24 TPTP problems not previously solved by any prover, including previous versions of Vampire .