Integrating Automated and Interactive Theorem Proving
-----------------------------------------------------

Wolfgang Ahrendt, Bernhard Beckert, Reiner Hähnle, Wolfram Menzel,
Wolfgang Reif, Gerhard Schellhorn, Peter H. Schmitt 

In this chapter we present a project to integrate interactive and
automated theorem proving. Its aim is to combine the advantages of the
two paradigms. We focus on one particular application domain, which is
deduction for the purpose of software verification.  software
verification Some of the reported facts may not be valid in other
domains.  We report on the integration concepts and on the
experimental results with a prototype implementation.