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.
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.
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.
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.
Gerhard Gentzen (1935):
Untersuchungen über das logische Schließen I.
Mathematische Zeitschrift 39(1),
pp. 176–210,
doi:10.1007/BF01201353.
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.
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.
Dale Miller (1987):
A compact representation of proofs.
Studia Logica 46(4),
pp. 347–370,
doi:10.1007/BF00370646.
Dale Miller (2011):
ProofCert: Broad Spectrum Proof Certificates.
ERC Advanced Grant 2012-2016.
Jens Otten (2010):
Restricting backtracking in connection calculi.
AI Commun. 23(2-3),
pp. 159–182,
doi:10.3233/AIC-2010-0464.
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.
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.
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).
eptcs@eptcs.org