G. Gentzen, UntersuchungenüberUntersuchungen¨Untersuchungenüber das logische Schließen II, Mathematische Zeitschrift, vol.39, issue.3, pp.405-431, 1935.
DOI : 10.1007/bf01201363

J. Goubault, -. , and I. Mackie, Proof theory and automated deduction, 1997.

A. Haken, The intractability of resolution, Theor. Comput. Sci, vol.39, pp.297-308, 1985.
DOI : 10.1016/0304-3975(85)90144-6
URL : https://doi.org/10.1016/0304-3975(85)90144-6

D. Knuth, The art of computer programming, Combinatorial algorithsms, Part, vol.4, 2012.

D. Knuth, The art of computer programming, Combinatorial algorithms, vol.4, 2018.

M. Mitzenmacher and E. Upfal, Probability and computing : randomized algorithms and probabilistic analysis, 2005.

R. John-alan, A machine-oriented logic based on the resolution principle, J. ACM, vol.12, issue.1, pp.23-41, 1965.

G. Tseitin, On the complexity of derivation in propositional calculus, Studies in Constructive Mathematics and Mathematical Logic, Part II, pp.115-125, 1970.

E. Tomás, M. E. Uribe, and . Stickel, Ordered binary decision diagrams and the Davis-Putnam procedure, Constraints in Computational Logics, First International Conference, CCL'94, pp.34-49, 1994.

S. Warshall, A theorem on boolean matrices, J. ACM, vol.9, issue.1, pp.11-12, 1962.
DOI : 10.1145/321105.321107