SAT-Based Subsumption Resolution
Logic in Computer Science
2024-02-01 v1
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 prover Vampire, and show that it is noticeably faster than the state of the art.
Keywords
Cite
@article{arxiv.2401.17832,
title = {SAT-Based Subsumption Resolution},
author = {Robin Coutelier and Laura Kovács and Michael Rawson and Jakob Rath},
journal= {arXiv preprint arXiv:2401.17832},
year = {2024}
}