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.
Relational Data Across Mathematical Libraries / Condoluci A.; Kohlhase M.; Muller D.; Rabe F.; Sacerdoti Coen C.; Wenzel M.. - STAMPA. - 11617:(2019), pp. 61-76. (Intervento presentato al convegno 12th International Conference on Intelligent Computer Mathematics, CICM 2019 tenutosi a cze nel 2019) [10.1007/978-3-030-23250-4_5].
Relational Data Across Mathematical Libraries
Condoluci A.
;Sacerdoti Coen C.
;
2019
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.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
