1. David Baelde (2012): Least and greatest fixed points in linear logic. ACM Trans. on Computational Logic 13(1), doi:10.1145/2071368.2071370. Available at
  2. 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
  3. 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
  4. David Baelde, Dale Miller & Zachary Snow (2010): Focused Inductive Theorem Proving. In: J. Giesl & R. Hähnle: Fifth International Joint Conference on Automated Reasoning, LNCS 6173, pp. 278–292, doi:10.1007/978-3-642-14203-1_24. Available at
  5. (2015): The Bedwyr system. Available at
  6. Robert S. Boyer & J. Strother Moore (1979): A Computational Logic. Academic Press.
  7. 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.
  8. Alan Bundy (1987): The use of explicit plans to guide inductive proofs. In: Conf. on Automated Deduction (CADE 9), pp. 111–120.
  9. 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.
  10. Dale Miller & Gopalan Nadathur (2012): Programming with Higher-Order Logic. Cambridge University Press, doi:10.1017/CBO9781139021326.
  11. 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.
  12. 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.
  13. Sean Wilson, Jacques Fleuriot & Alan Smaill (2010): Inductive Proof Automation for Coq. In: Second Coq Workshop. Available at

Comments and questions to:
For website issues: