Invited Talk: The Hows and Whys of Higher-Order
                                SMT
                                Sophie Tourret1
                                1
                                    Inria


                                                                         Abstract
                                                                         SMT solving for higher order logic has been around for a few years and many challenges remain to
                                                                         tackle. In this talk, I will present an assessment of the current state of research in higher-order SMT and
                                                                         focus on the challenge of quantifier instantiation, following a conflict-based approach inspired from
                                                                         first-order logic.




                                SMT 2024: 22st International Workshop on Satisfiability Modulo Theories July 22–23, 2024, Montreal Canada
                                $ stourret@loria.fr (S. Tourret)
                                                                       © 2024 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).
                                    CEUR
                                    Workshop
                                    Proceedings
                                                  http://ceur-ws.org
                                                  ISSN 1613-0073
                                                                       CEUR Workshop Proceedings (CEUR-WS.org)




CEUR
                  ceur-ws.org
Workshop      ISSN 1613-0073
Proceedings