nach oben

Erschienen in:

2019 | OriginalPaper | Buchkapitel

A Plugin to Export Coq Libraries to XML

verfasst von : Claudio Sacerdoti Coen

Erschienen in: Intelligent Computer Mathematics

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

We introduce a plugin for the interactive prover Coq to export its libraries to a machine readable XML format. The information exported is the one checked by Coq’s kernel after the input is elaborated, augmented with additional data coming from the elaboration itself.

The plugin has been applied to the 49 Coq libraries that have an opam package and that currently compile with the latest version of Coq (8.9.0), generating a large dataset of 1,235,934 compressed XML files organized in 18,780 directories that require 17 GB on disk.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel Inspection and Selection of Representations

Nächstes Kapitel Forms of Plagiarism in Digital Mathematical Libraries

[ABD03]

Asperti, A., Buchberger, B., Davenport, J.H. (eds.): MKM 2003. LNCS, vol. 2594. Springer, Heidelberg (2003). https://doi.org/10.1007/3-540-36469-2CrossRefMATH

[AGS+04]

Asperti, A., Guidi, F., Coen, C.S., Tassi, E., Zacchiroli, S.: A content based mathematical search engine: whelp. In: Filliâtre, J.-C., Paulin-Mohring, C., Werner, B. (eds.) TYPES 2004. LNCS, vol. 3839, pp. 17–32. Springer, Heidelberg (2006). https://doi.org/10.1007/11617990_2CrossRef

[ARST11]

Asperti, A., Ricciotti, W., Sacerdoti Coen, C., Tassi, E.: The Matita interactive theorem prover. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS, vol. 6803, pp. 64–69. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22438-6_7CrossRef

[ASTZ06]

Asperti, A., Coen, C.S., Tassi, E., Zacchiroli, S.: Crafting a proof assistant. In: Altenkirch, T., McBride, C. (eds.) TYPES 2006. LNCS, vol. 4502, pp. 18–32. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-74464-1_2CrossRef

[AW02]

Asperti, A., Wegner, B.: MOWGLI – an approach to machine-understandable representation of the mathematical information in digital documents. In: Bai, F., Wegner, B. (eds.) ICM 2002. LNCS, vol. 2730, pp. 14–23. Springer, Heidelberg (2003). https://doi.org/10.1007/978-3-540-45155-6_2CrossRefMATH

[CK18]

Czajka, L., Kaliszyk, C.: Hammer for Coq: automation for dependent type theory. J. Autom. Reasoning 61(1–4), 423–453 (2018). https://doi.org/10.1007/s10817-018-9458-4MathSciNetCrossRefMATH

[CKM+19]

Condoluci, A., Kohlhase, M., Müller, D., Rabe, F., Sacerdoti Coen, C., Wenzel, M.: Relational data across mathematical libraries. In: Kaliszyk, C., et al. (eds.) CICM 2019. LNAI, vol. 11617, pp. 61–76 (2019)

[DT]

Dowek, G., Thiré, F.: Logipedia: a multi-system encyclopedia of formal proofs. http://www.lsv.fr/~dowek/Publi/logipedia.pdf

[GA16]

Arias, E.J.G.: SerAPI: Machine-friendly, data-centric serialization for Coq, October 2016. Working paper or preprint. https://hal-mines-paristech.archives-ouvertes.fr/hal-01384408

[GS03]

Guidi, F., Schena, I.: A query language for a metadata framework about mathematical resources. In: Asperti, et al. [ABD03], pp. 105–118. https://doi.org/10.1007/3-540-36469-2_9

[ISA+16]

Irving, G., Szegedy, C., Alemi, A.A., Eén, N., Chollet, F., Urban, J.: DeepMath - deep sequence models for premise selection. In: Advances in Neural Information Processing Systems 29: Annual Conference on Neural Information Processing Systems, Barcelona, Spain, 5–10 December 2016, pp. 2235–2243 (2016). http://papers.nips.cc/paper/6280-deepmath-deep-sequence-models-for-premise-selection

[KS06]

Kohlhase, M., Sucan, I.: A search engine for mathematical formulae. In: Calmet, J., Ida, T., Wang, D. (eds.) AISC 2006. LNCS, vol. 4120, pp. 241–253. Springer, Heidelberg (2006). https://doi.org/10.1007/11856290_21CrossRef

[KWP99]

Kammüller, F., Wenzel, M., Paulson, L.C.: Locales a sectioning concept for Isabelle. In: Bertot, Y., Dowek, G., Théry, L., Hirschowitz, A., Paulin, C. (eds.) TPHOLs 1999. LNCS, vol. 1690, pp. 149–165. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-48256-3_11CrossRef

[MGK+17]

Müller, D., Gauthier, T., Kaliszyk, C., Kohlhase, M., Rabe, F.: Classification of alignments between concepts of formal mathematical systems. In: Geuvers, H., England, M., Hasan, O., Rabe, F., Teschke, O. (eds.) CICM 2017. LNCS, vol. 10383, pp. 83–98. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-62075-6_7CrossRef

[MRS19]

Müller, D., Rabe, F., Sacerdoti Coen, C.: The Coq library as a theory graph. In: Kaliszyk, C., et al. (eds.) CICM 2019. LNAI, vol. 11617, pp. 171–186 (2019)

[RK13]

Rabe, F., Kohlhase, M.: A scalable module system. Inf. Comput. 230, 1–54 (2013). https://doi.org/10.1016/j.ic.2013.06.001MathSciNetCrossRefMATH

[Sac01]

Sacerdoti Coen, C.: Project IST-2001-33562 MoWGLI. Technical report D2.a Exportation Module, Information Society Technologies (IST) Programme (2001). http://mowgli.cs.unibo.it/misc/deliverables/transformation/D2a_exportation_module/report.pdf

[Sac03]

Sacerdoti Coen, C.: From proof-assistants to distributed libraries of mathematics: tips and pitfalls. In: Asperti, et al. [ABD03], pp. 30–44. https://doi.org/10.1007/3-540-36469-2_3

[Sac04]

Sacerdoti Coen, C.: Mathematical knowledge management and interactive theorem proving. Ph.D. thesis, Technical report UBLCS 2004-5. University of Bologna (2004). http://www.cs.unibo.it/~sacerdot/tesidott/thesis.ps.gz

[Sac10]

Sacerdoti Coen, C.: Declarative representation of proof terms. J. Autom. Reasoning 44(1–2), 25–52 (2010). https://doi.org/10.1007/s10817-009-9136-7MathSciNetCrossRefMATH

[Tea19]

The Coq Development Team: The Coq Proof Assistant, version 8.9.0, January 2019. https://doi.org/10.5281/zenodo.2554024

Titel: A Plugin to Export Coq Libraries to XML
verfasst von: Claudio Sacerdoti Coen
Verlag: Springer International Publishing
Buch: Intelligent Computer Mathematics
Print ISBN: 978-3-030-23249-8

Electronic ISBN: 978-3-030-23250-4

Copyright-Jahr: 2019
DOI: https://doi.org/10.1007/978-3-030-23250-4_17

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"