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.
|
