Lori Lorigo, Department
of Computer Science, Cornell University. lolorigo@cs.cornell.edu. May 2002.
Position Statement: There is an open field of possibilities once one combines Computer Science and Mathematics to solve technical, theoretical and educational challenges. My interests lie in making the current digital mathematics more accessible and usable, both to those who build and contribute mathematical knowledge and also to those who study and develop systems. |
| COLLABORATIVE THEOREM PROVING |
| Goal: To allow collaboration in real-time on building digital proofs. |
| The Nuprl
5 Automated Thereom Prover consists of 3 independent processes that
communicate: an editor, library,
and proof engine.
Leveraging on this design, I wrote a collaborative tutorial for the system where multiple participants each ran their own local editors but worked jointly in the same library, on the same proof. The participants observed and responded to each others' changes on a particular proof, and completed a proof through team-work. |
| INTEGRATING PROOF ASSISTANTS |
| Goal: To share proofs, definitions, etc between different proof systems and to call external inference engines while building your proof. |
| I worked on the integration of Nuprl 5 with 2 other provers:
MetaPRL
system, and Jprover, a standalone first-order-logic
prover
Metaprl - In this case we imported data into the FDL, including meta-data about how to display formulas, and called the Metaprl refiner (using INET socket communication) on Metaprl proofs. Jprover - Here, we called Jprover as a heuristic to build Nuprl proofs. The difference in logics was taken into account, and assured not to cause inaccuracy in the final proof. Jprover has since then been linked to the Coq system as well. |
| DATA FORMATS for ACCESSIBILITY |
| Goal: To provide data formats for communicating mathematical content between systems and users. |
| I have worked on 2 formats below.
MathBus - This format used for communicating with MetaPRL and Jprover. XML - Using the EXPAT Parser, we have imported XML generated by a modeling tool, GME 2000, as part of an effort to use formal methods in embedded systems development. See the PCES project for detail. Also, I have written an XML Schema (work in progress) for terms in the FDL. I plan to use XSLT to transform the XML to other formats to make communicating with the FDL even more accessible. See the HELM Project for related work. |
Lori Lorigo, Department
of Computer Science, Cornell University. lolorigo@cs.cornell.edu. May 2002.