Sie befinden Sich nicht im Netzwerk der Universität Paderborn. Der Zugriff auf elektronische Ressourcen ist gegebenenfalls nur via VPN oder Shibboleth (DFN-AAI) möglich. mehr Informationen...
SMTtoTPTP – A Converter for Theorem Proving Formats
Ist Teil von
Automated Deduction - CADE-25, p.285-294
Ort / Verlag
Cham: Springer International Publishing
Link zum Volltext
Quelle
Alma/SFX Local Collection
Beschreibungen/Notizen
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.