Bhayat, A., Korovin, K., Kovács, L., & Schoisswohl, J. (2023). Refining Unification with Abstraction. In R. Piskac & A. Voronkov (Eds.), Proceedings of 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (pp. 36–47). EasyChair EPiC. https://doi.org/10.29007/h65j
E192-04 - Forschungsbereich Formal Methods in Systems Engineering
-
Published in:
Proceedings of 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning
-
Volume:
94
-
Date (published):
3-Jun-2023
-
Event name:
LPAR 2023 : 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning
en
Event date:
4-Jun-2023 - 9-Jun-2023
-
Event place:
Manizales, Colombia
-
Number of Pages:
12
-
Publisher:
EasyChair EPiC
-
Keywords:
arithmetic; automated theorem proving; unification; Unification with Abstraction
en
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
Project title:
Automated Reasoning with Theories and Induction for Software Technologies: 101002685 (ERC Consolidator Grant 2020) Semantische und kryptografische Grundlagen von Informationssicherheit und Datenschutz durch modulares Design: F 8504 (FWF - Österr. Wissenschaftsfonds)
CC BY-NC-ND 4.0
