{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T01:14:08Z","timestamp":1743124448954,"version":"3.40.3"},"publisher-location":"Cham","reference-count":36,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030995232"},{"type":"electronic","value":"9783030995249"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,3,30]],"date-time":"2022-03-30T00:00:00Z","timestamp":1648598400000},"content-version":"vor","delay-in-days":88,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>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 applications rely more and more on computational solutions, which are often calculated and verified by computer algebra systems. Hence, the correctness, accuracy, and reliability of both digital mathematical libraries and computer algebra systems is a crucial attribute for modern research. In this paper, we present a novel approach to verify a digital mathematical library and two computer algebra systems with one another by converting mathematical expressions from one system to the other. We use our previously developed conversion tool (referred to as \n\n\"Image missing\"\n\n) to translate formulae from the NIST Digital Library of Mathematical Functions to the computer algebra systems  and . The contributions of our presented work are as follows:\u00a0(1) we present the most comprehensive verification of computer algebra systems and digital mathematical libraries with one another; (2) we significantly enhance the performance of the underlying translator in terms of coverage and accuracy; and (3) we provide open access to translations for  and  of the formulae in the NIST Digital Library of Mathematical Functions.<\/jats:p>","DOI":"10.1007\/978-3-030-99524-9_5","type":"book-chapter","created":{"date-parts":[[2022,3,29]],"date-time":"2022-03-29T06:14:55Z","timestamp":1648534495000},"page":"87-105","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Comparative\u00a0Verification of the Digital Library of Mathematical Functions and Computer Algebra Systems"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5828-5497","authenticated-orcid":false,"given":"Andr\u00e9","family":"Greiner-Petter","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9398-455X","authenticated-orcid":false,"given":"Howard S.","family":"Cohl","sequence":"additional","affiliation":[]},{"given":"Abdou","family":"Youssef","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7141-4997","authenticated-orcid":false,"given":"Moritz","family":"Schubotz","sequence":"additional","affiliation":[]},{"given":"Avi","family":"Trost","sequence":"additional","affiliation":[]},{"given":"Rajen","family":"Dey","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6544-5076","authenticated-orcid":false,"given":"Akiko","family":"Aizawa","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6522-3019","authenticated-orcid":false,"given":"Bela","family":"Gipp","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,3,30]]},"reference":[{"key":"5_CR1","doi-asserted-by":"publisher","unstructured":"Aguirregabiria, J.M., Hern\u00e1ndez, A.M., Rivas, M.: Are we careful enough when using computer algebra? Computers in Physics 8(1), 56\u201361 (1994). https:\/\/doi.org\/10.1063\/1.4823260","DOI":"10.1063\/1.4823260"},{"key":"5_CR2","doi-asserted-by":"publisher","unstructured":"Barnett, M., Chang, B.Y.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: A modular reusable verifier for object-oriented programs. In: Formal Methods for Components and Objects, pp. 364\u2013387. Springer Berlin Heidelberg (2006). https:\/\/doi.org\/10.1007\/11804192_17","DOI":"10.1007\/11804192_17"},{"key":"5_CR3","doi-asserted-by":"crossref","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development - Coq\u2019Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. An EATCS Series, Springer Berlin Heidelberg (2004)","DOI":"10.1007\/978-3-662-07964-5"},{"key":"5_CR4","unstructured":"Bobot, F., Filli\u00e2tre, J.C., March\u00e9, C., Paskevich, A.: Why3: Shepherd your herd of provers. Boogie 2011: First International Workshop on Intermediate Verification Languages pp. 53\u201364 (5 2011), https:\/\/hal.inria.fr\/hal-00790310\/document"},{"key":"5_CR5","doi-asserted-by":"publisher","unstructured":"Boulm\u00e9, S., Hardin, T., Hirschkoff, D., M\u00e9nissier-Morain, V., Rioboo, R.: On the way to certify computer algebra systems. Electronic Notes in Theoretical Computer Science 23(3), 370\u2013385 (1999). https:\/\/doi.org\/10.1016\/S1571-0661(05)80609-7, cALCULEMUS 99, Systems for Integrated Computation and Deduction (associated to FLoC\u201999, the 1999 Federated Logic Conference)","DOI":"10.1016\/S1571-0661(05)80609-7"},{"key":"5_CR6","doi-asserted-by":"publisher","unstructured":"Carette, J., Kucera, M.: Partial evaluation of Maple. Science of Computer Programming 76(6), 469\u2013491 (6 2011). https:\/\/doi.org\/10.1016\/j.scico.2010.12.001","DOI":"10.1016\/j.scico.2010.12.001"},{"key":"5_CR7","doi-asserted-by":"publisher","unstructured":"Cohl, H.S., Greiner-Petter, A., Schubotz, M.: Automated symbolic and numerical testing of DLMF formulae using computer algebra systems. In: Intelligent Computer Mathematics CICM. vol. 11006, pp. 39\u201352. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-96812-4_4","DOI":"10.1007\/978-3-319-96812-4_4"},{"key":"5_CR8","doi-asserted-by":"publisher","unstructured":"Cohl, H.S., Schubotz, M., Youssef, A., Greiner-Petter, A., Gerhard, J., Saunders, B.V., McClain, M.A., Bang, J., Chen, K.: Semantic preserving bijective mappings of mathematical formulae between document preparation systems and computer algebra systems. In: Intelligent Computer Mathematics CICM. pp. 115\u2013131. Springer (2017). https:\/\/doi.org\/10.1007\/978-3-319-62075-6_9","DOI":"10.1007\/978-3-319-62075-6_9"},{"key":"5_CR9","doi-asserted-by":"publisher","unstructured":"Corless, R.M., Jeffrey, D.J., Watt, S.M., Davenport, J.H.: \u201cAccording to Abramowitz and Stegun\u201d or arccoth needn\u2019t be uncouth. SIGSAM Bulletin 34(2), 58\u201365 (2000). https:\/\/doi.org\/10.1145\/362001.362023","DOI":"10.1145\/362001.362023"},{"key":"5_CR10","unstructured":"DLMF: NIST Digital Library of Mathematical Functions. https:\/\/dlmf.nist.gov\/, Release 1.1.4 of 2022\u201301-15, F. W. J. Olver, A. B. Olde Daalhuis, D. W. Lozier, B. I. Schneider, R. F. Boisvert, C. W. Clark, B. R. Miller, B. V. Saunders, H. S. Cohl, and M. A. McClain, eds."},{"key":"5_CR11","doi-asserted-by":"crossref","unstructured":"Dur\u00e1n, A.J., P\u00e9rez, M., Varona, J.L.: The misfortunes of a trio of mathematicians using computer algebra systems. Can we trust in them? Notices of the AMS 61(10), 1249\u20131252 (2014)","DOI":"10.1090\/noti1173"},{"key":"5_CR12","doi-asserted-by":"publisher","unstructured":"Elphick, D., Leuschel, M., Cox, S.: Partial evaluation of MATLAB. In: Gen. Prog. and Component Eng., pp. 344\u2013363. Springer (2003). https:\/\/doi.org\/10.1007\/978-3-540-39815-8_21","DOI":"10.1007\/978-3-540-39815-8_21"},{"key":"5_CR13","doi-asserted-by":"publisher","unstructured":"Greiner-Petter, A., Schubotz, M., Aizawa, A., Gipp, B.: Making presentation math computable: Proposing a context sensitive approach for translating LaTeX to computer algebra systems. In: International Congress of Mathematical Software (ICMS). Lecture Notes in Computer Science, vol. 12097, pp. 335\u2013341. Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-52200-1_33","DOI":"10.1007\/978-3-030-52200-1_33"},{"key":"5_CR14","doi-asserted-by":"publisher","unstructured":"Greiner-Petter, A., Schubotz, M., Cohl, H.S., Gipp, B.: Semantic preserving bijective mappings for expressions involving special functions between computer algebra systems and document preparation systems. Aslib Journal of Information Management 71(3), 415\u2013439 (2019). https:\/\/doi.org\/10.1108\/AJIM-08-2018-0185","DOI":"10.1108\/AJIM-08-2018-0185"},{"key":"5_CR15","doi-asserted-by":"publisher","unstructured":"Greiner-Petter, A., Schubotz, M., M\u00fcller, F., Breitinger, C., Cohl, H.S., Aizawa, A., Gipp, B.: Discovering mathematical objects of interest - A study of mathematical notations. In: WWW. pp. 1445\u20131456. ACM \/ IW3C2 (2020). https:\/\/doi.org\/10.1145\/3366423.3380218","DOI":"10.1145\/3366423.3380218"},{"key":"5_CR16","doi-asserted-by":"publisher","unstructured":"Harrison, J.: HOL Light: A tutorial introduction. In: Srivas, M., Camilleri, A. (eds.) Formal Methods in Computer-Aided Design (FMCAD). Lecture Notes in Computer Science, vol.\u00a01166, pp. 265\u2013269. Springer Berlin Heidelberg. https:\/\/doi.org\/10.1007\/BFb0031814","DOI":"10.1007\/BFb0031814"},{"key":"5_CR17","doi-asserted-by":"publisher","unstructured":"Harrison, J.R., Th\u00e9ry, L.: A skeptic\u2019s approach to combining HOL and Maple 21(3), 279\u2013294. https:\/\/doi.org\/10.1023\/A:1006023127567","DOI":"10.1023\/A:1006023127567"},{"key":"5_CR18","doi-asserted-by":"publisher","unstructured":"Heras, J., Pascual, V., Rubio, J.: Using open mathematical documents to interface computer algebra and proof assistant systems. In: Intelligent Computer Mathematics MKM at CICM. Lecture Notes in Computer Science, vol. 5625, pp. 467\u2013473. Springer (2009). https:\/\/doi.org\/10.1007\/978-3-642-02614-0_37","DOI":"10.1007\/978-3-642-02614-0_37"},{"key":"5_CR19","unstructured":"Hickman, T., Laursen, C.P., Foster, S.: Certifying differential equation solutions from computer algebra systems in Isabelle\/HOL http:\/\/arxiv.org\/abs\/2102.02679"},{"key":"5_CR20","doi-asserted-by":"publisher","unstructured":"Kaliszyk, C., Wiedijk, F.: Certified computer algebra on top of an interactive theorem prover. In: Towards Mechanized Math. Assist., pp. 94\u2013105. Springer (2007). https:\/\/doi.org\/10.1007\/978-3-540-73086-6_8","DOI":"10.1007\/978-3-540-73086-6_8"},{"key":"5_CR21","unstructured":"Khan, M.T.: Formal Specification and Verification of Computer Algebra Software. phdthesis, Johannes Kepler University Linz (Apr 2014)"},{"key":"5_CR22","doi-asserted-by":"publisher","unstructured":"Kristianto, G.Y., Topi\u0107, G., Aizawa, A.: Utilizing dependency relationships between math expressions in math IR. Information Retrieval Journal 20(2), 132\u2013167 (3 2017). https:\/\/doi.org\/10.1007\/s10791-017-9296-8","DOI":"10.1007\/s10791-017-9296-8"},{"key":"5_CR23","doi-asserted-by":"publisher","unstructured":"Lamb\u00e1n, L., Rubio, J., Mart\u00edn-Mateos, F.J., Ruiz-Reina, J.L.: Verifying the bridge between simplicial topology and algebra: the Eilenberg-Zilber algorithm. Logic Journal of IGPL 22(1), 39\u201365 (8 2013). https:\/\/doi.org\/10.1093\/jigpal\/jzt034","DOI":"10.1093\/jigpal\/jzt034"},{"key":"5_CR24","doi-asserted-by":"publisher","unstructured":"Lee, W., Sharma, R., Aiken, A.: On automatically proving the correctness of math.h implementations. Proc. ACM on Prog. Lang. (POPL) 2(47), 1\u201332 (2018). https:\/\/doi.org\/10.1145\/3158135","DOI":"10.1145\/3158135"},{"key":"5_CR25","doi-asserted-by":"publisher","unstructured":"Leino, K.R.M.: Program proving using intermediate verification languages (IVLs) like Boogie and Why3. ACM SIGAda Ada Letters 32(3), 25\u201326 (11 2012). https:\/\/doi.org\/10.1145\/2402709.2402689","DOI":"10.1145\/2402709.2402689"},{"key":"5_CR26","doi-asserted-by":"publisher","unstructured":"Lewis, R.H., Wester, M.: Comparison of polynomial-oriented computer algebra systems. SIGSAM Bull. 33(4), 5\u201313 (12 1999). https:\/\/doi.org\/10.1145\/500457.500459","DOI":"10.1145\/500457.500459"},{"key":"5_CR27","doi-asserted-by":"publisher","unstructured":"Miller, B.R., Youssef, A.: Technical aspects of the digital library of mathematical functions. Ann. Math. Artif. Intell. 38(1-3), 121\u2013136 (2003). https:\/\/doi.org\/10.1023\/A:1022967814992","DOI":"10.1023\/A:1022967814992"},{"key":"5_CR28","doi-asserted-by":"publisher","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL - A Proof Assistant for Higher-Order Logic, Lecture Notes in Computer Science, vol.\u00a02283. Springer Berlin Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45949-9","DOI":"10.1007\/3-540-45949-9"},{"key":"5_CR29","unstructured":"Parisse, B.: Compiling LATEX to computer algebra-enabled HTML5 http:\/\/arxiv.org\/abs\/1707.01271"},{"key":"5_CR30","doi-asserted-by":"publisher","unstructured":"Prieto, H., Dalmas, S., Papegay, Y.: Mathematica as an OpenMath application 34(2), 22\u201326. https:\/\/doi.org\/10.1145\/362001.362016","DOI":"10.1145\/362001.362016"},{"key":"5_CR31","doi-asserted-by":"publisher","unstructured":"Schubotz, M., Greiner-Petter, A., Scharpf, P., Meuschke, N., Cohl, H.S., Gipp, B.: Improving the representation and conversion of mathematical formulae by considering their textual context. In: ACM\/IEEE JCDL. pp. 233\u2013242. ACM (2018). https:\/\/doi.org\/10.1145\/3197026.3197058","DOI":"10.1145\/3197026.3197058"},{"key":"5_CR32","doi-asserted-by":"publisher","unstructured":"Schubotz, M., Grigorev, A., Leich, M., Cohl, H.S., Meuschke, N., Gipp, B., Youssef, A.S., Markl, V.: Semantification of identifiers in mathematics for better math information retrieval. In: ACM SIGIR\u201916. pp. 135\u2013144. ACM Press (2016). https:\/\/doi.org\/10.1145\/2911451.2911503","DOI":"10.1145\/2911451.2911503"},{"key":"5_CR33","doi-asserted-by":"publisher","unstructured":"Shan, R., Youssef, A.: Towards math terms disambiguation using machine learning. In: Kamareddine, F., Sacerdoti Coen, C. (eds.) Proceedings of the International Conference on Intelligent Computer Mathematics (CICM). Lecture Notes in Computer Science, vol. 12833, pp. 90\u2013106. Springer. https:\/\/doi.org\/10.1007\/978-3-030-81097-9_7","DOI":"10.1007\/978-3-030-81097-9_7"},{"key":"5_CR34","doi-asserted-by":"publisher","unstructured":"Youssef, A.: Part-of-math tagging and applications. In: Intelligent Computer Mathematics CICM. Lecture Notes in Computer Science, vol. 10383, pp. 356\u2013374. Springer (2017). https:\/\/doi.org\/10.1007\/978-3-319-62075-6_25","DOI":"10.1007\/978-3-319-62075-6_25"},{"key":"5_CR35","doi-asserted-by":"publisher","unstructured":"Youssef, A., Miller, B.R.: A contextual and labeled math-dataset derived from NIST\u2019s DLMF. In: Intelligent Computer Mathematics CICM. Lecture Notes in Computer Science, vol. 12236, pp. 324\u2013330. Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-53518-6_25","DOI":"10.1007\/978-3-030-53518-6_25"},{"key":"5_CR36","doi-asserted-by":"publisher","unstructured":"Zanibbi, R., Oard, D.W., Agarwal, A., Mansouri, B.: Overview of ARQMath 2020: CLEF lab on answer retrieval for questions on math. In: CLEF. Lecture Notes in Computer Science, vol. 12260, pp. 169\u2013193. Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-58219-7_15","DOI":"10.1007\/978-3-030-58219-7_15"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-99524-9_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,3,29]],"date-time":"2022-03-29T06:18:25Z","timestamp":1648534705000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-99524-9_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783030995232","9783030995249"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-99524-9_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"30 March 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Munich","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Germany","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2 April 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 April 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2022\/tacas","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"159","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"46","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"4","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"29% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"10","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"16 tool papers of the affiliated competition SV-Comp and 1 paper consisting of the competition report are also included in the proceedings","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}