Proof Automation in Constructive Type Theory

sponsored by the National Science Foundation  

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 goal of this project is to enhance the automatic reasoning capabilities of tactical proof systems while preserving the interactive nature on which their strength is based. It will integrate a variety of automated proof tools into a tactical proof system, develop strategies for increasing the cooperation of different formal reasoning tools, and provide new forms of practical assistance for users of tactical proof systems.
The new capabilities will make it easier for novice users to solve nontrivial problems with tactical proof systems. Expert users will be able to prove difficult theorems with significantly less effort in a shorter amount of time, which allows them to focus on the intellectually challenging aspects of their tasks. Educators will find support for teaching systematic mathematical methods through experimentation with a formal system. Students will be able to learn how to find proofs by inspecting the formal proofs generated by the automatic proof tools. The project will also support the cooperation between research groups by helping them share tools and insights, which in turn will enable them to meet the rapidly growing demands for formal tools that can assure the safety and reliability of software.



Latest News

November '02 PVS linked to Nuprl
We have implemented a link between Nuprl and PVS that enables users to access PVS from the Nuprl theorem proving environment and to import PVS content into Nuprl.
March '02 JProver integrated into Coq
JProver, our theorem prover for first-order intuitionistic logic, originally developed for guiding the development of constructive proofs in Nuprl and MetaPRL has been integrated into the Coq proof assistant.

Back to main page