@article{Barbosa1712.01486,
TITLE = {Language and Proofs for Higher-Order {SMT} (Work in Progress)},
AUTHOR = {Barbosa, Haniel and Blanchette, Jasmin Christian and Cruanes, Simon and El Ouraoui, Daniel and Fontaine, Pascal},
LANGUAGE = {eng},
URL = {http://arxiv.org/abs/1712.01486},
DOI = {10.4204/EPTCS.262.3},
EPRINT = {1712.01486},
EPRINTTYPE = {arXiv},
YEAR = {2017},
ABSTRACT = {Satisfiability modulo theories (SMT) solvers have throughout the years been<br>able to cope with increasingly expressive formulas, from ground logics to full<br>first-order logic modulo theories. Nevertheless, higher-order logic within SMT<br>is still little explored. One main goal of the Matryoshka project, which<br>started in March 2017, is to extend the reasoning capabilities of SMT solvers<br>and other automatic provers beyond first-order logic. In this preliminary<br>report, we report on an extension of the SMT-LIB language, the standard input<br>format of SMT solvers, to handle higher-order constructs. We also discuss how<br>to augment the proof format of the SMT solver veriT to accommodate these new<br>constructs and the solving techniques they require.<br>},
JOURNAL = {Electronic Proceedings in Theoretical Computer Science},
VOLUME = {262},
PAGES = {15--22},
}