The study that you are about to participate in is part of a research project which is attempting to build a system to translate a formal proof which is generated by a computer system (in particular, Nuprl) into a natural language proof, specifically, a proof in English. As part of this project, it is important to look at how people perform this translation. The data from this study will be used to locate ways in which people agree on how a proof should be translated, to find where style is a factor and what the style differences are, and to build up a corpus of translated proofs as a training and testing resource for the system.

As a participant, you will be asked to read a Nuprl proof and then write a translation of this proof in English. You will also be asked to answer a small number of biographical questions and some questions about your experience in translating the proofs. You are not required to answer every question, but the more information you can supply, the better. There are 15 total proofs available to be translated, but you need only translate as many of them as you like. These proofs are all fairly short, so hopefully they can be translated quickly and many people will be able to get through all of them. You do not need to do this study all in one sitting; feel free to give me your results for a subset of the proofs at a time.

To proceed:

  • If you are unfamiliar with the Nuprl Proof Development system, proceed to the Introduction to Nuprl page. If you have ever used Nuprl before or know what a tactic is already, you can skip this page.
  • If you need a description of how to read Nuprl proofs on the web, proceed to the How to read Nuprl Proofs page.
  • A list of all of the tactics used in the following proofs along with their definitions is given on the Tactic Definitions page. If you are not a Nuprl user, you may want to skim this page.
  • To proceed to the first page of questions and begin the study, go to the Starting the Study page.
  • When you have finished translating as many proofs as you are going to complete, please visit the Exiting the Study page and answer the questions there. If you are stopping but intend to return and translate another proof, you can wait and visit that page later, but please remember to return and do so at some time.
Links back to all of these pages will be available on all subsequent pages of the study through the navigation bar. The introductory pages are there to help people who are not familiar with the system gain enough familiarity to be able to complete the study; they are not meant to be a full introduction to the system or to reflect the system as a whole.

If you have any questions about this study, any problems with this web site, or any comments, please contact me (Amanda Holland-Minkley) at the e-mail address or phone number given at the bottom of the page or stop by my office.

Intro to the Study | Introduction to Nuprl | How to Read Nuprl Proofs | Tactic Definitions | Starting the Study | Exiting the Study

In case of questions contact:

Amanda Holland-Minkley
Phone: 255-1181
Office: Upson 5141