Language and Proofs for Higher-Order SMT (Work in Progress)

Haniel Barbosa; Jasmin Christian Blanchette; Simon Cruanes; Daniel El Ouraoui; Pascal Fontaine

doi:10.4204/EPTCS.262.3

Language and Proofs for Higher-Order SMT (Work in Progress)

Haniel Barbosa, Jasmin Christian Blanchette, Simon Cruanes, Daniel El Ouraoui, Pascal Fontaine

Research output: Contribution to Journal › Article › Academic › peer-review

Abstract

Satisfiability modulo theories (SMT) solvers have throughout the years been able to cope with increasingly expressive formulas, from ground logics to full first-order logic modulo theories. Nevertheless, higher-order logic within SMT is still little explored. One main goal of the Matryoshka project, which started inMarch 2017, is to extend the reasoning capabilities of SMT solvers and other automatic provers beyond first-order logic. In this preliminary report, we report on an extension of the SMT-LIB language, the standard input format of SMT solvers, to handle higher-order constructs. We also discuss how to augment the proof format of the SMT solver veriT to accommodate these new constructs and the solving techniques they require.

Original language	English
Pages (from-to)	15-22
Number of pages	8
Journal	Electronic Proceedings in Theoretical Computer Science
Volume	262
Issue number	262
DOIs	https://doi.org/10.4204/EPTCS.262.3
Publication status	Published - 2017

Funding

†This work has been partially supported by the ANR/DFG project STU 483/2-1 SMArT ANR-13-IS02-0001 of the Agence Nationale de la Recherche, by the H2020-FETOPEN-2016-2017-CSA project SC2 (712689), and by the European Research Council (ERC) starting grant Matryoshka (713999).

Funders	Funder number
ANR/DFG	STU 483/2-1 SMArT ANR-13-IS02-0001
Horizon 2020 Framework Programme	713999, 712689
European Research Council
Agence Nationale de la Recherche	SC2

UN SDGs

This output contributes to the following UN Sustainable Development Goals (SDGs)

Access to Document

10.4204/EPTCS.262.3

Persistent URL (handle)

Copy link address

Cite this

@article{0c46c228576141a3bc3db10eb040a919,

title = "Language and Proofs for Higher-Order SMT (Work in Progress)",

abstract = "Satisfiability modulo theories (SMT) solvers have throughout the years been able to cope with increasingly expressive formulas, from ground logics to full first-order logic modulo theories. Nevertheless, higher-order logic within SMT is still little explored. One main goal of the Matryoshka project, which started inMarch 2017, is to extend the reasoning capabilities of SMT solvers and other automatic provers beyond first-order logic. In this preliminary report, we report on an extension of the SMT-LIB language, the standard input format of SMT solvers, to handle higher-order constructs. We also discuss how to augment the proof format of the SMT solver veriT to accommodate these new constructs and the solving techniques they require.",

author = "Haniel Barbosa and Blanchette, {Jasmin Christian} and Simon Cruanes and {El Ouraoui}, Daniel and Pascal Fontaine",

year = "2017",

doi = "10.4204/EPTCS.262.3",

language = "English",

volume = "262",

pages = "15--22",

journal = "Electronic Proceedings in Theoretical Computer Science",

issn = "2075-2180",

publisher = "Open Publishing Association",

number = "262",

}

TY - JOUR

T1 - Language and Proofs for Higher-Order SMT (Work in Progress)

AU - Barbosa, Haniel

AU - Blanchette, Jasmin Christian

AU - Cruanes, Simon

AU - El Ouraoui, Daniel

AU - Fontaine, Pascal

PY - 2017

Y1 - 2017

N2 - Satisfiability modulo theories (SMT) solvers have throughout the years been able to cope with increasingly expressive formulas, from ground logics to full first-order logic modulo theories. Nevertheless, higher-order logic within SMT is still little explored. One main goal of the Matryoshka project, which started inMarch 2017, is to extend the reasoning capabilities of SMT solvers and other automatic provers beyond first-order logic. In this preliminary report, we report on an extension of the SMT-LIB language, the standard input format of SMT solvers, to handle higher-order constructs. We also discuss how to augment the proof format of the SMT solver veriT to accommodate these new constructs and the solving techniques they require.

AB - Satisfiability modulo theories (SMT) solvers have throughout the years been able to cope with increasingly expressive formulas, from ground logics to full first-order logic modulo theories. Nevertheless, higher-order logic within SMT is still little explored. One main goal of the Matryoshka project, which started inMarch 2017, is to extend the reasoning capabilities of SMT solvers and other automatic provers beyond first-order logic. In this preliminary report, we report on an extension of the SMT-LIB language, the standard input format of SMT solvers, to handle higher-order constructs. We also discuss how to augment the proof format of the SMT solver veriT to accommodate these new constructs and the solving techniques they require.

UR - http://www.scopus.com/inward/record.url?scp=85045685151&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85045685151&partnerID=8YFLogxK

U2 - 10.4204/EPTCS.262.3

DO - 10.4204/EPTCS.262.3

M3 - Article

SN - 2075-2180

VL - 262

SP - 15

EP - 22

JO - Electronic Proceedings in Theoretical Computer Science

JF - Electronic Proceedings in Theoretical Computer Science

IS - 262

ER -

Language and Proofs for Higher-Order SMT (Work in Progress)

Abstract

Funding

UN SDGs

Access to Document

Persistent URL (handle)

Other files and links

Fingerprint

Cite this