Few people use formal methods, and of those that do, even fewer use proof. This is in part due to the poor tool support available specifically for carrying out proofs and the difficulty of doing it by hand. Our work attempts to meet the challenge of incorporating interactive features in automated theorem provers whilst preserving the advantages of automation. Many people are not able to use theorem provers to their full strength. The aim of our research is to make semi-automated theorem proving a real possibility for a wide range of people - from those primarily interested in formal specification, for whom proof is a chore, to developers of automated theorem proving systems themselves.