Peter Baumgartner, Joshua Bax, and Uwe Waldmann.
Beagle -- A Hierarchic Superposition Theorem Prover.
In Amy P. Felty and Aart Middeldorp, editors, CADE-25 -- 25th International Conference on Automated Deduction, volume 9195 of LNAI, pages 367--377. Springer, 2015.
Copyright Springer Verlag http://www.springer.de/comp/lncs/index.html. [ bib | .pdf ]
Beagle is an automated theorem prover for first-order logic modulo built-in theories. It implements a refined version of the hierarchic superposition calculus. This system description focuses on Beagle's proof procedure, background reasoning facilities, implementation, and experimental results.
 
Peter Baumgartner.
SMTtoTPTP -- A Converter for Theorem Proving Formats.
In Amy Felty and Aart Middeldorp, editors, CADE-25 -- The 25th International Conference on Automated Deduction, volume 9195 of LNAI, pages 285--294. Springer, 2015.
Copyright Springer Verlag http://www.springer.de/comp/lncs/index.html. [ bib | .pdf ]
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.