Friday 10 September 2021, 11:00 AM, room 3U47: On what is wrong with higher-order SMT and what we are doing to fix it, Sophie Tourret (INRIA, LORIA).

SMT solvers have been extended to deal with higher-order problems just a few years ago [1]. However, their performances are limited in this new domain, because only the ground SMT module has been extended.

This talk presents ongoing work about extending one of the most effective SMT instantiation technique, namely CCFV [2], to lambda-free HOL, as a first step to full HOL SMT instantiation. Surprisingly, moving to lambda-free HOL allows us to encode the problem as a propositional formula, such that its models correspond to instances we need. I will explain how this is done.

[1] Haniel Barbosa, Andrew Reynolds, Daniel El Ouraoui, Cesare Tinelli, Clark W. Barrett: Extending SMT Solvers to Higher-Order Logic. CADE 2019: 35-54

[2] Haniel Barbosa, Pascal Fontaine, Andrew Reynolds: Congruence Closure with Free Variables. TACAS (2) 2017: 214-230