SMTtoTPTP – A converter for theorem proving formats

Peter Baumgartner

doi:10.1007/978-3-319-21401-6_19

SMTtoTPTP – A converter for theorem proving formats

Peter Baumgartner^*

^*Corresponding author for this work

Research output: Contribution to journal › Conference article › peer-review

3 Citations (Scopus)

Abstract

SMTtoTPTP is a converter from proof problems written in the SMT-LIB format into the TPTP TFF format. The SMT-LIB format supports polymorphic sorts and frequently used theories like those of uninterpreted function symbols, arrays, and certain forms of arithmetics. The TPTP TFF format is an extension of the TPTP format widely used by automated theorem provers, adding a sort system and arithmetic theories. SMTtoTPTP is useful for, e.g., making SMT-LIB problems available to TPTP system developers, and for making TPTP systems available to users of SMT solvers. This paper describes how the conversion works, its functionality and limitations.

Original language	English
Pages (from-to)	285-294
Number of pages	10
Journal	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	9195
DOIs	https://doi.org/10.1007/978-3-319-21401-6_19
Publication status	Published - 2015
Event	25th International Conference on Automated Deduction CADE 2015 - Berlin, Germany Duration: 1 Aug 2015 → 7 Aug 2015

Access to Document

10.1007/978-3-319-21401-6_19

Cite this

@article{6db26c24f697465eb9bc7cdb0402542d,

title = "SMTtoTPTP – A converter for theorem proving formats",

abstract = "SMTtoTPTP is a converter from proof problems written in the SMT-LIB format into the TPTP TFF format. The SMT-LIB format supports polymorphic sorts and frequently used theories like those of uninterpreted function symbols, arrays, and certain forms of arithmetics. The TPTP TFF format is an extension of the TPTP format widely used by automated theorem provers, adding a sort system and arithmetic theories. SMTtoTPTP is useful for, e.g., making SMT-LIB problems available to TPTP system developers, and for making TPTP systems available to users of SMT solvers. This paper describes how the conversion works, its functionality and limitations.",

author = "Peter Baumgartner",

note = "Publisher Copyright: {\textcopyright} Springer International Publishing Switzerland 2015.; 25th International Conference on Automated Deduction CADE 2015 ; Conference date: 01-08-2015 Through 07-08-2015",

year = "2015",

doi = "10.1007/978-3-319-21401-6_19",

language = "English",

volume = "9195",

pages = "285--294",

journal = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

issn = "0302-9743",

publisher = "Springer Verlag",

}

TY - JOUR

T1 - SMTtoTPTP – A converter for theorem proving formats

AU - Baumgartner, Peter

N1 - Publisher Copyright: © Springer International Publishing Switzerland 2015.

PY - 2015

Y1 - 2015

N2 - SMTtoTPTP is a converter from proof problems written in the SMT-LIB format into the TPTP TFF format. The SMT-LIB format supports polymorphic sorts and frequently used theories like those of uninterpreted function symbols, arrays, and certain forms of arithmetics. The TPTP TFF format is an extension of the TPTP format widely used by automated theorem provers, adding a sort system and arithmetic theories. SMTtoTPTP is useful for, e.g., making SMT-LIB problems available to TPTP system developers, and for making TPTP systems available to users of SMT solvers. This paper describes how the conversion works, its functionality and limitations.

AB - SMTtoTPTP is a converter from proof problems written in the SMT-LIB format into the TPTP TFF format. The SMT-LIB format supports polymorphic sorts and frequently used theories like those of uninterpreted function symbols, arrays, and certain forms of arithmetics. The TPTP TFF format is an extension of the TPTP format widely used by automated theorem provers, adding a sort system and arithmetic theories. SMTtoTPTP is useful for, e.g., making SMT-LIB problems available to TPTP system developers, and for making TPTP systems available to users of SMT solvers. This paper describes how the conversion works, its functionality and limitations.

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

U2 - 10.1007/978-3-319-21401-6_19

DO - 10.1007/978-3-319-21401-6_19

M3 - Conference article

SN - 0302-9743

VL - 9195

SP - 285

EP - 294

JO - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

JF - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

T2 - 25th International Conference on Automated Deduction CADE 2015

Y2 - 1 August 2015 through 7 August 2015

ER -

SMTtoTPTP – A converter for theorem proving formats

Abstract

Access to Document

Other files and links

Fingerprint

Cite this