In this paper we describe a framework that allows users of Formal Development Environments (FDEs) to prove veri-fication conditions using stand-alone theorem provers. Veri fication conditions from a given FDE are translated into an intermediate representation, then in turn translated into a form that is readable by the target theorem prover.

In this paper we describe a systematic approach to the development of translators from the intermediate representation to a target theorem prover representation. The approach involves the development of a generic translator, which is instantiated for a particular target theorem prover by defining a variety of translation rules. In this paper we describe the different kinds of translation rules and illustrate their use with an example.