SAT-Based Subsumption Resolution
Robin Coutelier, Laura Kovács, Michael Rawson, Jakob Rath · Lecture notes in computer science · 2023
Abstract Subsumption resolution is an expensive but highly effective simplifying inference for first-order saturation theorem provers. We present a new SAT-based reasoning technique for subsumption resolution, without requiring radical changes to the underlying saturation algorithm. We implemented our work in the theorem proverVampire, and show that it is noticeably faster than the state of the art.