Email Gateway (Aug 18 2022 at 10:54): Email Gateway (Aug 18 2022 at 10:54):From: Lutz Schroeder <Lutz.Schroeder@dfki.de>
Googling the keywords "Isabelle" and "Computer Algebra" leads to a 1995
paper on an interface between Isabelle and Maple. Does this interface
still exist, respectively work with the present versions of Isabelle and
Maple? Is there any more recent work on connecting Isabelle to computer
algebra systems, or more generally to any kind of mathematics tools?
Thanks,
Lutz
Email Gateway (Aug 18 2022 at 10:55):From: Amine Chaieb <chaieb@in.tum.de>
Lutz Schroeder wrote:
Is there any more recent work on connecting Isabelle to computer
algebra systems, or more generally to any kind of mathematics tools?
Maximilian Schlund and I have an experimental communication tool between
Isabelle and some CAS - Axiom and Singular so far.
Amine.
Email Gateway (Aug 18 2022 at 10:55):From: Clemens Ballarin <ballarin@in.tum.de>
That particular interface only worked with Isabelle 1993. More
recent linkups (including Amine's) are based on an oracle mechanism
[1, Section 6.10] that was added to Isabelle's kernel only later. I
have later created an interface [2] to Bronstein's computer algebra
library Sumit [3]. I can probably find the sources to this interface
if required.
Clemens
[1] Lawrence C. Paulson, The Isabelle Reference Manual, 2005.
[2] Clemens Ballarin and Lawrence C. Paulson. A Pragmatic Approach to
Extending Provers by Computer Algebra - with Applications to Coding
Theory. Fundamenta Informaticae, 39(1, 2), 1-20, 1999.
[3] Manuel Bronstein. Sumit — a strongly-typed embeddable computer
algebra
library. In Calmet and Limongelli: DISCO ’96, Karlsruhe, Germany,
LNCS 1128, pages 22–33, 1996.
Last updated: May 03 2024 at 08:18 UTC