@article(andreoli1992logic,
 author       = {Jean{-}Marc Andreoli},
 year         = {1992},
 title        = {Logic Programming with Focusing Proofs in Linear Logic},
 journal      = {J. Log. Comput.},
 volume       = {2},
 number       = {3},
 pages        = {297--347},
 doi          = {10.1093/logcom/2.3.297},
)
@inproceedings(biere1999symbolic,
 author       = {A. Biere and A. Cimatti and E. M. Clarke and M. Fujita and Y. Zhu},
 year         = {1999},
 title        = {Symbolic Model Checking Using SAT Procedures Instead of BDDs},
 booktitle    = {Proceedings of the 36th Annual ACM/IEEE Design Automation Conference},
 series       = {DAC '99},
 publisher    = {ACM},
 address      = {New York, NY, USA},
 pages        = {317--320},
 doi          = {10.1145/309847.309942},
)
@article(biere2013lingeling,
 author       = {Armin Biere},
 year         = {2013},
 title        = {Lingeling, Plingeling and Treengeling entering the SAT competition 2013},
 journal      = {Proceedings of SAT Competition},
 volume       = {2013},
)
@inbook(chihani2015proof,
 author       = {Zakaria Chihani and Tomer Libal and Giselle Reis},
 year         = {2015},
 title        = {The Proof Certifier Checkers},
 pages        = {201--210},
 publisher    = {Springer International Publishing},
 address      = {Cham},
 doi          = {10.1007/978-3-319-24312-2_14},
 url          = {https://doi.org/10.1007/978-3-319-24312-2_14},
)
@article(Gentzen1935,
 author       = {Gerhard Gentzen},
 year         = {1935},
 title        = {Untersuchungen {\"u}ber das logische Schlie{\ss}en. I},
 journal      = {Mathematische Zeitschrift},
 volume       = {39},
 number       = {1},
 pages        = {176--210},
 doi          = {10.1007/BF01201353},
)
@inproceedings(biere2015,
 author       = {Marijn Heule and Armin Biere},
 year         = {2015},
 title        = {Proofs for Satisfiability Problems},
 booktitle    = {All about Proofs, Proofs for All (APPA), Mathematical Logic and Foundations},
 volume       = {55},
 publisher    = {College Publications},
 pages        = {1--22},
)
@inproceedings(jouannaud2010certification,
 author       = {Jean-Pierre Jouannaud and Pierre-Yves Strub and Lianyi Zhang},
 year         = {2010},
 title        = {{Certification of SAT Solvers in Coq}},
 booktitle    = {{Guangzhou Symposium on Satisfiability in Logic-Based Modeling}},
 series       = {Proc. Guangzhou Symposium on Satisfiability in Logic-Based Modeling},
 organization = {{Yuping Shen, Institute of Logic and Cognition Sun Yat-sen University, Guangzhou.}},
 address      = {Zuhai, China},
 url          = {https://hal.inria.fr/inria-00516906},
)
@inproceedings(kautz1996pushing,
 author       = {Henry A. Kautz and Bart Selman},
 year         = {1996},
 title        = {Pushing the Envelope: Planning, Propositional Logic and Stochastic Search},
 booktitle    = {Proceedings of the Thirteenth National Conference on Artificial Intelligence and Eighth Innovative Applications of Artificial Intelligence Conference, {AAAI} 96, {IAAI} 96, Portland, Oregon, August 4-8, 1996, Volume 2.},
 pages        = {1194--1201},
 url          = {http://www.aaai.org/Library/AAAI/1996/aaai96-177.php},
)
@inbook(lammich17,
 author       = {Peter Lammich},
 year         = {2017},
 title        = {Efficient Verified (UN)SAT Certificate Checking},
 pages        = {237--254},
 publisher    = {Springer International Publishing},
 address      = {Cham},
 doi          = {10.1007/978-3-319-63046-5_15},
 url          = {https://doi.org/10.1007/978-3-319-63046-5_15},
)
@article(LiaMil09,
 author       = {Chuck Liang and Dale Miller},
 year         = {2009},
 title        = {Focusing and polarization in linear, intuitionistic, and classical logics},
 journal      = {Theor. Comput. Sci.},
 volume       = {410},
 number       = {46},
 pages        = {4747--4768},
 doi          = {10.1016/j.tcs.2009.07.041},
)
@article(massacci2000logical,
 author       = {Fabio Massacci and Laura Marraro},
 year         = {2000},
 title        = {Logical Cryptanalysis as a SAT Problem},
 journal      = {Journal of Automated Reasoning},
 volume       = {24},
 number       = {1},
 pages        = {165--203},
 doi          = {10.1023/A:1006326723002},
 url          = {https://doi.org/10.1023/A:1006326723002},
)
@unpublished(erc,
 author       = {Dale Miller},
 year         = {2011},
 title        = {ProofCert: Broad Spectrum Proof Certificates},
 note         = {An ERC Advanced Grant funded for the five years 2012-2016},
)
@inbook(wetzler2014drat,
 author       = {Nathan Wetzler and Marijn J. H. Heule and Warren A. Hunt},
 year         = {2014},
 title        = {DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs},
 pages        = {422--429},
 publisher    = {Springer International Publishing},
 address      = {Cham},
 doi          = {10.1007/978-3-319-09284-3_31},
 url          = {https://doi.org/10.1007/978-3-319-09284-3_31},
)