KnowledgeBase » SEMINAR » ID = 577

Proof Automation in Constructive Type Theory

by Christoph Kreitz
2001-2002

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.