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.
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.
Armin Biere (2013):
Lingeling, Plingeling and Treengeling entering the SAT competition 2013.
Proceedings of SAT Competition 2013.
Gerhard Gentzen (1935):
Untersuchungen über das logische Schließen. I.
Mathematische Zeitschrift 39(1),
pp. 176–210,
doi:10.1007/BF01201353.
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.
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 https://hal.inria.fr/inria-00516906.
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 http://www.aaai.org/Library/AAAI/1996/aaai96-177.php.
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.