References

1

Aubin, R. Mechanizing Structural Induction. Ph.D. thesis, University of Edinburgh, 1976.

2

Basin, D. and Walsh, T. Difference matching. In Kapur, D. editor, 11th Conference on Automated Deduction, 295-309. Springer Verlag, 1992. Lecture Notes in Computer Science No. 607. Also available from Edinburgh as DAI Research Paper 556.

3

Basin, D. and Walsh, T. Difference unification. In Proceedings of the 13th IJCAI. International Joint Conference on Artificial Intelligence, 1993. Also available as Technical Report MPI-I-92-247, Max-Planck-Institute für Informatik.

4

Basin, D. and Walsh, T. Termination orderings for rippling. In Bundy, A. editor, 12th Conference on Automated Deduction, 466-483. Springer Verlag, 1994. Lecture Notes in Artificial Intelligence No. 814.

5

Bouhoula, A., Kounalis, E., and Rusinowitch, M. Spike: A theorem-prover. In Proceedings of LPAR'92, Lecture Notes in Artificial Intelligence 624. Springer-Verlag, 1992.

6

Bouhoula, A. and Rusinowitch, M. Implicit induction in conditional theories. Journal of Automated Reasoning, 14(2), 189-235, 1995.

7

Bouhoula, A. and Rusinowitch, M. Spike user manual. INRIA Lorraine and CRIN, 615 rue du Jardin Botanique, Villers-lès-Nancy, France, 1995. Available from ftp://ftp.loria.fr/pub/loria/protheo/softwares/Spike/.

8

Boyer, R. and Moore, J. A Computational Logic. Academic Press, 1979. ACM monograph series.

9

Bundy, A., Stevens, A., van Harmelen, F., Ireland, A., and Smaill, A. Rippling: A heuristic for guiding inductive proofs. Artificial Intelligence, 62, 185-253, 1993. Also available from Edinburgh as DAI Research Paper No. 567.

10

Bundy, A., van Harmelen, F., Horn, C., and Smaill, A. The Oyster-Clam system. In Stickel, M. editor, 10th International Conference on Automated Deduction, 647-648. Springer-Verlag, 1990. Lecture Notes in Artificial Intelligence No. 449.

11

Dershowitz, N. and Pinchover, E. Inductive Synthesis of Equational Programs. In Proceedings of the 8th National Conference on AI, 234-239, 1990. American Association for Artificial Intelligence.

12

Hermann, M. Crossed term rewriting systems CRIN report 89-R-003, Centre de Recherche en Informatique de Nancy, 1989.

13

Ireland, A. The Use of Planning Critics in Mechanizing Inductive Proof. In Proceedings of LPAR'92, Lecture Notes in Artificial Intelligence 624. Springer-Verlag, 1992. Also available as Research Report 592, Dept of AI, Edinburgh University.

14

Ireland, A. and Bundy, A. Using failure to guide inductive proof. Technical report, Dept. of Artificial Intelligence, University of Edinburgh, 1992. Available from Edinburgh as DAI Research Paper 613.

15

Kirchner, H. Schematization of infinite sets of rewrite rules. Application to the divergence of completion processes, In Proceedings of RTA'87, 180-191, 1987.

16

Protzen, M. Disproving conjectures. In Kapur, D. editor, 11th Conference on Automated Deduction, 340-354. Springer Verlag, 1992. Lecture Notes in Computer Science No. 607.

17

Thomas, M. and Jantke, K. Inductive Inference for Solving Divergence in Knuth-Bendix Completion. In Proceedings of International Workshop AII'89, 288-303, 1989.

18

Thomas, M. and Watson, P. Solving divergence in Knuth-Bendix completion by enriching signatures. Theoretical Computer Science, 112, 145-185, 1993.

19

Walsh, T. A divergence critic. In Bundy, A. editor, 12th Conference on Automated Deduction, 14-25. Springer Verlag, 1994. Lecture Notes in Artificial Intelligence No. 814.

20

Walsh, T., Nunes, A., and Bundy, A. The use of proof plans to sum series. In Kapur, D. editor, 11th Conference on Automated Deduction, 325-339. Springer Verlag, 1992. Lecture Notes in Computer Science No. 607. Also available from Edinburgh as DAI Research Paper 563.

21

Yoshida, T., Bundy, A., Green, I., Walsh, T., and Basin, D. Coloured rippling: the extension of a theorem proving heuristic. In Cohn, A. editor, European Conference on Artificial Intelligence (ECAI-94), 1994.