Planning and Patching Proof - Artificial Intelligence and Symbolic Computation - page 35

[Benzmuller et al , 1997] Benzmuller, C., Cheikhrouhou, L., Fehrer, D., Fiedler, A.,
Huang, X., Kerber, M., Kohlhase, K., Meier, A, Melis, E., Schaarschmidt, W.,
Siekmann, J. and Sorge, V. (1997). Ω mega: Towards a mathematical assistant. In
McCune, W., (ed.), 14th International Conference on Automated Deduction , pages
252-255. Springer-Verlag.
[Boulton et al , 1998] Boulton, R., Slind, K., Bundy, A. and Gordon, M. (Septem-
ber/October 1998). An interface between CLAM and HOL. In Grundy, J. and
Newey, M., (eds.), Proceedings of the 11th International Conference on Theorem
Proving in Higher Order Logics (TPHOLs'98) , volume 1479 of Lecture Notes in
Computer Science , pages 87-104, Canberra, Australia. Springer.
[Bundy & Green, 1996] Bundy, Alan and Green, Ian. (December 1996). An experimen-
tal comparison of rippling and exhaustive rewriting. Research paper 836, Dept. of
Artificial Intelligence, University of Edinburgh.
[Bundy & Lombart, 1995] Bundy, A. and Lombart, V. (1995). Relational rippling: a
general approach. In Mellish, C., (ed.), Proceedings of IJCAI-95 , pages 175-181.
IJCAI.
[Bundy, 1988] Bundy, A. (1988). The use of explicit plans to guide inductive proofs. In
Lusk, R. and Overbeek, R., (eds.), 9th International Conference on Automated De-
duction , pages 111-120. Springer-Verlag. Longer version available from Edinburgh
as DAI Research Paper No. 349.
[Bundy, 1991] Bundy, Alan. (1991). A science of reasoning. In Lassez, J.-L. and
Plotkin, G., (eds.), Computational Logic: Essays in Honor of Alan Robinson , pages
178-198. MIT Press. Also available from Edinburgh as DAI Research Paper 445.
[Bundy, 2001] Bundy, Alan. (2001). The automation of proof by mathematical induc-
tion. In Robinson, A. and Voronkov, A., (eds.), Handbook of Automated Reasoning,
Volume 1 . Elsevier.
[Bundy, 2002] Bundy, A. (2002). A Critique of Proof Planning , pages 160-177.
Springer.
[Bundy et al , 1989] Bundy, A., van Harmelen, F., Hesketh, J., Smaill, A. and Stevens,
A. (1989). A rational reconstruction and extension of recursion analysis. In Srid-
haran, N. S., (ed.), Proceedings of the Eleventh International Joint Conference
on Artificial Intelligence , pages 359-365. Morgan Kaufmann. Also available from
Edinburgh as DAI Research Paper 419.
[Bundy et al , 1990] Bundy, A., van Harmelen, F., Horn, C. and Smaill, A. (1990). The
Oyster-Clam system. In Stickel, M. E., (ed.), 10th International Conference on
Automated Deduction , pages 647-648. Springer-Verlag. Lecture Notes in Artificial
Intelligence No. 449. Also available from Edinburgh as DAI Research Paper 507.
[Bundy et al , 1993] Bundy, A., Stevens, A., van Harmelen, F., Ireland, A. and Smaill,
A. (1993). Rippling: A heuristic for guiding inductive proofs. Artificial Intelligence ,
62:185-253. Also available from Edinburgh as DAI Research Paper No. 567.
[Bundy et al , 2005] Bundy, A., Basin, D., Hutter, D. and Ireland, A. (2005). Rippling:
Meta-level Guidance for Mathematical Reasoning . Cambridge University Press.
[Dennis et al , 2000] Dennis, L., Bundy, A. and Green, I. (2000). Making a productive
use of failure to generate witness for coinduction from divergent proof attempts.
Annals of Mathematics and Artificial Intelligence , 29:99-138. Also available as
paper No. RR0004 in the Informatics Report Series.
[Desimone, 1989] Desimone, R. V. (1989). Explanation-Based Learning of Proof Plans.
In Kodratoff, Y. and Hutchinson, A., (eds.), Machine and Human Learning . Kogan
Page. Also available as DAI Research Paper 304. Previous version in proceedings
of EWSL-86.