Skip to main content

TS

SMTtoTPTP - a converter for theorem proving formats

Authors

Peter Baumgartner

NICTA

Abstract

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

  @inproceedings{Baumgartner_15,
    author           = {Baumgartner, Peter},
    month            = aug,
    slides           = {http://ts.data61.csiro.au/publications/nicta_slides/8727.pdf},
    year             = {2015},
    keywords         = {satisfiability modulo theories, first-order theorem proving},
    title            = {{SMTtoTPTP} - A Converter for Theorem Proving Formats},
    booktitle        = {International Conference on Automated Deduction},
    pages            = {285-294},
    address          = {Berlin, Germany}
  }

Download

Served by Apache on Linux on seL4.
Served by Apache on Linux on seL4.