Skip to content
Snippets Groups Projects
Select Git revision
  • master default
  • zolekode-master-patch-26857
  • zolekode-master-patch-78201
  • zolekode-master-patch-54259
  • zolekode-master-patch-38209
5 results
Blame Permalink
logosphere.md 1.37 KiB 
layout: project

title: "Logosphere: Formal Digital Libraries"
shorttitle: Logosphere
teaser: Integrating Theorem Prover Libraries through Meta-logical Frameworks

active: false
start_date: '2003'
end_date: '2006'
publink: auto

people:
    - mkohlhase
    - inormann

collaborators: 
    - Carsten Schürmann, Yale University
    - Frank Pfenning, CMU
    - Natarajan Shankar, SRI International
    - Sam Owre, SRI International

funding: NSF
program: ITR
grantid: CCR-ITR-0325808

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