Building Theories in Nuprl
by David A. Basin
Proceedings of Logic at Botik '89
This paper provides an account of how mathematical knowledge is represented, reasoned about, and used computationally in a mechanized constructive theorem proving environment. We accomplish this by presenting a particular theory developed in the Nuprl proof development system: finite set theory culminating in Ramsey's theorem. We believe that this development is interesting as a case study in the relationship between constructive mathematics and computer science. Moreover, the aspects we emphasize--the high-level development of definitions and lemmas, the use of tactics to automate reasoning, and the use of type theory as a programming logic--are not restricted in relevance to this particular theory, and indicate the promise of our approach for other branches of constructive mathematics.
bibTex ref: Bas89