@incollection(Armand2011,
 author       = {Michael Armand and Germain Faure and Benjamin Grégoire and Chantal Keller and Laurent Théry and Benjamin Werner},
 year         = {2011},
 title        = {A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses},
 booktitle    = {CPP},
 series       = {Lecture Notes in Computer Science},
 publisher    = {Springer Berlin Heidelberg},
 pages        = {135--150},
 doi          = {10.1007/978-3-642-25379-9\_12},
)
@article(ceres,
 author       = {Matthias Baaz and Alexander Leitsch},
 year         = {2000},
 title        = {Cut-elimination and Redundancy-elimination by Resolution},
 journal      = {Journal of Symbolic Computation},
 volume       = {29},
 number       = {2},
 pages        = {149--176},
 doi          = {10.1006/jsco.1999.0359},
)
@inproceedings(dunchev13,
 author       = {Cvetan Dunchev and Alexander Leitsch and Tomer Libal and Martin Riener and Mikheil Rukhaia and Daniel Weller and Bruno Woltzenlogel Paleo},
 year         = {2013},
 title        = {{PROOFTOOL:} a {GUI} for the {GAPT} Framework},
 booktitle    = {10th {UITP}},
 series       = {{EPTCS}},
 volume       = {118},
 pages        = {1--14},
 doi          = {10.4204/EPTCS.118.1},
)
@article(weller13,
 author       = {Cvetan Dunchev and Alexander Leitsch and Mikheil Rukhaia and Daniel Weller},
 year         = {2013},
 title        = {{CERES} for First-Order Schemata},
 journal      = {CoRR},
 volume       = {abs/1303.4257},
 doi          = {10.1007/978-3-662-46906-4\_8},
)
@article(gentzen35,
 author       = {Gerhard Gentzen},
 year         = {1935},
 title        = {{U}ntersuchungen \"uber das logische {S}chlie{\ss}en {I}},
 journal      = {Mathematische Zeitschrift},
 volume       = {39},
 number       = {1},
 pages        = {176--210},
 doi          = {10.1007/BF01201353},
)
@inproceedings(hetzl14,
 author       = {Stefan Hetzl and Alexander Leitsch and Giselle Reis and Janos Tapolczai and Daniel Weller},
 year         = {2014},
 title        = {Introducing Quantified Cuts in Logic with Equality},
 booktitle    = {7th {IJCAR}},
 series       = {Lecture Notes in Computer Science},
 volume       = {8562},
 publisher    = {Springer},
 pages        = {240--254},
 doi          = {10.1007/978-3-319-08587-6\_17},
)
@inproceedings(KaliszykCPP2015,
 author       = {Cezary Kaliszyk and Josef Urban and Vysko\v{c}il, Ji\v{r}i},
 year         = {2015},
 title        = {Certified Connection Tableaux Proofs for HOL Light and TPTP},
 series       = {CPP '15},
 publisher    = {ACM},
 address      = {New York, NY, USA},
 pages        = {59--66},
 doi          = {10.1145/2676724.2693176},
)
@article(miller87,
 author       = {Dale Miller},
 year         = {1987},
 title        = {A compact representation of proofs},
 journal      = {Studia Logica},
 volume       = {46},
 number       = {4},
 pages        = {347--370},
 doi          = {10.1007/BF00370646},
)
@unpublished(proofcert,
 author       = {Dale Miller},
 year         = {2011},
 title        = {ProofCert: Broad Spectrum Proof Certificates},
 note         = {ERC Advanced Grant 2012-2016},
)
@article(otten10,
 author       = {Jens Otten},
 year         = {2010},
 title        = {Restricting backtracking in connection calculi},
 journal      = {{AI} Commun.},
 volume       = {23},
 number       = {2-3},
 pages        = {159--182},
 doi          = {10.3233/AIC-2010-0464},
)
@article(robinson65,
 author       = {J. A. Robinson},
 year         = {1965},
 title        = {A Machine-Oriented Logic Based on the Resolution Principle},
 journal      = {J. ACM},
 volume       = {12},
 number       = {1},
 pages        = {23--41},
 doi          = {10.1145/321250.321253},
)
@article(tptp,
 author       = {G. Sutcliffe},
 year         = {2009},
 title        = {{The TPTP Problem Library and Associated Infrastructure: The FOF and CNF Parts, v3.5.0}},
 journal      = {Journal of Automated Reasoning},
 volume       = {43},
 number       = {4},
 pages        = {337--362},
 doi          = {10.1007/s10817-009-9143-8},
)
@article(Sutcliffe2007,
 author       = {Steven Trac and Yury Puzis and Geoff Sutcliffe},
 year         = {2007},
 title        = {An Interactive Derivation Viewer},
 journal      = {Electronic Notes in Theoretical Computer Science},
 volume       = {174},
 number       = {2},
 pages        = {109 -- 123},
 doi          = {10.1016/j.entcs.2006.09.025},
 note         = {Proceedings of the 7th Workshop on User Interfaces for Theorem Provers (UITP 2006)},
)