|
Ph.D. Candidate |
403 Rhodes Hall phone: (607) 255-8957 |
Most recently, I have been the instructor for CS/ENGRI 172: Computing, Information, and Intelligence during both the Fall 2003 and Summer 2003 semesters. In the past I have also been an instructor for CS 114: Unix Tools and a teaching assistant for CS 212: Java Practicum, CS 100: Introduction to Programming, and CS 410: Data Structures.
In my graduate work, I have investigated the presentation of formal mathematics through natural language, primarily focusing on the organizational and planning issues involved in structuring a mathematical text. I have implemented a prototype system for converting computer-generated proofs into textbook-style English texts via an empirically-motivated intermediate plan representation. My focus has been on the discourse planning component, with the goal of connecting highly structured formal proofs with the text structure required for effective communication via a mathematically- and language-coherent intermediate representation. Doing so required drawing on work from natural language generation, knowledge representation, automated reasoning and formal mathematics. To ground the work, I performed a series of studies of how people knowledgeable in formal mathematics prefer to represent and manipulate this mathematics in a textual form. The resulting system is able to produce proof texts that are competitive with human-produced proofs in their effectiveness at communicating proof content.
During this work, I performed three studies to examine how people translate formal proofs, specifically those created by Nuprl theorem proving system, to English proofs. The first study was administered via the web and is still available on-line. An initial version of the system was constructed based on our findings from this study. Texts generated automatically by this system (as described in the AAAI99 paper below) are available here. The second study was then administered to determine the extensibility of the generation techniques extracted from the first study, specifically to proofs within the domain of number theory which use the technique of proof by induction. These results are described in my INLG '02 paper. In the final study, analyzed in my thesis, we perform a comparison of the output of the system to proof texts created by human experts.
See below for publications and presentations on my work.My advisor on this project is Robert Constable and I am a member of the Nuprl research group. The libraries of formal mathematics that we generate text from are available on the Nuprl group page, as well as information on other projects going on within the group.
My other professional activities include having served as President and Chair of the Diversity Committee for the Engineering Graduate Student Association, coordinating the Czarships positions in the computer science department, and co-founding the Cornell At What Cost? organization.
My current hobbies include reading, photography, quilting, knitting, and other crafts. I am an occassional volunteer proofreader with Project Gutenberg's Distributed Proofreaders project. My personal homepage is hosted elsewhere; visit it for links to my weblog, book reviews, and other content.
Amanda M. Holland-Minkley. Planning Proof Content for Communicating Induction. Second International Natural Language Generation Conference (pdf)
Amanda M. Holland-Minkley, Regina Barzilay, and Robert Constable. Verbalization of High-Level Formal Proofs. Sixteenth National Conference on Artificial Intelligence (pdf)
Susannah Hobbs, Amanda Holland-Minkley, and Lynette Millett. A Case for Building Inclusive Research Communities as an Integral Part of Science and Engineering Graduate Education. 1999 IEEE International Symposium on Technology and Society (pdf)
"Nuprl Library Annotation", Prl Seminar, Cornell University, April 5, 2004 (informal outline)
"A Linguistic View of Constructive Type Theory", Prl Seminar, Cornell University, February 2, 2004
"Structure in Computing and Language", Dedication of the Charles F. & Barbara D. Weiss Directorship of the Information Science Program in Computing and Information Science, Cornell University, October 2001
"Generating Text from High-Level Formal Proofs", Second Annual Graduate Conference of the Northeastern Cognitive Science Society (NECCS), University of Pennsylvania, April 30-May 1, 1999
"Verbalization of High-Level Formal Proofs", Prl Seminar, Cornell University, February 1, 1999
Informal Discussion of the Motivation of the Project of Generating Text from Nuprl Proofs, Fall 1998
Informal Discussion of the Study to Create a Corpus of Human-Generated Texts, Fall 1998