<div class="csl-bib-body">
<div class="csl-entry">Bhayat, A., Korovin, K., Kovács, L., & Schoisswohl, J. (2023). Refining Unification with Abstraction. In R. Piskac & A. Voronkov (Eds.), <i>Proceedings of 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning</i> (pp. 36–47). EasyChair EPiC. https://doi.org/10.29007/h65j</div>
</div>
-
dc.identifier.uri
http://hdl.handle.net/20.500.12708/193926
-
dc.description.abstract
Automated reasoning with theories and quantifiers is a common demand in formal methods. A major challenge that arises in this respect comes with rewriting/simplifying terms that are equal with respect to a background first-order theory T, as equality reasoning in this context requires unification moduloT. We introduce a refined algorithm for unification with abstraction inT, allowing for a fine-grained control of equality constraints and substitutions introduced by standard unification with abstraction approaches. We experimentally show the benefit of our approach within first-order linear rational arithmetic.
en
dc.description.sponsorship
ERC Consolidator Grant 2020
-
dc.description.sponsorship
FWF - Österr. Wissenschaftsfonds
-
dc.language.iso
en
-
dc.relation.ispartofseries
EPiC Series in Computing
-
dc.rights.uri
http://creativecommons.org/licenses/by-nc-nd/4.0/
-
dc.subject
arithmetic
en
dc.subject
automated theorem proving
en
dc.subject
unification
en
dc.subject
Unification with Abstraction
en
dc.title
Refining Unification with Abstraction
en
dc.type
Inproceedings
en
dc.type
Konferenzbeitrag
de
dc.rights.license
Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International
en
dc.rights.license
Creative Commons Namensnennung - Nicht kommerziell - Keine Bearbeitungen 4.0 International
de
dc.relation.publication
Proceedings of 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning
-
dc.contributor.affiliation
University of Manchester, United Kingdom of Great Britain and Northern Ireland (the)
-
dc.contributor.affiliation
University of Manchester, United Kingdom of Great Britain and Northern Ireland (the)
-
dc.contributor.editoraffiliation
Yale University, United States of America (the)
-
dc.contributor.editoraffiliation
University of Manchester, United Kingdom of Great Britain and Northern Ireland (the)
-
dc.relation.issn
2398-7340
-
dc.description.startpage
36
-
dc.description.endpage
47
-
dc.relation.grantno
101002685
-
dc.relation.grantno
F 8504
-
dc.rights.holder
Authors
-
dc.type.category
Full-Paper Contribution
-
tuw.booktitle
Proceedings of 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning
-
tuw.container.volume
94
-
tuw.book.ispartofseries
EPiC Series in Computing
-
tuw.relation.publisher
EasyChair EPiC
-
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.29007/h65j
-
dc.identifier.libraryid
AC17202271
-
dc.description.numberOfPages
12
-
tuw.author.orcid
0000-0002-1343-5084
-
tuw.author.orcid
0000-0002-8299-2714
-
dc.rights.identifier
CC BY-NC-ND 4.0
en
dc.rights.identifier
CC BY-NC-ND 4.0
de
tuw.editor.orcid
0000-0002-3267-0776
-
tuw.editor.orcid
0000-0003-1073-7615
-
tuw.event.name
LPAR 2023 : 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning
en
dc.description.sponsorshipexternal
EPSRC
-
dc.relation.grantnoexternal
EP/V000497/1
-
tuw.event.startdate
04-06-2023
-
tuw.event.enddate
09-06-2023
-
tuw.event.online
On Site
-
tuw.event.type
Event for scientific audience
-
tuw.event.place
Manizales
-
tuw.event.country
CO
-
tuw.event.presenter
Schoisswohl, Johannes
-
wb.sciencebranch
Informatik
-
wb.sciencebranch.oefos
1020
-
wb.sciencebranch.value
100
-
item.openairecristype
http://purl.org/coar/resource_type/c_5794
-
item.openaccessfulltext
Open Access
-
item.openairetype
conference paper
-
item.fulltext
with Fulltext
-
item.mimetype
application/pdf
-
item.languageiso639-1
en
-
item.grantfulltext
open
-
item.cerifentitytype
Publications
-
crisitem.author.dept
University of Manchester
-
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
