Abstract
In this paper we analyse the modifications on logical operations – as proof checking, type inference, reduction and convertibility – that are required for the identification of a proof assistant environment with a distributed mathematical library, focusing on proof assistants based on the Curry–Howard isomorphism.
This identification is aimed at the integration of Mathematical Knowledge Management tools with interactive theorem provers: once the distinction between the proof assistant environment and a mathematical library is blurred, it is possible to exploit Mathematical Knowledge Management rendering, indexing and searching services inside an interactive theorem prover, a first step towards effective loosely-coupled collaborative mathematical environments.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Asperti, A., Guidi, F., Padovani, L., Sacerdoti Coen, C., Schena, I.: Mathematical Knowledge Management in HELM. Annals of Mathematics and Artificial Intelligence 38(1), 27–46 (2003)
Buchberger, B.: Computer-Supported Mathematical Theory Exploration: Schemes, Failing Proof Analysis, and Metaprogramming. Technical report, RISC, Austria (September 2004)
Colton, S.: Automated Theory Formation in Pure Mathematics Series: Distinguished Dissertations, vol. XVI, p. 380 (2002), ISBN: 1-85233-609-9
Coquand, T.: An Analysis of Girard’s Paradox. In: Proc. Symposium on Logic in Computer Science, Cambridge, Massachusetts, pp. 227–236. IEEE Computer Society Press, Los Alamitos (1986)
Coquand, T., Huet, G.: The Calculus of Constructions. Technical report 530, INRIA (May 1986)
Courant, J.: Explicit universes for the calculus of constructions. In: Carreño, V.A., Muñoz, C.A., Tahar, S. (eds.) TPHOLs 2002. LNCS, vol. 2410, pp. 115–130. Springer, Heidelberg (2002)
Luo, Z.: An Extended Calculus of Constructions. PhD thesis, University of Edinburgh (1990)
Harper, R., Pollack, R.: Type checking with universes. Theoretical Computer Science 89, 107–136 (1991)
Sacerdoti Coen, C.: Mathematical Knowledge Management and Interactive Theorem Proving. PhD thesis, University of Bologna (2004)
Sacerdoti Coen, C.: From Proof-Assistants to Distributed Libraries of Mathematics: Tips and Pitfalls. In: Asperti, A., Buchberger, B., Davenport, J.H. (eds.) MKM 2003. LNCS, vol. 2594, pp. 30–44. Springer, Heidelberg (2003)
Werner, B.: Une Theorie des Constructions Inductives. PhD thesis, Université Paris VII (1994)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Coen, C.S. (2004). Mathematical Libraries as Proof Assistant Environments. In: Asperti, A., Bancerek, G., Trybulec, A. (eds) Mathematical Knowledge Management. MKM 2004. Lecture Notes in Computer Science, vol 3119. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-27818-4_24
Download citation
DOI: https://doi.org/10.1007/978-3-540-27818-4_24
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-23029-8
Online ISBN: 978-3-540-27818-4
eBook Packages: Springer Book Archive