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.

Agency
National Science Foundation (NSF)
Institute
Division of Computer and Communication Foundations (CCF)
Application #
0204193
Program Officer
Robert B Grafton
Project Start
Project End
Budget Start
2002-07-01
Budget End
2006-06-30
Support Year
Fiscal Year
2002
Total Cost
$285,000
Indirect Cost
Name
Cornell University
Department
Type
DUNS #
City
Ithaca
State
NY
Country
United States
Zip Code
14850