Extracting Theory Graphs from Aldor Libraries
Rabe F, Watt SM (2023)
Publication Type: Conference contribution
Publication year: 2023
Journal
Publisher: Springer Science and Business Media Deutschland GmbH
Book Volume: 14101 LNAI
Pages Range: 315-320
Conference Proceedings Title: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Event location: Cambridge, GBR
ISBN: 9783031427527
DOI: 10.1007/978-3-031-42753-4_24
Abstract
Aldor is a programming language for computer algebra that allows natural expression of algebraic objects while also allowing compilation to efficient code. Its language primitives, however, do not correspond exactly to those of modern proof assistants nor to those of data formats used in mathematical knowledge management. We discuss these difficulties and export the Aldor library as a diagram in the category of theories and theory morphisms, using a simplified model of the Aldor language that retains its essential expressivity. This allows us to capture a rich set of expert-designed interfaces for use in mathematical knowledge management settings.
Authors with CRIS profile
Involved external institutions
Canada (CA)How to cite
APA:
Rabe, F., & Watt, S.M. (2023). Extracting Theory Graphs from Aldor Libraries. In Catherine Dubois, Manfred Kerber (Eds.), Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (pp. 315-320). Cambridge, GBR: Springer Science and Business Media Deutschland GmbH.
MLA:
Rabe, Florian, and Stephen M. Watt. "Extracting Theory Graphs from Aldor Libraries." Proceedings of the Proceedings of the 16th Conference on Intelligent Computer Mathematics, CICM 2023, Cambridge, GBR Ed. Catherine Dubois, Manfred Kerber, Springer Science and Business Media Deutschland GmbH, 2023. 315-320.
BibTeX: Download