Retrieval (not yet implemented.)

Stay tuned.

Submission. (Actively under construction.)

News

Talk at the Math Wiki Workshop 2007, Edinburgh on the state of the Logosphere system.

The Economist ran an intersting article March 31, 2005 about Proofs and Beauty. Enjoy.

Carsten Schürmann, Mark-Oliver Stehr. An Executable Formalization of the HOL/Nurpl Connection in Twelf. 11th International Conference on Logic for Programming Artificial Intelligence and Reasoning March 14-18th, 2005, Montevideo, Uruguay. The complete Twelf development source code can be found here: hol-nuprl.tgz.

Logosphere Workshop, June 9 2004 is going to be held at Carnegie Mellon University. Plese find local arrangement information here and information about the programme here.

A mailing list for the Logosphere developers has been created. To sign up, please visit http://www.mailman.cs.yale.edu/mailman/listinfo/logosphere-developer.

The kick-off meeting for the Logosphere project and the Infer! project took place at SRI International 10/26-10/27/03. Carsten's slides and Franks's slides are available online.

Project Summary

Mathematical knowledge is at the core of science and engineering. The quantity of mathematical knowledge is growing faster than our ability to formalize and organize it. The proposed research focuses on developing a Formal Digital Library called Logosphere, a common and open infrastructure for managing and sharing mathematical knowledge and formal proof. Central to this work is the design of a logical framework as a representation language for logical formalisms, individual theories, and proofs, with an interface to theorem proving systems such as PVS or HOL, that have been effective in industrial practice. Logoshpere emphasizes interoperability between theorem proving systems, and the exchange and reusability of mathematical facts across different systems. The Logosphere infrastructure is designed to be scalable with respect to the size of the knowledge base as well as the diversity of formalisms.

The Logosphere project encourages industry and academia to contribute, maintain, and use basic mathematical knowledge related to formal methods in hardware, software, and engineering. The Logosphere project contributes to the cyberinfrastructure by formalizing and organizing practical mathematical knowledge in a readily usable form. Application areas for Logosphere include education, computer-aided design, mathematical modelling, formal verification, and scientific research.

People

Yale University

Carnegie Mellon University

SRI International

Acknowledgements