Refining Unification with Abstraction

Ahmed Bhayat; Konstantin Korovin; Laura Kovacs; Johannes Schoisswohl

doi:10.29007/h65j

Refining Unification with Abstraction

Ahmed Bhayat, Konstantin Korovin, Laura Kovacs, Johannes Schoisswohl

Formal Methods

Research output: Chapter in Book/Conference proceeding › Chapter › peer-review

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 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.

Original language	English
Title of host publication	Proceedings of 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning
Publisher	Easy Chair
Pages	36-23
ISBN (Electronic)	2398-7340
DOIs	https://doi.org/10.29007/h65j
Publication status	Published - 3 Jun 2023

Access to Document

10.29007/h65jLicence: CC BY-NC-ND

SCorCH: Secure Code for Capability Hardware
Reger, G. (PI), Cordeiro, L. (CoI), Korovin, K. (CoI), Mustafa, M. (CoI) & Olivier, P. (CoI)
1/07/20 → 31/12/23
Project: Research

Cite this

@inbook{75012da15f524b4c8e7af9317b775e04,

title = "Refining Unification with Abstraction",

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 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.",

author = "Ahmed Bhayat and Konstantin Korovin and Laura Kovacs and Johannes Schoisswohl",

year = "2023",

month = jun,

day = "3",

doi = "10.29007/h65j",

language = "English",

pages = "36--23",

booktitle = "Proceedings of 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning",

publisher = "Easy Chair",

address = "United States",

}

TY - CHAP

T1 - Refining Unification with Abstraction

AU - Bhayat, Ahmed

AU - Korovin, Konstantin

AU - Kovacs, Laura

AU - Schoisswohl, Johannes

PY - 2023/6/3

Y1 - 2023/6/3

N2 - 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.

AB - 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.

U2 - 10.29007/h65j

DO - 10.29007/h65j

M3 - Chapter

SP - 36

EP - 23

BT - Proceedings of 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning

PB - Easy Chair

ER -

Refining Unification with Abstraction

Abstract

Access to Document

Fingerprint

Projects

SCorCH: Secure Code for Capability Hardware

Cite this