<div class="csl-bib-body">
<div class="csl-entry">Bhayat, A., Schoisswohl, J., & Rawson, M. (2023). Superposition with Delayed Unification. 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. 23–40). Springer. https://doi.org/10.1007/978-3-031-38499-8_2</div>
</div>
-
dc.identifier.uri
http://hdl.handle.net/20.500.12708/192946
-
dc.description.abstract
Classically, in saturation-based proof systems, unification has been considered atomic. However, it is also possible to move unification to the calculus level, turning the steps of the unification algorithm into inferences. For calculi that rely on unification procedures returning large or even infinite sets of unifiers, integrating unification into the calculus is an attractive method of dovetailing unification and inference. This applies, for example, to AC-superposition and higher-order superposition. We show that first-order superposition remains complete when moving unification rules to the calculus level. We discuss some of the benefits this has even for standard first-order superposition and provide an experimental evaluation.
en
dc.description.sponsorship
ERC Consolidator Grant 2020
-
dc.description.sponsorship
FWF - Österr. Wissenschaftsfonds
-
dc.language.iso
en
-
dc.relation.ispartofseries
Lecture Notes in Computer Science
-
dc.subject
higher-order logic
en
dc.subject
theorem proving
en
dc.subject
Superposition
en
dc.title
Superposition with Delayed Unification
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.affiliation
University of Manchester, United Kingdom of Great Britain and Northern Ireland (the)
-
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
23
-
dc.description.endpage
40
-
dc.relation.grantno
101002685
-
dc.relation.grantno
F 8504
-
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.project.title
Automated Reasoning with Theories and Induction for Software Technologies
-
tuw.project.title
Semantische und kryptografische Grundlagen von Informationssicherheit und Datenschutz durch modulares Design
-
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_2
-
dc.description.numberOfPages
18
-
tuw.author.orcid
0000-0002-1343-5084
-
tuw.author.orcid
0000-0001-5550-196X
-
tuw.author.orcid
0000-0001-7834-1567
-
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
Bhayat, Ahmed
-
wb.sciencebranch
Informatik
-
wb.sciencebranch.oefos
1020
-
wb.sciencebranch.value
100
-
item.cerifentitytype
Publications
-
item.languageiso639-1
en
-
item.fulltext
no Fulltext
-
item.openairetype
conference paper
-
item.openairecristype
http://purl.org/coar/resource_type/c_5794
-
item.grantfulltext
none
-
crisitem.project.funder
European Commission
-
crisitem.project.funder
FWF - Österr. Wissenschaftsfonds
-
crisitem.project.grantno
ERC Consolidator Grant 2020
-
crisitem.project.grantno
F 8500
-
crisitem.author.dept
University of Manchester
-
crisitem.author.dept
E192-04 - Forschungsbereich Formal Methods in Systems Engineering
-
crisitem.author.dept
E192-04 - Forschungsbereich Formal Methods in Systems Engineering
