nach oben

Erschienen in:

2019 | OriginalPaper | Buchkapitel

Relational Data Across Mathematical Libraries

verfasst von : Andrea Condoluci, Michael Kohlhase, Dennis Müller, Florian Rabe, Claudio Sacerdoti Coen, Makarius Wenzel

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

Formal libraries are treasure troves of detailed mathematical knowledge, but this treasure is usually locked into system- and logic-specific representations that can only be understood by the respective theorem prover system. In this paper we present an ontology for using relational information on mathematical knowledge and a corresponding data set generated from the Isabelle and Coq libraries. We show the utility of the generated data by setting a relational query engine that provides easy access to certain library information that was previously hard or impossible to determine.

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 A Tale of Two Set Theories

Nächstes Kapitel Variadic Equational Matching

https://swmath.org/software/NUMBER.

http://msc2010.org/resources/MSC/2010/CLASS.

https://www.acm.org/publications/class-2012.

We have reconsidered the name of this class many times: all suggested names can be misunderstood. The current name stems from the intuition that axioms and theorems are the most important named truth-establishing declarations, and statement is a common way to unify them. Arguably more systematic would be proof: anything that establishes truth is formalized as an operator that constructs a proof.

https://github.com/sacerdot/coq.

https://gl.mathhub.info/Coqxml.

Versions: Isabelle/9c60fcfdf495, AFP/d50417d0ae64, MMT/e6fa4b852bf9.

https://github.com/openlink/virtuoso-opensource.

[ADL12]

Aspinall, D., Denney, E., Lüth, C.: A semantic basis for proof queries and transformations. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR 2013. LNCS, vol. 8312, pp. 53–70. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-45221-5_4CrossRefMATH

[AS04]

Asperti, A., Selmi, M.: Efficient retrieval of mathematical statements. In: Asperti, A., Bancerek, G., Trybulec, A. (eds.) MKM 2004. LNCS, vol. 3119, pp. 17–31. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-27818-4_2CrossRefMATH

[Asp+06]

Asperti, A., Guidi, F., Sacerdoti Coen, C., 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

[GC16]

Guidi, F., Coen, C.S.: A survey on retrieval of mathematical knowledge. Math. Comput. Sci. 10(4), 409–427 (2016). https://doi.org/10.1007/s11786-016-0274-0MathSciNetCrossRefMATH

[Lan11]

Lange, C.: Enabling Collaboration on Semiformal Mathematical Knowledge by Semantic Web Integration. Studies on the Semantic Web 11. AKA Verlag and IOS Press, Heidelberg and Amsterdam (2011)

[MPPS09]

Motik, B., Parsia, B., Patel-Schneider, P.F.: OWL 2 Web Ontology Language: XML Serialization. W3C Recommendation. World Wide Web Consortium (W3C), 27 October 2009. http://www.w3.org/TR/2009/REC-owl2-xml-serialization-20091027/

[Mül+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 (LNAI), vol. 10383, pp. 83–98. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-62075-6_7CrossRef

[Pau90]

Paulson, L.C.: Isabelle: the next 700 theorem provers. In: Odifreddi, P. (ed.) Logic and Computer Science, pp. 361–386. Academic Press, Cambridge (1990)

[Qed]

The QED Project (1996). http://www-unix.mcs.anl.gov/qed/

[Rab12]

Rabe, F.: A query language for formal mathematical libraries. In: Jeuring, J., et al. (eds.) CICM 2012. LNCS (LNAI), vol. 7362, pp. 143–158. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-31374-5_10. arXiv:1204.4685 [cs.LO]CrossRef

[RK13]

Rabe, F., Kohlhase, M.: A scalable module system. Inf. Comput. 230, 1–54 (2013). http://kwarc.info/frabe/Research/mmt.pdfMathSciNetCrossRef

[ULO]

ULO Documentation. https://ulo.mathhub.info/. Accessed 03 Nov 2019

[W3c]

SPARQL 1.1 Overview. W3C Recommendation. World Wide Web Consortium (W3C), 23 March 2013. https://www.w3.org/TR/sparql11-overview/

[Wen18a]

Wenzel, M.: Isabelle/jEdit as IDE for domain-specific formal languages and informal text documents. In: Masci, P., Monahan, R., Prevosto, V. (eds.) 4th Workshop on Formal Integrated Development Environment, F-IDE 2018 (2018). https://sketis.net/wp-content/uploads/2018/05/isabelle-jedit-fide2018.pdfCrossRef

[Wen18b]

Wenzel, M.: Isabelle/MMT: export of Isabelle theories and import as OMDoc content. Blog entry (2018). https://sketis.net/2018/isabelle-mmt-export-of-isabelle-theories-and-import-as-omdoc-content

[Wen18c]

Wenzel, M.: Isabelle/PIDE after 10 years of development. Presented at the UITP Workshop: User Interfaces for Theorem Provers (2018). https://sketis.net/wp-content/uploads/2018/08/isabelle-pide-uitp2018.pdf

[RDF04]

RDF Core Working Group of the W3C. Resource Description Framework Specification (2004). http://www.w3.org/RDF/

[Sac19]

Coen, C.S.: A plugin to export Coq libraries to XML. In: 12th International Conference on Intelligent Computer Mathematics (CICM 19). LNAI (2019)

Titel: Relational Data Across Mathematical Libraries
verfasst von: Andrea Condoluci
Michael Kohlhase
Dennis Müller
Florian Rabe
Claudio Sacerdoti Coen
Makarius Wenzel
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_5

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"