Share  Bookmark

 Download from



[1] A. Bundy. A science of reasoning. In J.L. Lassez and G. Plotkin, editors, Computational Logic: Essays in Honor of Alan Robinson, pages 178{198. MIT Press, 1991.
[2] A. Bundy. The automation of proof by mathematical induction. In A. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning, volume 1. Elsevier, 2001.
[3] A. Bundy, F. van Harmelan, C. Horn, and A. Smaill. The oysterclam system. In M. E. Stickel, editor, 10th International Conference on Automated Deduction, volume 449 of Lecture Notes in Arti cial Intelligence, pages 647{648. Springer, 1990.
[4] H. Comon and R. Nieuwenhuis. Induction = Iaxiomatization + rstorder consistency. Information and Computation, 159(1{2), 2000.
[5] L. A. Dennis and J. Brotherston. clam v4: User/Developer's Manual. Mathematical Reasoning Group, Division of Informatics, University of Edinburgh, 2002.
[6] L. Dixon and J. D. Fleuriot. IsaPlanner: A prototype proof planner in Isabelle. In F. Baader, editor, 19th International Conference on Automated Deduction, volume 2741 of Lecture Notes in Computer Science, pages 279{283. Springer, 2003.
[7] M. Franova and Y. Kodrato . Predicate synthesis from formal speci cation. In B. Neumann, editor, 10th European Conference on Arti cial Intelligence, pages 97{91. John Wiley and Sons, 1992.
[8] M. J. C. Gordon and T. F. Melham. Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, 1993.
[9] J. Gow. The Dynamic Creation of Induction Rules Using Proof Planning. PhD thesis, Centre for Intelligent Systems and their Applications, School of Informatics, University of Edinburgh, 2004.
[10] A. Ireland and A. Bundy. Productive use of failure in inductive proof. Journal of Automated Reasoning, 16(1{2):79{111, 1996.