Interactively guided proof assistants have been successfully used in the formal design, verification, and optimization of software and hardware systems. Because of their expressive logics, they are more generally applicable than fully automated tools, yet at a much lesser degree of automation. The main goal of this project is to combine the expressive power of proof assistants with the automatic reasoning capabilities of proof search procedures, proof planners, decision procedures, model checkers, etc. and to use the enhanced system in the formal design of reliable software. In particular we aim at providing proof automation for the Nuprl proof development system, a tactical proof environment that has been used in numerous applications. It offers a proven basis for solving mathematical problems and for designing reliable hardware and software systems. The newest release of Nuprl features one of the most exible architectures for interacting with external problem solving devices. Our experience with connecting Nuprl with JProver, a theorem prover for first-order intuitionistic logic, has shown that Nuprl supports interoperability between formalsystems in a way that makes our goal feasible.