Notational Definition and Top-Down Refinement for Interactive Proof Development Systems

Other Titles


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 λ-calculus together with a method of representing expressions in a given language L as λ-expressions. The λ-calculus has a very simple abbreviative mechanism that allows a new constant, introduced by means of a δ-equation, to represent a closed expression. A new construct, called a Δ-equation, is introduced. It provides a higher-level means of introducing new notations that is close to the conventional style of definition. A Δ-equation is given meaning by a translation into a simple δ-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.

Journal / Series

Volume & Issue



Date Issued



Cornell University


computer science; technical report


Effective Date

Expiration Date




Union Local


Number of Workers

Committee Chair

Committee Co-Chair

Committee Member

Degree Discipline

Degree Name

Degree Level

Related Version

Related DOI

Related To

Related Part

Based on Related Item

Has Other Format(s)

Part of Related Item

Related To

Related Publication(s)

Link(s) to Related Publication(s)


Link(s) to Reference(s)

Previously Published As

Government Document




Other Identifiers


Rights URI


technical report

Accessibility Feature

Accessibility Hazard

Accessibility Summary

Link(s) to Catalog Record