Skip to main content

SMTtoTPTP — a converter for theorem proving formats


Peter Baumgartner



SMTtoTPTP is a converter from proof problems written in the SMT-LIB format into the TPTP TFF format. It is useful for exchanging proof problems between SMT-Solvers and first-order theorem provers. In particular, the existing (large) SMT-LIB problem libraries could be made available to the first-order theorem proving world. The SMT-LIB format supports polymorphic data structures and frequently used theories like arrays and various forms of arithmetics. Because the SMT-LIB format is much richer than the (monomorphic) TPTP TFF format the conversion is not quite trivial. This paper describes how the conversion works and provides an overview of SMTtoTPTP's functionality and current limitations.

BibTeX Entry

    month            = aug,
    keywords         = {satisfiability modulo theories, first-order theorem proving},
    paperurl         = {},
    booktitle        = {International Conference on Automated Deduction},
    slides           = {},
    author           = {Baumgartner, Peter},
    year             = {2015},
    pages            = {285--294},
    title            = {{SMTtoTPTP} --- A Converter for Theorem Proving Formats},
    address          = {Berlin, Germany}