Record link: 
http://hdl.handle.net/20.500.12708/192839
-
Title: 
SAT-Based Subsumption Resolution
en
Citation: 
Coutelier, R., Kovács, L., Rawson, M., & Rath, J. (2023). SAT-Based Subsumption Resolution. In B. Pientka & C. Tinelli (Eds.), Automated Deduction – CADE 29  29th International Conference on Automated Deduction, Rome, Italy, July 1–4, 2023, Proceedings (pp. 190–206). Springer. https://doi.org/10.1007/978-3-031-38499-8_11
-
Publisher DOI: 
10.1007/978-3-031-38499-8_11
-
Publication Type: 
Inproceedings - Full-Paper Contribution
en
Language: 
English
-
Authors: 
Coutelier, Robin 
Kovács, Laura 
Rawson, Michael 
Rath, Jakob 
-
Organisational Unit: 
E192-04 - Forschungsbereich Formal Methods in Systems Engineering 
-
Published in: 
Automated Deduction – CADE 29 29th International Conference on Automated Deduction, Rome, Italy, July 1–4, 2023, Proceedings 
-
ISBN: 
978-3-031-38498-1
-
Volume: 
14132
-
DOI of the book: 
10.1007/978-3-031-38499-8
-
Date (published): 
2-Sep-2023
-
Event name: 
29th International Conference on Automated Deduction 
en
Event date: 
1-Jul-2023 - 4-Jul-2023
-
Event place: 
Roma, Italy
-
Number of Pages: 
17
-
Publisher: 
Springer, Cham
-
Keywords: 
automated reasoning; first-order theorem proving; subsumption; resolution; SAT solving
en
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.
en
Research Areas: 
Logic and Computation: 100%
-
Science Branch: 
1020 - Informatik: 100%
-
Appears in Collections:
Conference Paper

Show full item record

Page view(s)

268
checked on Jan 26, 2024

Google ScholarTM

Check