Datensatz Zitierlink: 
http://hdl.handle.net/20.500.12708/192839
-
Titel: 
SAT-Based Subsumption Resolution
en
Zitat: 
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
-
Verlags-DOI: 
10.1007/978-3-031-38499-8_11
-
Publikationstyp: 
Konferenzbeitrag - Full-Paper Contribution
de
Sprache: 
Englisch
-
Autor_innen: 
Coutelier, Robin 
Kovács, Laura 
Rawson, Michael 
Rath, Jakob 
-
Organisations­einheit: 
E192-04 - Forschungsbereich Formal Methods in Systems Engineering 
-
Erschienen in: 
Automated Deduction – CADE 29 29th International Conference on Automated Deduction, Rome, Italy, July 1–4, 2023, Proceedings 
-
ISBN: 
978-3-031-38498-1
-
Band: 
14132
-
DOI des Buches: 
10.1007/978-3-031-38499-8
-
Datum (veröffentlicht): 
2-Sep-2023
-
Veranstaltungs­name: 
29th International Conference on Automated Deduction 
en
Veranstaltungs­zeitraum: 
1-Jul-2023 - 4-Jul-2023
-
Veranstaltungs­ort: 
Roma, Italien
-
Umfang: 
17
-
Verlag: 
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
Forschungs­schwerpunkte: 
Logic and Computation: 100%
-
Wissenschafts­zweig: 
1020 - Informatik: 100%
-
Enthalten in den Sammlungen:
Conference Paper

Zur Langanzeige

Seiten Aufrufe

171
aufgerufen am 26.01.2024

Google ScholarTM

Check