A. Balint, D. Gall, G. Kapler, and R. Retz, R.: Experiment design and administration for computer clusters for sat-solvers (edacc, JSAT, 2010.

M. Boespflug, Q. Carbonneaux, and O. Hermant, The ??-calculus modulo as a universal proof language, Proceedings of PxTP2012: Proof Exchange for Theorem Proving, pp.28-43, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00917845

Z. Chihani, D. Miller, and F. Renaud, Checking foundational proof certificates for first-order logic (extended abstract), Third International Workshop on Proof Exchange for Theorem Proving, pp.58-66, 2013.

Z. Chihani, D. Miller, and F. Renaud, Foundational Proof Certificates in First-Order Logic, Conference on Automated Deduction 2013, pp.162-177, 2013.
DOI : 10.1007/978-3-642-38574-2_11
URL : https://hal.archives-ouvertes.fr/hal-00906485

A. Grabowski, A. Kornilowicz, and A. Naumowicz, Mizar in a nutshell, Journal of Formalized Reasoning, vol.3, issue.2, pp.153-245, 1980.

C. Liang and D. Miller, Focusing and polarization in linear, intuitionistic, and classical logics, Theoretical Computer Science, vol.410, issue.46, pp.4747-4768, 2009.
DOI : 10.1016/j.tcs.2009.07.041

D. Miller, Proofcert: Broad spectrum proof certificates), an ERC Advanced Grant funded for the five years, pp.2012-2016, 2011.

D. Miller and G. Nadathur, Programming with Higher-Order Logic, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00776197

J. Otten and G. Sutcliffe, Using the tptp language for representing derivations in tableau and connection calculi, EPiC Series EasyChair, vol.9, pp.95-105, 2012.

G. Robinson and L. Wos, Paramodulation and theorem-proving in first-order theories with equality, Automation of Reasoning, pp.298-313, 1983.

S. Schulz, System Description: E??1.8, Logic for Programming, pp.735-743, 2013.
DOI : 10.1007/978-3-642-45221-5_49

A. Stump, A. Reynolds, C. Tinelli, A. Laugesen, H. Eades et al., Lfsc for smt proofs: Work in progress