1. Jean-Marc Andreoli (1992): Logic Programming with Focusing Proofs in Linear Logic. J. Log. Comput. 2(3), pp. 297–347, doi:10.1093/logcom/2.3.297.
  2. A. Biere, A. Cimatti, E. M. Clarke, M. Fujita & Y. Zhu (1999): Symbolic Model Checking Using SAT Procedures Instead of BDDs. In: Proceedings of the 36th Annual ACM/IEEE Design Automation Conference, DAC '99. ACM, New York, NY, USA, pp. 317–320, doi:10.1145/309847.309942.
  3. Armin Biere (2013): Lingeling, Plingeling and Treengeling entering the SAT competition 2013. Proceedings of SAT Competition 2013.
  4. Zakaria Chihani, Tomer Libal & Giselle Reis (2015): The Proof Certifier Checkers, pp. 201–210. Springer International Publishing, Cham, doi:10.1007/978-3-319-24312-2_14. Available at
  5. Gerhard Gentzen (1935): Untersuchungen über das logische Schließen. I. Mathematische Zeitschrift 39(1), pp. 176–210, doi:10.1007/BF01201353.
  6. Marijn Heule & Armin Biere (2015): Proofs for Satisfiability Problems. In: All about Proofs, Proofs for All (APPA), Mathematical Logic and Foundations 55. College Publications, pp. 1–22.
  7. Jean-Pierre Jouannaud, Pierre-Yves Strub & Lianyi Zhang (2010): Certification of SAT Solvers in Coq. In: Guangzhou Symposium on Satisfiability in Logic-Based Modeling, Proc. Guangzhou Symposium on Satisfiability in Logic-Based Modeling. Yuping Shen, Institute of Logic and Cognition Sun Yat-sen University, Guangzhou., Zuhai, China. Available at
  8. Henry A. Kautz & Bart Selman (1996): Pushing the Envelope: Planning, Propositional Logic and Stochastic Search. In: 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., pp. 1194–1201. Available at
  9. Peter Lammich (2017): Efficient Verified (UN)SAT Certificate Checking, pp. 237–254. Springer International Publishing, Cham, doi:10.1007/978-3-319-63046-5_15. Available at
  10. Chuck Liang & Dale Miller (2009): Focusing and polarization in linear, intuitionistic, and classical logics. Theor. Comput. Sci. 410(46), pp. 4747–4768, doi:10.1016/j.tcs.2009.07.041.
  11. Fabio Massacci & Laura Marraro (2000): Logical Cryptanalysis as a SAT Problem. Journal of Automated Reasoning 24(1), pp. 165–203, doi:10.1023/A:1006326723002. Available at
  12. Dale Miller (2011): ProofCert: Broad Spectrum Proof Certificates. An ERC Advanced Grant funded for the five years 2012-2016.
  13. Nathan Wetzler, Marijn J. H. Heule & Warren A. Hunt (2014): DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs, pp. 422–429. Springer International Publishing, Cham, doi:10.1007/978-3-319-09284-3_31. Available at

Comments and questions to:
For website issues: