Refining Unification with Abstraction

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.

Authors

• Ahmed Bhayat
• Konstantin Korovin
• Laura Kovács
• Johannes Schoisswohl

Keywords

No keywords are indexed for this paper.