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 ifrst-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). CPWrEooUrckResehdoinpgs IhStpN:/c1e6u1r3-w-0s.o7r3g CEUR Workshop Proceedings (CEUR-WS.org)