The Coq development team (2004):
The Coq proof assistant reference manual.
LogiCal Project.
Available at http://coq.inria.fr.
Version 8.0.
Robert L. Constable, Stuart F. Allen, H. M. Bromley, W. R. Cleaveland, J. F. Cremer, R. W. Harper, Douglas J. Howe, T. B. Knoblock, N. P. Mendler, P. Panangaden, James T. Sasaki & Scott F. Smith (1986):
Implementing Mathematics with the Nuprl Proof Development System.
Prentice-Hall,
NJ.
Tobias Nipkow, Markus Wenzel & Lawrence C. Paulson (2002):
Isabelle/HOL: A Proof Assistant for Higher-order Logic.
Springer-Verlag,
Berlin, Heidelberg,
doi:10.1007/3-540-45949-9.
Ulf Norell (2009):
Dependently Typed Programming in Agda.
In: Proceedings of the 4th International Workshop on Types in Language Design and Implementation,
TLDI '09.
ACM,
New York, NY, USA,
pp. 1–2,
doi:10.1145/1481861.1481862.
Edwin Brady (2013):
Idris, a general-purpose dependently typed programming language: Design and implementation.
Journal of Functional Programming 23,
pp. 552–593,
doi:10.1017/S095679681300018X.
Henk P. Barendregt (1984):
The Lambda Calculus Its Syntax and Semantics,
revised edition 103.
North Holland.
Peter Sestoft (2001):
Demonstrating Lambda Calculus Reduction.
Electr. Notes Theor. Comput. Sci. 45,
pp. 424–432,
doi:10.1016/S1571-0661(04)80973-3.
http://www.itu.dk/people/sestoft/lamreduce/.
Lucas Champollion, Joshua Tauberer & Maribel Romero (2007):
The Penn Lambda Calculator: Pedagogical Software for Natural Language Semantics.
Technical Report.
University of Konstanz, Germany, KOPS.
Available at http://kops.ub.uni-konstanz.de/volltexte/2009/9605/.
http://lambdacalculator.com/.
David Ruiz & Mateu Villaret (2009):
TILC: The Interactive Lambda-Calculus Tracer.
Electron. Notes Theor. Comput. Sci. 248,
pp. 173–183,
doi:10.1016/j.entcs.2009.07.067.
Alexandre Riazanov & Andrei Voronkov (1999):
Vampire.
In: Automated Deduction - CADE-16, 16th International Conference on Automated Deduction, Trento, Italy, July 7-10, 1999, Proceedings,
pp. 292–296,
doi:10.1007/3-540-48660-7_26.
Stephan Schulz (2002):
E - a brainiac theorem prover.
AI Commun. 15(2,3),
pp. 111–126.
Konstantin Korovin (2008):
iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description).
In: A. Armando, P. Baumgartner & G. Dowek: Proceedings of the 4th International Joint Conference on Automated Reasoning, (IJCAR 2008),
Lecture Notes in Computer Science 5195.
Springer,
pp. 292–298,
doi:10.1007/978-3-540-71070-7_24.
Jens Otten (2008):
leanCoP 2.0 and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (System Descriptions).
In: Proceedings of the 4th international joint conference on Automated Reasoning,
IJCAR '08.
Springer-Verlag,
Berlin, Heidelberg,
pp. 283–291,
doi:10.1007/978-3-540-71070-7_23.
Lawrence C. Paulson & Jasmin C. Blanchette (2012):
Three years of experience with Sledgehammer, a Practical Link Between Automatic and Interactive Theorem Provers.
In: Geoff Sutcliffe, Stephan Schulz & Eugenia Ternovska: IWIL 2010. The 8th International Workshop on the Implementation of Logics,
EPiC Series in Computing 2.
EasyChair,
pp. 1–11,
doi:10.29007/36dt.
Available at https://easychair.org/publications/paper/wV.
Geoff 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.
Joe Hurd (2003):
First-order proof tactics in higher-order logic theorem provers.
In: Design and Application of Strategies/Tactics in Higher Order Logics, number NASA/CP-2003-212448 in NASA Technical Reports,
pp. 56–68.
John A. Robinson (1965):
A Machine-Oriented Logic Based on the Resolution Principle.
J. ACM 12(1),
pp. 23–41,
doi:10.1145/321250.321253.
Alberto Martelli & Ugo Montanari (1982):
An Efficient Unification Algorithm.
ACM Trans. Program. Lang. Syst. 4(2),
pp. 258–282,
doi:10.1145/357162.357169.
Robert M. Colomb (1991):
Enhancing unification in PROLOG through clause indexing.
The Journal of Logic Programming 10(1),
pp. 23–44,
doi:10.1016/0743-1066(91)90004-9.
Gerhard Gentzen (1935):
Untersuchungen über das logische Schließen. I.
Mathematische Zeitschrift 39(1),
pp. 176–210,
doi:10.1007/BF01201353.
Max Wisniewski, Alexander Steen & Christoph Benzmüller (2014):
The Leo-III Project.
In: Alexander Bolotov & Manfred Kerber: Joint Automated Reasoning Workshop and Deduktionstreffen,
pp. 38.
Available at http://christoph-benzmueller.de/papers/W53.pdf.
eptcs@eptcs.org