Building Problem Solving Environments In Constructive Type Theory

We have developed powerful environments within the Nuprl Proof Development System for problem solving in diverse domains. Definitions, proofs, and programs are constructed naturally and at a high-level in these environments, with decision procedures and other tactics providing a degree of automation approaching that found in more specialized theorem provers. Our environments have a wide range of applications that include: Ramsey theory, hardware specification and verification, combinational logic synthesis from proofs, CMOS circuit synthesis from boolean expressions, recursion theory, and partial program development. Several of these applications establish new theorem proving paradigms. We also provide an account of rewriting in type theory and related decision procedures. We have implemented a very general rewrite package for reasoning about arbitrary user defined relations, and we have used this package to construct a number of sophisticated term normalizers, simplifiers, and equality decision procedures. We demonstrate that one of these decision problems deciding if two terms containing otherwise uninterpreted associative-commutative function symbols and commutative variable binding operators are equal, is polynomially equivalent to determining if two graphs are isomorphic