Lifting congruence closure with free variables to λ-free higher-order logic via SAT encoding

International audienceRecent work in extending SMT solvers to higher-order logic (HOL) has not explored lifting quantifier instantiation algorithms to perform higher-order unification. As a consequence, widely used instantiation techniques, such as trigger-and particularly conflictbased, can only be applied in a limited manner. Congruence closure with free variables (CCFV) is a decision procedure for the E-ground (dis-)unification problem, which is at the heart of these instantiation techniques. Here, as a first step towards fully supporting trigger-and conflict-based instantiation in HOL, we define the E-ground (dis-)unification problem in λ-free higher-order logic (λfHOL), an extension of first-order logic where function symbols may be partially applied and functional variables may occur, and extend CCFV to solve it. To improve scalability in the context of handling higher-order variables, we rely on an encoding of the CCFV search as a propositional formula. We present a solution reconstruction procedure so that models for the propositional formula lead to solutions for the E-ground (dis-)unification problem. This is instrumental to port triggerand conflict-based instantiation to be fully applied in λfHOL. * The order of authors is inverse alphabetic