Skip to main content
U.S. flag

An official website of the United States government

Official websites use .gov
A .gov website belongs to an official government organization in the United States.

Secure .gov websites use HTTPS
A lock ( ) or https:// means you’ve safely connected to the .gov website. Share sensitive information only on official, secure websites.

Comparative Verification & Validation of Digital Mathematical Libraries and Computer Algebra Systems

Published

Author(s)

Howard Cohl, Abdou Youssef, Andre Greiner Petter, Moritz Schubotz, Bela Gipp, Akiko Aizawa, Avi Trost, Rajen Dey

Abstract

Digital Mathematical Libraries assemble the knowledge of years of mathematical research. Numerous disciplines (e.g., physics, engineering, pure and applied mathematics) rely heavily on compendia gathered findings. Likewise, modern research relies more and more on computational solutions, which are often calculated and verified by computer algebra systems. Hence, the correctness, accuracy, and reliability of both mathematical libraries and computer algebra systems is a crucial attribute for modern research. In this paper, we present a comparative approach for the verification and validation of digital mathematical libraries and computer algebra systems. We use our previously developed conversion tool (referred to as LaCASt) to translate formulae from the NIST Digital Library of Mathematical Functions to the computer algebra systems Maple and Mathematica. Our main contributions in this paper are: (1) significant enhancement of the performance of LaCASt by the inclusion of translations for sums, products, limits, integrals, Lagrange's notation for derivatives (prime notation) and Wronskian relations; (2) automated verification and computation for mathematical formulae from a digital mathematical library; and (3) the provision of an open API endpoint for the translator.
Proceedings Title
Tools and Algorithms for the Construction and Analysis of Systems
Volume
13243
Conference Dates
June 19-23, 2020
Conference Location
Munich, DE
Conference Title
28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2–7, 2022, Proceedings, Part I

Keywords

LaCASt, Translations, LaTeX, Semantic LaTeX, Computer Algebra Systems, Digital Mathematical Library

Citation

Cohl, H. , Youssef, A. , Greiner Petter, A. , Schubotz, M. , Gipp, B. , Aizawa, A. , Trost, A. and Dey, R. (2022), Comparative Verification & Validation of Digital Mathematical Libraries and Computer Algebra Systems, Tools and Algorithms for the Construction and Analysis of Systems, Munich, DE, [online], https://doi.org/10.1007/978-3-030-99524-9 (Accessed December 5, 2024)

Issues

If you have any questions about this publication or are having problems accessing it, please contact reflib@nist.gov.

Created March 30, 2022, Updated March 27, 2024