|
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.
|
|
