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
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
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
CERES for First-Order Schemata, pp.978-981, 2013. ,
Untersuchungen ???ber das logische Schlie???en. I, Mathematische Zeitschrift, vol.39, issue.1, pp.176-21010, 1935. ,
DOI : 10.1007/BF01201353
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
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
A compact representation of proofs, Studia Logica, vol.19, issue.4, pp.347-37010, 1987. ,
DOI : 10.1007/BF00370646
PROOFCERT ??? Broad Spectrum Proof Certificates ??? ERC, Impact, vol.2017, issue.3, 2011. ,
DOI : 10.21820/23987073.2017.3.68
Restricting backtracking in connection calculi. AI Commun, pp.159-182, 2010. ,
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
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
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