Tags:Arithmetic, Automated theorem proving, Unification and 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.