<div class="csl-bib-body">
<div class="csl-entry">Coutelier, R., Kovács, L., Rawson, M., & Rath, J. (2023). SAT-Based Subsumption Resolution. In B. Pientka & C. Tinelli (Eds.), <i>Automated Deduction – CADE 29 29th International Conference on Automated Deduction, Rome, Italy, July 1–4, 2023, Proceedings</i> (pp. 190–206). Springer. https://doi.org/10.1007/978-3-031-38499-8_11</div>
</div>
-
dc.identifier.uri
http://hdl.handle.net/20.500.12708/192839
-
dc.description.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
dc.language.iso
en
-
dc.relation.ispartofseries
Lecture Notes in Computer Science
-
dc.subject
automated reasoning
en
dc.subject
first-order theorem proving
en
dc.subject
subsumption
en
dc.subject
resolution
en
dc.subject
SAT solving
en
dc.title
SAT-Based Subsumption Resolution
en
dc.type
Inproceedings
en
dc.type
Konferenzbeitrag
de
dc.relation.publication
Automated Deduction – CADE 29 29th International Conference on Automated Deduction, Rome, Italy, July 1–4, 2023, Proceedings
-
dc.contributor.editoraffiliation
McGill University, Canada
-
dc.contributor.editoraffiliation
University of Iowa, United States of America (the)
-
dc.relation.isbn
978-3-031-38498-1
-
dc.relation.doi
10.1007/978-3-031-38499-8
-
dc.relation.issn
0302-9743
-
dc.description.startpage
190
-
dc.description.endpage
206
-
dc.type.category
Full-Paper Contribution
-
dc.relation.eissn
1611-3349
-
tuw.booktitle
Automated Deduction – CADE 29 29th International Conference on Automated Deduction, Rome, Italy, July 1–4, 2023, Proceedings
-
tuw.container.volume
14132
-
tuw.book.ispartofseries
Lecture Notes in Computer Science
-
tuw.relation.publisher
Springer
-
tuw.relation.publisherplace
Cham
-
tuw.researchTopic.id
I1
-
tuw.researchTopic.name
Logic and Computation
-
tuw.researchTopic.value
100
-
tuw.publication.orgunit
E192-04 - Forschungsbereich Formal Methods in Systems Engineering
-
tuw.publisher.doi
10.1007/978-3-031-38499-8_11
-
dc.description.numberOfPages
17
-
tuw.author.orcid
0000-0002-8299-2714
-
tuw.author.orcid
0000-0001-7834-1567
-
tuw.author.orcid
0000-0003-0346-6749
-
tuw.editor.orcid
0000-0002-2549-4276
-
tuw.event.name
29th International Conference on Automated Deduction
en
tuw.event.startdate
01-07-2023
-
tuw.event.enddate
04-07-2023
-
tuw.event.online
On Site
-
tuw.event.type
Event for scientific audience
-
tuw.event.place
Roma
-
tuw.event.country
IT
-
tuw.event.institution
Sapienza University of Rome
-
tuw.event.presenter
Coutelier, Robin
-
wb.sciencebranch
Informatik
-
wb.sciencebranch.oefos
1020
-
wb.sciencebranch.value
100
-
item.openairecristype
http://purl.org/coar/resource_type/c_5794
-
item.languageiso639-1
en
-
item.fulltext
no Fulltext
-
item.grantfulltext
none
-
item.openairetype
conference paper
-
item.cerifentitytype
Publications
-
crisitem.author.dept
E192-04 - Forschungsbereich Formal Methods in Systems Engineering
-
crisitem.author.dept
E192-04 - Forschungsbereich Formal Methods in Systems Engineering
-
crisitem.author.dept
E192-04 - Forschungsbereich Formal Methods in Systems Engineering
-
crisitem.author.dept
E192-04 - Forschungsbereich Formal Methods in Systems Engineering
