Proof Automation in Constructive Type Theory
by Christoph Kreitz
The Nuprl proof development system has been used in a number of significant
applications such as the formal design, verification, and optimization of
protocols for the Ensemble Group Communication Toolkit. However, the degree of
automatic support for these formal developments is comparably low, which makes
dealing with the immense amount of formal details unneccessarily tedious,
particularly when it comes to dealing with complex but intellectually trivial
problems. While the concept of tactics provides the opportunity to program the
application of logical inferences, the system contains still only a few basic
techniques for finding proofs automatically.
The open architecture of Nuprl 5 enables us to connect external proof engines to the Nuprl system and thus to extend its reasoning power by integrating well-understood techniques from automated theorem proving. This has recently been demonstrated by connecting Nuprl with JProver, a complete theorem prover for first-order intuitionistic logic.
In the seminar I will briefly discuss a variety of proof mechanisms that will provide significant improvements to Nuprl's automated reasoning capabilities if they can be successfully integrated. Besides possible enhancements of JProver towards dealing with type theory these include
-- inductive theorem proving based on rippling techniques
-- proof planning
-- decision procedures for certain application domains
-- model checking
The purpose of the seminar is to sketch possible research directions that could be followed in the near future. The above list is not complete and suggestions are more than welcome.