| Rippling: A heuristic for guiding inductive proofs A Bundy, A Stevens, F Van Harmelen, A Ireland, A Smaill Artificial intelligence 62 (2), 185-253, 1993 | 394 | 1993 |
| Productive use of failure in inductive proof A Ireland, A Bundy Automated Mathematical Induction, 79-111, 1996 | 262 | 1996 |
| Rippling: meta-level guidance for mathematical reasoning A Bundy Cambridge University Press, 2005 | 217 | 2005 |
| The use of planning critics in mechanizing inductive proofs A Ireland International Conference on Logic for Programming Artificial Intelligence …, 1992 | 127 | 1992 |
| Extensions to the rippling-out tactic for guiding inductive proofs A Bundy, F Van Harmelen, A Smaill, A Ireland 10th International Conference on Automated Deduction: Kaiserslautern, FRG …, 1990 | 99 | 1990 |
| Invariant discovery via failed proof attempts J Stark, A Ireland International Workshop on Logic Programming Synthesis and Transformation …, 1998 | 64 | 1998 |
| On the automatic discovery of loop invariants A Ireland, J Stark NASA Conference Publication, 137-152, 1997 | 47 | 1997 |
| On the use of the constructive omega-rule within automated deduction S Baker, A Ireland, A Smaill Logic Programming and Automated Reasoning: International Conference LPAR'92 …, 1992 | 40 | 1992 |
| Extensions to a generalization critic for inductive proof A Ireland, A Bundy International Conference on Automated Deduction, 47-61, 1996 | 33 | 1996 |
| Proof plans for the correction of false conjectures R Monroy, A Bundy, A Ireland Logic Programming and Automated Reasoning: 5th International Conference …, 1994 | 33 | 1994 |
| Automatic verification of functions with accumulating parameters A Ireland, A Bundy Journal of Functional Programming 9 (2), 225-245, 1999 | 30 | 1999 |
| Proof planning for strategy development A Ireland, J Stark Annals of Mathematics and Artificial Intelligence 29, 65-97, 2000 | 27 | 2000 |
| Towards a skeleton based parallelising compiler for SML G Michaelson, A Ireland, P King Proceedings of 9th International Workshop on Implementation of Functional …, 1997 | 26 | 1997 |
| Reasoned modelling critics: turning failed proofs into modelling guidance A Ireland, G Grov, MT Llano, M Butler Science of Computer Programming 78 (3), 293-309, 2013 | 25 | 2013 |
| Interactive proof critics A Ireland, M Jackson, G Reid Formal Aspects of Computing 11, 302-325, 1999 | 25 | 1999 |
| An integrated approach to high integrity software verification A Ireland, BJ Ellis, A Cook, R Chapman, J Barnes Journal of Automated Reasoning 36, 379-410, 2006 | 23 | 2006 |
| Rippling: A heuristic for guiding inductive proofs. Research Paper 567, Dept. of Artificial Intelligence, Edinburgh, 1991 A Bundy, A Stevens, F van Harmelen, A Ireland, A Smaill Artificial Intelligence, 0 | 19 | |
| Low-level programming in Hume: an exploration of the HW-Hume level K Hammond, G Grov, G Michaelson, A Ireland Symposium on Implementation and Application of Functional Languages, 91-107, 2006 | 18 | 2006 |
| Increasing the versatility of heuristic based theorem provers A Manning, A Ireland, A Bundy Logic Programming and Automated Reasoning: 4th International Conference …, 1993 | 18 | 1993 |
| Formal verification of concurrent scheduling strategies using TLA G Grov, G Michaelson, A Ireland 2007 International Conference on Parallel and Distributed Systems, 1-6, 2007 | 16 | 2007 |
