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