SAT-Based Subsumption Resolution
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , , , |
|---|---|
| Format: | Preprint |
| Publié: |
2024
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866911768398266368 |
|---|---|
| author | Coutelier, Robin Kovács, Laura Rawson, Michael Rath, Jakob |
| author_facet | Coutelier, Robin Kovács, Laura Rawson, Michael Rath, Jakob |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2401_17832 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | SAT-Based Subsumption Resolution Coutelier, Robin Kovács, Laura Rawson, Michael Rath, Jakob Logic in Computer Science 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. |
| title | SAT-Based Subsumption Resolution |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2401.17832 |