peter-2015.bib

@comment{{This file has been generated by bib2bib 1.99}}

@comment{{Command line: bib2bib -c 'year=2015 and not annote:"skip_html" and not annote:"unpublished"' -ob peter-2015.bib -oc peter-2015.cite peter.bib}}

@inproceedings{Baumgartner:SMTtoTPTP:CADE:2015,
  author = {Peter Baumgartner},
  title = {{SMTtoTPTP} -- {A} {C}onverter for {T}heorem {P}roving {F}ormats},
  booktitle = {CADE-25 -- The 25th International Conference on Automated
		  Deduction},
  editor = {Amy Felty and Aart Middeldorp},
  year = {2015},
  series = {LNAI},
  volume = {9195},
  pages = {285--294},
  series = {LNAI},
  copyright = {Copyright Springer Verlag \url{http://www.springer.de/comp/lncs/index.html}},
  publisher = {Springer},
  url = {SMTtoTPTP.pdf},
  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.}
}

@inproceedings{Baumgartner:Bax:Waldmann:Beagle:CADE:2015,
  author = {Peter Baumgartner and Joshua Bax and Uwe Waldmann},
  title = {{Beagle} -- {A} {H}ierarchic {S}uperposition {T}heorem {P}rover},
  booktitle = {CADE-25 -- 25th International Conference on Automated
		  Deduction},
  editor = {Amy P. Felty and Aart Middeldorp},
  year = {2015},
  series = {LNAI},
  volume = {9195},
  pages = {367--377},
  copyright = {Copyright Springer Verlag \url{http://www.springer.de/comp/lncs/index.html}},
  publisher = {Springer},
  url = {Beagle.pdf},
  abstract = {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.}
}