@article(Bachmair1994,
 author       = {Leo Bachmair and Harald Ganzinger},
 year         = {1994},
 title        = {{Rewrite-Based Equational Theorem Proving with Selection and Simplification}},
 journal      = {Journal of Logic and Computation},
 volume       = {4},
 number       = {3},
 pages        = {217--247},
 doi          = {10.1093/logcom/4.3.217},
)
@incollection(Barbosa2017-proofs,
 author       = {Haniel Barbosa and Jasmin Christian Blanchette and Pascal Fontaine},
 year         = {2017},
 title        = {Scalable Fine-Grained Proofs for Formula Processing},
 editor       = {Leonardo de Moura},
 booktitle    = {Conference on Automated Deduction (CADE)},
 series       = {LNCS},
 volume       = {10395},
 publisher    = {Springer},
 pages        = {398--412},
 doi          = {10.1007/978-3-319-63046-5_25},
)
@techreport(Barbosa2017-proofs-extended,
 author       = {Haniel Barbosa and Jasmin Christian Blanchette and Pascal Fontaine},
 year         = {2017},
 title        = {{Scalable Fine-Grained Proofs for Formula Processing}},
 type         = {Research Report},
 institution  = {Inria},
 doi          = {10.1007/978-3-319-63046-5_25},
 url          = {https://hal.inria.fr/hal-01526841},
)
@inproceedings(Barbosa2017,
 author       = {Haniel Barbosa and Pascal Fontaine and Andrew Reynolds},
 year         = {2017},
 title        = {Congruence Closure with Free Variables},
 editor       = {Axel Legay and Tiziana Margaria},
 booktitle    = {Tools and Algorithms for Construction and Analysis of Systems (TACAS)},
 series       = {LNCS},
 volume       = {10206},
 pages        = {214--230},
 doi          = {10.1007/978-3-662-54580-5_13},
)
@techreport(Barrett2015,
 author       = {Clark Barrett and Pascal Fontaine and Cesare Tinelli},
 year         = {2015},
 title        = {{The SMT-LIB Standard: Version 2.5}},
 type         = {Technical Report},
 institution  = {Department of Computer Science, The University of Iowa},
 note         = {Available at {\tt www.SMT-LIB.org}},
)
@inproceedings(Besson2011,
 author       = {Fr{\'e}d{\'e}ric Besson and Pascal Fontaine and Laurent Th{\'e}ry},
 year         = {2011},
 title        = {A Flexible Proof Format for {SMT}: a Proposal},
 editor       = {Pascal Fontaine and Aaron Stump},
 booktitle    = {Workshop on Proof eXchange for Theorem Proving (PxTP)},
 url          = {https://hal.inria.fr/hal-00642544},
)
@article(Blanchette2016-isar,
 author       = {Jasmin Christian Blanchette and Sascha B{\"{o}}hme and Mathias Fleury and Steffen Juilf Smolka and Albert Steckermeier},
 year         = {2016},
 title        = {Semi-intelligible {I}sar Proofs from Machine-Generated Proofs},
 journal      = {Journal of Automated Reasoning},
 volume       = {56},
 number       = {2},
 pages        = {155--200},
 doi          = {10.1007/s10817-015-9335-3},
)
@article(blanchette-et-al-2016-qed,
 author       = {Jasmin Christian Blanchette and Cezary Kaliszyk and Lawrence C. Paulson and Josef Urban},
 year         = {2016},
 title        = {Hammering towards {QED}},
 journal      = {Journal of Formalized Reasoning},
 volume       = {9},
 number       = {1},
 pages        = {101--148},
 doi          = {10.6092/issn.1972-5787/4593},
)
@inproceedings(bouton2009verit,
 author       = {Thomas Bouton and Diego Caminha B. de Oliveira and David D{\'{e}}harbe and Pascal Fontaine},
 year         = {2009},
 title        = {{veriT}: {A}n {O}pen, {T}rustable and {E}fficient {SMT-S}olver},
 editor       = {Renate A. Schmidt},
 booktitle    = {Conference on Automated Deduction (CADE)},
 series       = {LNCS},
 volume       = {5663},
 publisher    = {Springer},
 pages        = {151--156},
 doi          = {10.1007/978-3-642-02959-2_12},
)
@inproceedings(Ebner2016,
 author       = {Gabriel Ebner and Stefan Hetzl and Giselle Reis and Martin Riener and Simon Wolfsteiner and Sebastian Zivota},
 year         = {2016},
 title        = {System Description: {GAPT} 2.0},
 editor       = {Nicola Olivetti and Ashish Tiwari},
 booktitle    = {International Joint Conference on Automated Reasoning (IJCAR)},
 series       = {LNCS},
 volume       = {9706},
 publisher    = {Springer},
 pages        = {293--301},
 doi          = {10.1007/978-3-319-40229-1_20},
)
@article(Nieuwenhuis2006,
 author       = {Robert Nieuwenhuis and Albert Oliveras and Cesare Tinelli},
 year         = {2006},
 title        = {Solving SAT and SAT Modulo Theories: From an Abstract Davis--Putnam--Logemann--Loveland Procedure to DPLL(T)},
 journal      = {Journal of the ACM},
 volume       = {53},
 number       = {6},
 pages        = {937--977},
 doi          = {10.1145/1217856.1217859},
)
@incollection(Nieuwenhuis2001-har,
 author       = {Robert Nieuwenhuis and Albert Rubio},
 year         = {2001},
 title        = {{Paramodulation-Based Theorem Proving}},
 editor       = {Alan Robinson and Andrei Voronkov},
 booktitle    = {Handbook of Automated Reasoning},
 volume       = {I},
 pages        = {371--443},
 doi          = {10.1016/B978-044450813-3/50009-6},
)
@inproceedings(rosen2015tip,
 author       = {Dan Ros{\'e}n and Nicholas Smallbone},
 year         = {2015},
 title        = {TIP: Tools for Inductive Provers},
 editor       = {Martin Davis and Ansgar Fehnker and Annabelle McIver and Andrei Voronkov},
 booktitle    = {Logic for Programming, Artificial Intelligence, and Reasoning (LPAR)},
 publisher    = {Springer},
 pages        = {219--232},
 doi          = {10.1007/978-3-662-48899-7_16},
)