Abstract
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. © Springer-Verlag Berlin Heidelberg 2003.
Cite
CITATION STYLE
Coen, C. S. (2003). From proof-assistants to distributed libraries of mathematics: Tips and pitfalls. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2594, 30–44. https://doi.org/10.1007/3-540-36469-2_3
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
