| Using the Rippling Heuristic in Set Membership Proofs | 2 | 0.34 | 1997 |
| Middle-Out Reasoning for Synthesis and Induction | 20 | 6.57 | 1996 |
| Implementing Z in Isabelle | 8 | 1.20 | 1995 |
| Mollusc: A General Proof-Development Shell for Sequent-Based Logics | 2 | 0.59 | 1994 |
| Middle-out reasoning for logic program synthesis | 17 | 1.15 | 1993 |
| A framework for program development based on schematic proof | 6 | 0.91 | 1993 |
| Logic Program Synthesis via Proof Planning | 100 | 4.08 | 1992 |
| Automatic abduction of qualitative models | 26 | 3.54 | 1992 |
| Synthesis and Transfomation of Logic Programs from Constructive, Inductive Proof | 2 | 0.41 | 1991 |
