Quantifier Simplification by Unification in SMT

Pascal Fontaine (1, 2, 3) , Hans-Jörg Schurr (1, 2)

1 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
2 MOSEL - Proof-oriented development of computer-based systems
3 Université de Liège

Quantifier reasoning in SMT solvers relies on instantiation: ground instances are generated heuristically from the quantified formulas until a contradiction is reached at the ground level. Current instantiation heuristics, however, often fail in presence of nested quantifiers. To address this issue we introduce a unification-based method that augments the problem with shallow quantified formulas obtained from assertions with nested quantifiers. These new formulas help unlocking the regular instantiation techniques, but parsimony is necessary since they might also be misguiding. To mitigate this, we identify some effective restricting conditions. The method is implemented in the veriT solver, and tested on benchmarks from the SMT-LIB. It allows the solver to prove more formulas, faster.

Mots clés: SMT; quantifier instantiation; theorem proving

Domaines: Logique en informatique [cs.LO]

Pascal Fontaine, Hans-Jörg Schurr. Quantifier Simplification by Unification in SMT. FroCos 2021 - 13th International Symposium on Frontiers of Combining Systems, Sep 2021, Birmingham, United Kingdom. pp.232-249, ⟨10.1007/978-3-030-86205-3_13⟩. ⟨hal-03341368⟩