Title:	Building Problem Solving Environments In Constructive Type Theory
Authors:	Basin, David A.
Keywords:	computer science technical report
Issue Date:	Dec-1989
Publisher:	Cornell University
Citation:	http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR89-1063
Abstract:	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.
URI:	http://hdl.handle.net/1813/6863
Appears in Collections:	Computer Science Technical Reports

Files in This Item: File Description Size Format 89-1063.pdf 11.3 MB Adobe PDF View/Open 89-1063.ps 2.35 MB Postscript View/Open

Items in eCommons are protected by copyright, with all rights reserved, unless otherwise indicated.