×

Verified interactive computation of definite integrals. (English) Zbl 07437096

Platzer, André (ed.) et al., Automated deduction – CADE 28. 28th international conference on automated deduction, virtual event, July 12–15, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12699, 485-503 (2021).
Summary: Symbolic computation is involved in many areas of mathematics, as well as in analysis of physical systems in science and engineering. Computer algebra systems present an easy-to-use interface for performing these calculations, but do not provide strong guarantees of correctness. In contrast, interactive theorem proving provides much stronger guarantees of correctness, but requires more time and expertise. In this paper, we propose a general framework for combining these two methods, and demonstrate it using computation of definite integrals. It allows the user to carry out step-by-step computations in a familiar user interface, while also verifying the computation by translating it to proofs in higher-order logic. The system consists of an intermediate language for recording computations, proof automation for simplification and inequality checking, and heuristic integration methods. A prototype is implemented in Python based on HolPy, and tested on a large collection of examples at the undergraduate level.
For the entire collection see [Zbl 1475.68026].

MSC:

03B35 Mechanization of proofs and logical operations
68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] The HOL 4 system. http://hol.sourceforge.net/
[2] MIT Integration Bee. http://www.mit.edu/ pax/integrationbee.html, accessed: 2020-1-22
[3] Adams, A., Dunstan, M., Gottliebsen, H., Kelsey, T., Martin, U., Owre, S.: Computer algebra meets automated theorem proving: Integrating Maple and PVS. In: Boulton, R.J., Jackson, P.B. (eds.) Theorem Proving in Higher Order Logics. Lecture Notes in Computer Science, vol. 2152, pp. 27-42. Springer Berlin Heidelberg, Berlin, Heidelberg (2001) · Zbl 1005.68997
[4] Althoff, M., Frehse, G., Girard, A.: Set propagation techniques for reachability analysis. Annual Review of Control, Robotics, and Autonomous Systems 4(1) (2021)
[5] Arias, E.J.G., Pin, B., Jouvelot, P.: jsCoq: Towards hybrid theorem proving interfaces. In: Autexier, S., Quaresma, P. (eds.) Proceedings of the 12th Workshop on User Interfaces for Theorem Provers, UITP 2016, Coimbra, Portugal, 2nd July 2016. EPTCS, vol. 239, pp. 15-27 (2016)
[6] Aström, K.J., Murray, R.M.: Feedback Systems: An Introduction for Scientists and Engineers. Princeton University Press, Princeton (2008) · Zbl 1144.93001
[7] Avigad, J., Lewis, R.Y., Roux, C.: A heuristic prover for real inequalities. J. Autom. Reasoning 56(3), 367-386 (2016) · Zbl 1356.68174
[8] Ballarin, C., Homann, K., Calmet, J.: Theorems and algorithms: An interface between Isabelle and Maple. In: Levelt, A.H.M. (ed.) Proceedings of the 1995 International Symposium on Symbolic and Algebraic Computation. p. 150-157. ISSAC ’95, Association for Computing Machinery, New York, NY, USA (1995) · Zbl 0922.68080
[9] Bohrer, B., Rahli, V., Vukotic, I., Völp, M., Platzer, A.: Formally verified differential dynamic logic. In: Bertot, Y., Vafeiadis, V. (eds.) Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, Paris, France, January 16-17, 2017. pp. 208-221 (2017)
[10] Bréhard, F., Mahboubi, A., Pous, D.: A certificate-based approach to formally verified approximations. In: Harrison, J., O’Leary, J., Tolmach, A. (eds.) 10th International Conference on Interactive Theorem Proving, ITP 2019, September 9-12, 2019, Portland, OR, USA. LIPIcs, vol. 141, pp. 8:1-8:19 (2019) · Zbl 07649957
[11] Buchberger, B., Jebelean, T., Kutsia, T., Maletzky, A., Windsteiger, W.: Theorema 2.0: Computer-assisted natural-style mathematics. J. Formaliz. Reason. 9(1), 149-185 (2016) · Zbl 1451.68319
[12] Butler, R.W.: Formalization of the integral calculus in the PVS theorem prover. J. Formalized Reasoning 2(1), 1-26 (2009) · Zbl 1175.68410
[13] Chen, S., Wang, G., Li, X., Zhang, Q., Shi, Z., Guan, Y.: Formalization of camera pose estimation algorithm based on rodrigues formula. Formal Aspects Comput. 32(4-6), 417-437 (2020) · Zbl 1458.68226
[14] Chyzak, F., Mahboubi, A., Sibut-Pinote, T., Tassi, E.: A computer-algebra-based formal proof of the irrationality of \(\zeta (3)\). In: Klein, G., Gamboa, R. (eds.) Interactive Theorem Proving. Lecture Notes in Computer Science, vol. 8558, pp. 160-176. Springer International Publishing, Cham (2014) · Zbl 1416.68155
[15] Durán, A.J., Pérez, M., Varona, J.L.: The misfortunes of a trio of mathematicians using computer algebra systems. can we trust in them? Notices Amer. Math. Soc. 61(10), 1249-1252 (2014) · Zbl 1338.68299
[16] Eberl, M.: Verified real asymptotics in Isabelle/HOL. In: Davenport, J.H., Wang, D., Kauers, M., Bradford, R.J. (eds.) Proceedings of the 2019 on International Symposium on Symbolic and Algebraic Computation, ISSAC 2019, Beijing, China, July 15-18, 2019. pp. 147-154. ACM (2019) · Zbl 1467.68204
[17] Fu, H., Zhong, X., Zeng, Z.: Automated and readable simplification of trigonometric expressions. Mathematical and Computer Modelling 44(11-12), 1169-1177 (2006) · Zbl 1137.68065
[18] Fulton, N., Mitsch, S., Quesel, J., Völp, M., Platzer, A.: KeYmaera X: an axiomatic tactical theorem prover for hybrid systems. In: Felty, A.P., Middeldorp, A. (eds.) Automated Deduction - CADE-25 - 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings. Lecture Notes in Computer Science, vol. 9195, pp. 527-538 (2015) · Zbl 1465.68281
[19] Geddes, K.O., Czapor, S.R., Labahn, G.: The Risch Integration Algorithm, pp. 511-573. Springer US, Boston, MA (1992)
[20] Harrison, J.: Theorem proving with the real numbers. CPHC/BCS distinguished dissertations, Springer (1998) · Zbl 0932.68099
[21] Harrison, J.: HOL Light: An overview. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) Theorem Proving in Higher Order Logics. Lecture Notes in Computer Science, vol. 5674, pp. 60-66. Springer Berlin Heidelberg, Berlin, Heidelberg (2009) · Zbl 1252.68255
[22] Harrison, J.: Formal proofs of hypergeometric sums - dedicated to the memory of Andrzej Trybulec. J. Autom. Reasoning 55(3), 223-243 (2015) · Zbl 1356.68190
[23] Harrison, J., Théry, L.: A skeptic’s approach to combining HOL and Maple. J. Autom. Reason. 21(3), 279-294 (1998) · Zbl 0916.68142
[24] Hölzl, J., Heller, A.: Three chapters of measure theory in Isabelle/HOL. In: van Eekelen, M., Geuvers, H., Schmaltz, J., Wiedijk, F. (eds.) Interactive Theorem Proving - Second International Conference, ITP 2011, Berg en Dal, The Netherlands, August 22-25, 2011. Proceedings. Lecture Notes in Computer Science, vol. 6898, pp. 135-151 (2011) · Zbl 1342.68287
[25] Immler, F.: A verified ODE solver and the Lorenz attractor. J. Autom. Reason. 61(1-4), 73-111 (2018) · Zbl 1448.68460
[26] Immler, F., Traut, C.: The flow of ODEs. In: Blanchette, J.C., Merz, S. (eds.) Interactive Theorem Proving - 7th International Conference, ITP 2016, Nancy, France, August 22-25, 2016, Proceedings. Lecture Notes in Computer Science, vol. 9807, pp. 184-199 (2016) · Zbl 1468.68324
[27] Kouba, D.A.: The calculus page problems list. https://www.math.ucdavis.edu/ kouba/ProblemsList.html, accessed: 2020-1-22
[28] Lewis, R.Y.: An extensible ad hoc interface between Lean and Mathematica. In: Dubois, C., Paleo, B.W. (eds.) Proceedings of the Fifth Workshop on Proof eXchange for Theorem Proving, PxTP 2017, Brasília, Brazil, 23-24 September 2017. EPTCS, vol. 262, pp. 23-37 (2017)
[29] Li, L., Shi, Z., Guan, Y., Zhang, Q., Li, Y.: Formalization of geometric algebra in HOL Light. J. Autom. Reasoning 63(3), 787-808 (2019) · Zbl 1468.68329
[30] Mahboubi, A., Melquiond, G., Sibut-Pinote, T.: Formally verified approximations of definite integrals. J. Autom. Reason. 62(2), 281-300 (2019) · Zbl 1468.68301
[31] Mhamdi, T., Hasan, O., Tahar, S.: On the formalization of the Lebesgue integration theory in HOL. In: Kaufmann, M., Paulson, L.C. (eds.) Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings. Lecture Notes in Computer Science, vol. 6172, pp. 387-402 (2010) · Zbl 1291.68362
[32] Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL - A Proof Assistant for Higher-Order Logic. Lecture Notes in Computer Science, vol. 2283. Springer (2002) · Zbl 0994.68131
[33] Oppenheim, A.V., Willsky, A.S.: Signals and Systems. Prentice Hall, Upper Saddle River, New Jersey (1996) · Zbl 0539.93001
[34] Platzer, A.: Differential dynamic logic for hybrid systems. J. Autom. Reason. 41(2), 143-189 (2008) · Zbl 1181.03035
[35] Platzer, A.: A complete uniform substitution calculus for differential dynamic logic. J. Autom. Reason. 59(2), 219-265 (2017) · Zbl 1437.03119
[36] Prajna, S., Jadbabaie, A.: Safety verification of hybrid systems using barrier certificates. In: Alur, R., Pappas, G.J. (eds.) Hybrid Systems: Computation and Control, 7th International Workshop, HSCC 2004, Philadelphia, PA, USA, March 25-27, 2004, Proceedings. Lecture Notes in Computer Science, vol. 2993, pp. 477-492 (2004) · Zbl 1135.93317
[37] Rashid, A., Hasan, O.: On the formalization of Fourier transform in higher-order logic. In: Blanchette, J.C., Merz, S. (eds.) Interactive Theorem Proving. Lecture Notes in Computer Science, vol. 9807, pp. 483-490. Springer International Publishing, Cham (2016) · Zbl 1478.68441
[38] Rashid, A., Hasan, O.: Formal analysis of continuous-time systems using Fourier transform. J. Symb. Comput. 90, 65-88 (2019) · Zbl 1395.68251
[39] Rich, A.D., Scheibe, P., Abbasi, N.M.: Rule-based integration: An extensive system of symbolic integration rules. J. Open Source Softw. 3(32), 1073 (2018)
[40] Richter, S.: Formalizing integration theory with an application to probabilistic algorithms. In: Slind, K., Bunker, A., Gopalakrishnan, G. (eds.) Theorem Proving in Higher Order Logics, 17th International Conference, TPHOLs 2004, Park City, Utah, USA, September 14-17, 2004, Proceedings. Lecture Notes in Computer Science, vol. 3223, pp. 271-286 (2004) · Zbl 1099.68736
[41] Sankaranarayanan, S., Sipma, H., Manna, Z.: Constructing invariants for hybrid systems. In: Alur, R., Pappas, G.J. (eds.) Hybrid Systems: Computation and Control, 7th International Workshop, HSCC 2004, Philadelphia, PA, USA, March 25-27, 2004, Proceedings. Lecture Notes in Computer Science, vol. 2993, pp. 539-554 (2004) · Zbl 1135.93322
[42] Selsam, D., Liang, P., Dill, D.L.: Developing bug-free machine learning systems with formal mathematics. In: Precup, D., Teh, Y.W. (eds.) Proceedings of the 34th International Conference on Machine Learning, ICML 2017, Sydney, NSW, Australia, 6-11 August 2017. Proceedings of Machine Learning Research, vol. 70, pp. 3047-3056 (2017)
[43] Shi, Z., Gu, W., Li, X., Guan, Y., Ye, S., Zhang, J., Wei, H.: The gauge integral theory in HOL4. J. Applied Mathematics 2013, 160875:1-160875:7 (2013) · Zbl 1268.65033
[44] Shi, Z., Wu, A., Yang, X., Guan, Y., Li, Y., Song, X.: Formal analysis of the kinematic Jacobian in screw theory. Formal Aspects Comput. 30(6), 739-757 (2018) · Zbl 1426.70008
[45] Slagle, J.R.: A heuristic program that solves symbolic integration problems in freshman calculus. J. ACM 10(4), 507-520 (1963) · Zbl 0113.32801
[46] Taqdees, S.H., Hasan, O.: Formalization of Laplace transform using the multivariable calculus theory of HOL-Light. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) Logic for Programming, Artificial Intelligence, and Reasoning - 19th International Conference, LPAR-19, Stellenbosch, South Africa, December 14-19, 2013. Proceedings. Lecture Notes in Computer Science, vol. 8312, pp. 744-758 (2013) · Zbl 1407.68443
[47] Wang, S., Zhan, N., Zou, L.: An improved HHL prover: An interactive theorem prover for hybrid systems. In: Butler, M., Conchon, S., Zaïdi, F. (eds.) Formal Methods and Software Engineering - 17th International Conference on Formal Engineering Methods, ICFEM 2015, Paris, France, November 3-5, 2015, Proceedings. Lecture Notes in Computer Science, vol. 9407, pp. 382-399 (2015)
[48] Wenzel, M.: The Isabelle/Isar reference manual. http://isabelle.in.tum.de/doc/isar-ref.pdf · Zbl 1431.68125
[49] Zhan, B., Ji, Z., Zhou, W., Xiang, C., Hou, J., Sun, W.: Design of point-and-click user interfaces for proof assistants. In: Ait-Ameur, Y., Qin, S. (eds.) Formal Methods and Software Engineering - 21st International Conference on Formal Engineering Methods, ICFEM 2019, Shenzhen, China, November 5-9, 2019, Proceedings. Lecture Notes in Computer Science, vol. 11852, pp. 86-103 (2019)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.