M. Armand, G. Faure, B. Grgoire, C. Keller, L. Thry et al., A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses, In: CPP, Lecture Notes in Computer Science, vol.53, issue.6, pp.135-150, 2011.
DOI : 10.1145/1217856.1217859
URL : https://hal.archives-ouvertes.fr/hal-00639130

M. Baaz and &. Leitsch, Cut-elimination and Redundancy-elimination by Resolution, Journal of Symbolic Computation, vol.29, issue.2, pp.149-176, 2000.
DOI : 10.1006/jsco.1999.0359

C. Dunchev, A. Leitsch, T. Libal, M. Riener, M. Rukhaia et al., PROOFTOOL: a GUI for the GAPT Framework, Electronic Proceedings in Theoretical Computer Science, vol.118, pp.10-11, 2013.
DOI : 10.4204/EPTCS.118.1

C. Dunchev, A. Leitsch, and D. Weller, CERES for First-Order Schemata, pp.978-981, 2013.

G. Gentzen, Untersuchungen ???ber das logische Schlie???en. I, Mathematische Zeitschrift, vol.39, issue.1, pp.176-21010, 1935.
DOI : 10.1007/BF01201353

S. Hetzl, A. Leitsch, G. Reis, J. Tapolczai, and &. Weller, Introducing Quantified Cuts in Logic with Equality, Lecture Notes in Computer Science, vol.8562, pp.7-240, 2014.
DOI : 10.1007/978-3-319-08587-6_17

C. Kaliszyk, J. Urban, and &. Vysko?il, Certified Connection Tableaux Proofs for HOL Light and TPTP. CPP '15, pp.59-6610, 2015.
DOI : 10.1145/2676724.2693176
URL : http://arxiv.org/abs/1410.5476

D. Miller, A compact representation of proofs, Studia Logica, vol.19, issue.4, pp.347-37010, 1987.
DOI : 10.1007/BF00370646

D. Miller, PROOFCERT ??? Broad Spectrum Proof Certificates ??? ERC, Impact, vol.2017, issue.3, 2011.
DOI : 10.21820/23987073.2017.3.68

J. Otten, Restricting backtracking in connection calculi. AI Commun, pp.159-182, 2010.

J. A. Robinson, A Machine-Oriented Logic Based on the Resolution Principle, Journal of the ACM, vol.12, issue.1, pp.23-41, 1965.
DOI : 10.1145/321250.321253

G. Sutcliffe, The TPTP Problem Library and Associated Infrastructure, Journal of Automated Reasoning, vol.13, issue.2, pp.337-362, 2009.
DOI : 10.1007/s10817-009-9143-8

S. Trac, Y. Puzis, and &. Sutcliffe, An Interactive Derivation Viewer, Proceedings of the 7th Workshop on User Interfaces for Theorem Provers, pp.109-123, 2006.
DOI : 10.1016/j.entcs.2006.09.025