Notational Definition and Top-Down Refinement for Interactive Proof Development Systems
| dc.contributor.author | Griffin, Timothy G. | en_US |
| dc.date.accessioned | 2007-04-23T17:34:25Z | |
| dc.date.available | 2007-04-23T17:34:25Z | |
| dc.date.issued | 1988-08 | en_US |
| dc.description.abstract | This thesis is concerned with issues related to the design and implementation of systems that support interactive proof development. The goal is to provide logic-independent frameworks that can be used in the design and implementation of component parts for such systems. In particular, this thesis will focus on two frameworks: a language-independent account of notational definition and a logic-independent account of a structure-oriented approach to the interactive construction of goal-directed proofs. These particular concerns were inspired and motivated by the Nuprl proof development system. However, the results presented in this thesis are meant to be applicable to a wide class of logics. The formal account of notational definition begins with the presentation of a simply typed $\lambda$-calculus together with a method of representing expressions in a given language $\cal L$ as $\lambda$-expressions. The $\lambda$-calculus has a very simple abbreviative mechanism that allows a new constant, introduced by means of a $\delta$-equation, to represent a closed expression. A new construct, called a $\Delta$-equation, is introduced. It provides a higher-level means of introducing new notations that is close to the conventional style of definition. A $\Delta$-equation is given meaning by a translation into a simple $\delta$-equation. The implementation of mechanisms that support notational definitions in interactive proof development systems as well as applications to Nuprl are discussed. The second part of the thesis presents a logic-independent framework for top-down proof development called abstract refinement. Rather than presenting, as is done for Nuprl, refinement and refinement rules as primitive notions that are extended by grafting on tactics, tactics are instead viewed as the basic notion from which refinement trees arise as tree-structured representations of the iterated composition of tactics. This is accomplished with the definition of a new construct called a tactic tree that extends the LCF tactics framework in a natural way. Several examples of proof development using tactic trees are presented. One example demonstrates that the refinement rules and the extraction mechanism of Nuprl can be modeled in this framework. | en_US |
| dc.format.extent | 9342370 bytes | |
| dc.format.extent | 1924157 bytes | |
| dc.format.mimetype | application/pdf | |
| dc.format.mimetype | application/postscript | |
| dc.identifier.citation | http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR88-937 | en_US |
| dc.identifier.uri | https://hdl.handle.net/1813/6777 | |
| dc.language.iso | en_US | en_US |
| dc.publisher | Cornell University | en_US |
| dc.subject | computer science | en_US |
| dc.subject | technical report | en_US |
| dc.title | Notational Definition and Top-Down Refinement for Interactive Proof Development Systems | en_US |
| dc.type | technical report | en_US |