Bibliography

1

Alan Bundy.
The use of explicit plans to guide inductive proofs.
In R. Lusk and R. Overbeek, editors, 9th Conference on Automated Deduction, pages 111-120. Springer-Verlag, 1988.
Longer version available from Edinburgh as DAI Research Paper No. 349.

2

A. Ireland.
The Use of Planning Critics in Mechanizing Inductive Proofs.
In A. Voronkov, editor, International Conference on Logic Programming and Automated Reasoning - LPAR 92, St. Petersburg, Lecture Notes in Artificial Intelligence No. 624, pages 178-189. Springer-Verlag, 1992.
Also available from Edinburgh as DAI Research Paper 592.

3

A. Ireland and A. Bundy.
Extensions to a Generalization Critic for Inductive Proof.
In M. A. McRobbie and J. K. Slaney, editors, 13th Conference on Automated Deduction, pages 47-61. Springer-Verlag, 1996.
Springer Lecture Notes in Artificial Intelligence No. 1104. Also available from Edinburgh as DAI Research Paper 786.

4

A. Ireland and A. Bundy.
Productive Use of Failure in Inductive Proof.
Journal of Automated Reasoning, 16(1-2):79-111, 1996.
Also available as DAI Research Paper No 716, Dept. of Artificial Intelligence, Edinburgh.

5

A. Ireland and A. Bundy.
Automatic Verification of Functions with Accumulating Parameters.
Research Memo RM/97/11, Dept. of Computing and Electrical Engineering, Heriot-Watt University, 1997.
Submitted to a special issue of the Journal of Functional Programming on Theorem Proving and Functional Programming. Also to appear as an Edinburgh DAI Research Paper.

6

A. Ireland, M. Jackson, and G. Reid.
Interactive proof critics.
1998.
Submitted to a Special Issue of the Journal of Formal Aspects of Computing on User Interfaces for Theorem Provers. Available from Dept. of Computing and Electrical Engineering, Heriot-Watt University, Research Memo RM/98/15.

7

A. Ireland and J. Stark.
On the Automatic Discovery of Loop Invariants.
Research Memo RM/97/1, Dept. of Computing and Electrical Engineering, Heriot-Watt University, 1997.

8

M. Jackson.
HCI Techniques for Theorem Proving.
Master's thesis, Department of Computing & Electrical Engineering, Edinburgh, 1996.

9

J. Stark and A. Ireland.
Invariant discovery via failed proof attempts.
In Proceedings of LOPSTR 98, University of Manchester Technical Report UMCS-98-6-1. Full version to be published LNCS Springer-Verlag., 1998.
Also available from Dept. of Computing and Electrical Engineering, Heriot-Watt University, Research Memo RM/98/2.