Foundations for the Management of Formal Mathematical Knowledge

by Robert L. Constable
2004-2005

A small international community is gaining experience in managing formal mathematical knowledge, the sort arising from the use of theorem provers. At Cornell we have been involved in this activity for several years, stimulated by our use of three theorem proving systems, Nuprl, MetaPRL, and JProver and by Doug Howe's 1997 work combining results from Nuprl and HOL.

My lecture will highlight three of the discoveries we have made in this subject. One is about sharing content across logics and systems and is an extension of Howe's work by Evan Moran. Another is work by Stuart Allen on logical concepts that support proofs using results from different systems, hybrid proofs. The third are results from Lori Lorigo that help automate the organization of formal material for presentation and search. I will also discuss future directions for our work.

Foundations for the Management of Formal Mathematical Knowledge

by Robert L. Constable 2004-2005

by Robert L. Constable
2004-2005