David Baelde, Kaustuv Chaudhuri, Andrew Gacek, Dale Miller, Gopalan Nadathur, Alwen Tiu & Yuting Wang (2014):
Abella: A System for Reasoning about Relational Specifications.
Journal of Formalized Reasoning 7(2),
doi:10.6092/issn.1972-5787/4650.
Available at http://jfr.unibo.it/article/download/4650/4137.
David Baelde & Dale Miller (2007):
Least and greatest fixed points in linear logic.
In: N. Dershowitz & A. Voronkov: International Conference on Logic for Programming and Automated Reasoning (LPAR),
LNCS 4790,
pp. 92–106.
Available at http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/lpar07final.pdf.
(2015):
The Bedwyr system.
Available at http://slimmer.gforge.inria.fr/bedwyr/.
Robert S. Boyer & J. Strother Moore (1979):
A Computational Logic.
Academic Press.
A. Bundy, A. Stevens, F. van Harmelen, A. Ireland & A. Smaill (1993):
Rippling: A Heuristic for Guiding Inductive Proofs.
Artificial Intelligence 62(2),
pp. 185–253,
doi:10.1016/0004-3702(93)90079-Q.
Alan Bundy (1987):
The use of explicit plans to guide inductive proofs.
In: Conf. on Automated Deduction (CADE 9),
pp. 111–120.
Zakaria Chihani, Dale Miller & Fabien Renaud (2013):
Foundational proof certificates in first-order logic.
In: Maria Paola Bonacina: CADE 24: Conference on Automated Deduction 2013,
LNAI 7898,
pp. 162–177,
doi:10.1007/978-3-642-38574-2_11.
Dale Miller & Gopalan Nadathur (2012):
Programming with Higher-Order Logic.
Cambridge University Press,
doi:10.1017/CBO9781139021326.
Frank Pfenning & Carsten Schürmann (1999):
System Description: Twelf — A Meta-Logical Framework for Deductive Systems.
In: H. Ganzinger: 16th Conf. on Automated Deduction (CADE),
LNAI 1632.
Springer,
Trento,
pp. 202–206,
doi:10.1007/3-540-48660-7_14.
Carsten Schürmann & Frank Pfenning (2003):
A Coverage Checking Algorithm for LF.
In: Theorem Proving in Higher Order Logics: 16th International Conference, TPHOLs 2003,
LNCS 2758.
Springer,
pp. 120–135,
doi:10.1007/10930755_8.