Relational Data Across Mathematical Libraries

Condoluci A, Kohlhase M, Müller D, Rabe F, Sacerdoti Coen C, Wenzel M (2019)

Publication Type: Conference contribution

Publication year: 2019

Journal

Lecture Notes in Computer Science Springer Verlag

Publisher: Springer Verlag

Book Volume: 11617 LNAI

Pages Range: 61-76

Conference Proceedings Title: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

Event location: Prague CZ

ISBN: 9783030232498

DOI: 10.1007/978-3-030-23250-4_5

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.

Authors with CRIS profile

Michael Kohlhase Professur für Wissensrepräsentation und -verarbeitung Dennis Müller Professur für Wissensrepräsentation und -verarbeitung Florian Rabe Professur für Wissensrepräsentation und -verarbeitung

Involved external institutions

University of Bologna / Università di Bologna IT Italy (IT)

How to cite

APA:

Condoluci, A., Kohlhase, M., Müller, D., Rabe, F., Sacerdoti Coen, C., & Wenzel, M. (2019). Relational Data Across Mathematical Libraries. In Claudio Sacerdoti Coen, Andrea Kohlhase, Edwin Brady, Cezary Kaliszyk (Eds.), Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (pp. 61-76). Prague, CZ: Springer Verlag.

MLA:

Condoluci, Andrea, et al. "Relational Data Across Mathematical Libraries." Proceedings of the 12th International Conference on Intelligent Computer Mathematics, CICM 2019, Prague Ed. Claudio Sacerdoti Coen, Andrea Kohlhase, Edwin Brady, Cezary Kaliszyk, Springer Verlag, 2019. 61-76.

BibTeX: Download