Show simple item record

dc.contributor.authorBasin, David A.en_US
dc.description.abstractWe 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.en_US
dc.format.extent11567051 bytes
dc.format.extent2410869 bytes
dc.publisherCornell Universityen_US
dc.subjectcomputer scienceen_US
dc.subjecttechnical reporten_US
dc.titleBuilding Problem Solving Environments In Constructive Type Theoryen_US
dc.typetechnical reporten_US

Files in this item


This item appears in the following Collection(s)

Show simple item record