H. Amjad, Compressing Propositional Refutations, Sixth International Workshop on Automated Verification of Critical Systems (AVOCS '06) ? Preliminary Proceedings, pp.7-18, 2006.
DOI : 10.1016/j.entcs.2007.05.025

URL : https://hal.archives-ouvertes.fr/inria-00089495

H. Amjad, Data Compression for Proof Replay, Journal of Automated Reasoning, vol.14, issue.3, pp.193-218, 2008.
DOI : 10.1007/s10817-008-9109-2

O. Bar-ilan, O. Fuhrmann, S. Hoory, O. Shacham, and O. Strichman, Linear-Time Reductions of Resolution Proofs, HVC '08: 4th Intl. Haifa Verification Conf. on Hardware and Software, pp.114-128, 2009.
DOI : 10.1007/3-540-44798-9_4

S. Böhme and T. Weber, Fast LCF-Style Proof Reconstruction for Z3, Interactive Theorem Proving, 2010.
DOI : 10.1007/978-3-642-14052-5_14

T. Bouton, D. Caminha, B. De-oliveira, D. Deharbe, and P. Fontaine, veriT: An Open, Trustable and Efficient SMT-Solver, 22nd Intl. Conf. Automated Deduction (CADE-22), 2009.
DOI : 10.1007/978-3-540-73595-3_38

URL : https://hal.archives-ouvertes.fr/inria-00430634

A. Ciabattoni and A. Leitsch, Towards an algorithmic construction of cut-elimination procedures, Mathematical Structures in Computer Science, vol.2381, issue.01, 2008.
DOI : 10.1007/BF01201353

A. Cimatti, A. Griggio, and R. Sebastiani, A Simple and Flexible Way of Computing Small Unsatisfiable Cores in SAT Modulo Theories, Theory and Applications of Satisfiability Testing (SAT), pp.334-339, 2007.
DOI : 10.1007/978-3-540-72788-0_32

S. Cotton, Some techniques for minimizing resolution proofs, Theory and Applications of Satisfiability Testing (SAT), 2010.

P. Fontaine, J. Marion, S. Merz, L. P. Nieto, and A. Tiu, Expressiveness + Automation + Soundness: Towards Combining SMT Solvers and Interactive Proof Assistants, 12th Intl. Conf. Tools and Algorithms for the Construction and Analysis of Systems, pp.167-181, 2006.
DOI : 10.1007/3-540-45620-1_26

URL : https://hal.archives-ouvertes.fr/inria-00001088

J. Girard, Proof-nets: The parallel syntax for proof-theory, Logic and Algebra, 1996.

A. Guglielmi and T. Gundersen, Normalisation Control in Deep Inference via Atomic Flows, Logical Methods in Computer Science, vol.4, issue.1, pp.1-36, 2008.
DOI : 10.2168/LMCS-4(1:9)2008

R. Jhala and K. L. Mcmillan, Interpolant-based transition relation approximation, Logical Methods in Computer Science, vol.3, issue.4, 2007.
DOI : 10.1007/11513988_6

URL : http://arxiv.org/abs/0706.0523

A. Leitsch, The resolution calculus, 1997.
DOI : 10.1007/978-3-642-60605-2

D. Oe, A. Reynolds, and A. Stump, Fast and flexible proof checking for SMT, Proceedings of the 7th International Workshop on Satisfiability Modulo Theories, SMT '09, pp.14-29, 2009.
DOI : 10.1145/1670412.1670414