1. Michael Armand, Germain Faure, Benjamin Grégoire, Chantal Keller, Laurent Théry & Benjamin Werner (2011): A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses. In: CPP, Lecture Notes in Computer Science. Springer Berlin Heidelberg, pp. 135–150, doi:10.1007/978-3-642-25379-9_12.
  2. Matthias Baaz & Alexander Leitsch (2000): Cut-elimination and Redundancy-elimination by Resolution. Journal of Symbolic Computation 29(2), pp. 149–176, doi:10.1006/jsco.1999.0359.
  3. Cvetan Dunchev, Alexander Leitsch, Tomer Libal, Martin Riener, Mikheil Rukhaia, Daniel Weller & Bruno Woltzenlogel Paleo (2013): PROOFTOOL: a GUI for the GAPT Framework. In: 10th UITP, EPTCS 118, pp. 1–14, doi:10.4204/EPTCS.118.1.
  4. Cvetan Dunchev, Alexander Leitsch, Mikheil Rukhaia & Daniel Weller (2013): CERES for First-Order Schemata. CoRR abs/1303.4257, doi:10.1007/978-3-662-46906-4_8.
  5. Gerhard Gentzen (1935): Untersuchungen über das logische Schließen I. Mathematische Zeitschrift 39(1), pp. 176–210, doi:10.1007/BF01201353.
  6. Stefan Hetzl, Alexander Leitsch, Giselle Reis, Janos Tapolczai & Daniel Weller (2014): Introducing Quantified Cuts in Logic with Equality. In: 7th IJCAR, Lecture Notes in Computer Science 8562. Springer, pp. 240–254, doi:10.1007/978-3-319-08587-6_17.
  7. Cezary Kaliszyk, Josef Urban & Jiři Vyskočil (2015): Certified Connection Tableaux Proofs for HOL Light and TPTP. CPP '15. ACM, New York, NY, USA, pp. 59–66, doi:10.1145/2676724.2693176.
  8. Dale Miller (1987): A compact representation of proofs. Studia Logica 46(4), pp. 347–370, doi:10.1007/BF00370646.
  9. Dale Miller (2011): ProofCert: Broad Spectrum Proof Certificates. ERC Advanced Grant 2012-2016.
  10. Jens Otten (2010): Restricting backtracking in connection calculi. AI Commun. 23(2-3), pp. 159–182, doi:10.3233/AIC-2010-0464.
  11. J. A. Robinson (1965): A Machine-Oriented Logic Based on the Resolution Principle. J. ACM 12(1), pp. 23–41, doi:10.1145/321250.321253.
  12. G. Sutcliffe (2009): The TPTP Problem Library and Associated Infrastructure: The FOF and CNF Parts, v3.5.0. Journal of Automated Reasoning 43(4), pp. 337–362, doi:10.1007/s10817-009-9143-8.
  13. Steven Trac, Yury Puzis & Geoff Sutcliffe (2007): An Interactive Derivation Viewer. Electronic Notes in Theoretical Computer Science 174(2), pp. 109 – 123, doi:10.1016/j.entcs.2006.09.025. Proceedings of the 7th Workshop on User Interfaces for Theorem Provers (UITP 2006).

Comments and questions to:
For website issues: