{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T13:01:13Z","timestamp":1760014873391},"reference-count":0,"publisher":"EasyChair","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>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 modulo T . We introduce a refined algorithm for unification with abstraction in T , 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.<\/jats:p>","DOI":"10.29007\/h65j","type":"proceedings-article","created":{"date-parts":[[2023,6,3]],"date-time":"2023-06-03T18:10:10Z","timestamp":1685815810000},"page":"36-23","source":"Crossref","is-referenced-by-count":3,"title":["Refining Unification with Abstraction"],"prefix":"10.29007","volume":"94","author":[{"given":"Ahmed","family":"Bhayat","sequence":"first","affiliation":[]},{"given":"Konstantin","family":"Korovin","sequence":"additional","affiliation":[]},{"given":"Laura","family":"Kovacs","sequence":"additional","affiliation":[]},{"given":"Johannes","family":"Schoisswohl","sequence":"additional","affiliation":[]}],"member":"11545","event":{"name":"Proceedings of 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning"},"container-title":["EPiC Series in Computing"],"original-title":[],"deposited":{"date-parts":[[2023,6,3]],"date-time":"2023-06-03T18:10:18Z","timestamp":1685815818000},"score":1,"resource":{"primary":{"URL":"https:\/\/easychair.org\/publications\/paper\/mHz7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"references-count":0,"URL":"https:\/\/doi.org\/10.29007\/h65j","relation":{},"ISSN":["2398-7340"],"issn-type":[{"type":"print","value":"2398-7340"}],"subject":[]}}