We propose to work on this problem through a subcontract to GrammaTech. They have an SBIR contract from ONR to provide a Formal Methods Environment (FME) for integrating such tools. They are especially concerned with the following problem.
User-Interface inadequacies: existing formal methods are hobbled by weak user-interfaces, and the cost of making better ones often dominates the cost of implementing the core method.
Our proposal directly attacks these problems. We have worked with GrammaTech before to build a standard user interface for Nuprl. The prototype they built for us is the basis for their plans to build one for PVS with SBIR funding. We are proposing that they expand their plans to include an interface to the LPE we are building.
Our previous work with GrammaTech also helped us test our design of an open theorem proving architecture. We wrote an editor interface that will support foreign as well as resident editors.