Adolfo Villaorita

Content areas: abstraction, automated reasoning, interactive theorem proving The goal of the work described in this paper is the development of a sys-tem, called ABSFOL, which allows the user to state declaratively abstractions and to use them according to the desired control strategy. ABSFOL has been successfully tested on many examples. So far we have failed to nd an in-teresting abstraction whose implementation requires a major programming eort. Alan Bundy provided much of the inspiration for the solution of the Goedel ex-ample. The authors ' names are purely alphabetical. 1