Anzeige
Erschienen in:
2003 | OriginalPaper | Buchkapitel
From Proof-Assistants to Distributed Libraries of Mathematics: Tips and Pitfalls
verfasst von : Claudio Sacerdoti Coen
Erschienen in: Mathematical Knowledge Management
Verlag: Springer Berlin Heidelberg
Enthalten in: Professional Book Archive
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
When we try to extract to an open format formal mathematical knowledge from libraries of already existing proof-assistants, we must face several problems and make important design decisions. This paper is based on our experiences on the exportation to XML of the theories developed in Coq and NuPRL: we try to collect a set of (hopefully useful) suggestions to pave the way to other teams willing to attempt the same operation.