{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T18:44:45Z","timestamp":1742928285382,"version":"3.40.3"},"publisher-location":"Cham","reference-count":49,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030798758"},{"type":"electronic","value":"9783030798765"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,7,5]],"date-time":"2021-07-05T00:00:00Z","timestamp":1625443200000},"content-version":"vor","delay-in-days":185,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>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.<\/jats:p>","DOI":"10.1007\/978-3-030-79876-5_28","type":"book-chapter","created":{"date-parts":[[2021,7,7]],"date-time":"2021-07-07T09:20:19Z","timestamp":1625649619000},"page":"485-503","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Verified Interactive Computation of Definite Integrals"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1521-7379","authenticated-orcid":false,"given":"Runqing","family":"Xu","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5445-2684","authenticated-orcid":false,"given":"Liming","family":"Li","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5377-9351","authenticated-orcid":false,"given":"Bohua","family":"Zhan","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2021,7,5]]},"reference":[{"key":"28_CR1","unstructured":"The HOL 4 system. http:\/\/hol.sourceforge.net\/"},{"key":"28_CR2","unstructured":"MIT Integration Bee. http:\/\/www.mit.edu\/~pax\/integrationbee.html, accessed: 2020-1-22"},{"key":"28_CR3","doi-asserted-by":"crossref","unstructured":"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\u201342. Springer Berlin Heidelberg, Berlin, Heidelberg (2001)","DOI":"10.1007\/3-540-44755-5_4"},{"key":"28_CR4","doi-asserted-by":"crossref","unstructured":"Althoff, M., Frehse, G., Girard, A.: Set propagation techniques for reachability analysis. Annual Review of Control, Robotics, and Autonomous Systems 4(1) (2021)","DOI":"10.1146\/annurev-control-071420-081941"},{"key":"28_CR5","doi-asserted-by":"crossref","unstructured":"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\u201327 (2016)","DOI":"10.4204\/EPTCS.239.2"},{"key":"28_CR6","doi-asserted-by":"crossref","unstructured":"Astr\u00f6m, K.J., Murray, R.M.: Feedback Systems: An Introduction for Scientists and Engineers. Princeton University Press, Princeton (2008)","DOI":"10.1515\/9781400828739"},{"key":"28_CR7","doi-asserted-by":"crossref","unstructured":"Avigad, J., Lewis, R.Y., Roux, C.: A heuristic prover for real inequalities. J. Autom. Reasoning 56(3), 367\u2013386 (2016)","DOI":"10.1007\/s10817-015-9356-y"},{"key":"28_CR8","doi-asserted-by":"crossref","unstructured":"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\u2013157. ISSAC \u201995, Association for Computing Machinery, New York, NY, USA (1995)","DOI":"10.1145\/220346.220366"},{"key":"28_CR9","doi-asserted-by":"crossref","unstructured":"Bohrer, B., Rahli, V., Vukotic, I., V\u00f6lp, 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\u201317, 2017. pp. 208\u2013221 (2017)","DOI":"10.1145\/3018610.3018616"},{"key":"28_CR10","unstructured":"Br\u00e9hard, F., Mahboubi, A., Pous, D.: A certificate-based approach to formally verified approximations. In: Harrison, J., O\u2019Leary, J., Tolmach, A. (eds.) 10th International Conference on Interactive Theorem Proving, ITP 2019, September 9\u201312, 2019, Portland, OR, USA. LIPIcs, vol. 141, pp. 8:1\u20138:19 (2019)"},{"key":"28_CR11","unstructured":"Buchberger, B., Jebelean, T., Kutsia, T., Maletzky, A., Windsteiger, W.: Theorema 2.0: Computer-assisted natural-style mathematics. J. Formaliz. Reason. 9(1), 149\u2013185 (2016)"},{"key":"28_CR12","unstructured":"Butler, R.W.: Formalization of the integral calculus in the PVS theorem prover. J. Formalized Reasoning 2(1), 1\u201326 (2009)"},{"key":"28_CR13","doi-asserted-by":"crossref","unstructured":"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\u2013437 (2020)","DOI":"10.1007\/s00165-020-00520-5"},{"key":"28_CR14","doi-asserted-by":"crossref","unstructured":"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\u2013176. Springer International Publishing, Cham (2014)","DOI":"10.1007\/978-3-319-08970-6_11"},{"key":"28_CR15","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 Amer. Math. Soc. 61(10), 1249\u20131252 (2014)","DOI":"10.1090\/noti1173"},{"key":"28_CR16","doi-asserted-by":"crossref","unstructured":"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\u201318, 2019. pp. 147\u2013154. ACM (2019)","DOI":"10.1145\/3326229.3326240"},{"key":"28_CR17","doi-asserted-by":"crossref","unstructured":"Fu, H., Zhong, X., Zeng, Z.: Automated and readable simplification of trigonometric expressions. Mathematical and Computer Modelling 44(11\u201312), 1169\u20131177 (2006)","DOI":"10.1016\/j.mcm.2006.04.002"},{"key":"28_CR18","doi-asserted-by":"crossref","unstructured":"Fulton, N., Mitsch, S., Quesel, J., V\u00f6lp, 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\u2013538 (2015)","DOI":"10.1007\/978-3-319-21401-6_36"},{"key":"28_CR19","doi-asserted-by":"crossref","unstructured":"Geddes, K.O., Czapor, S.R., Labahn, G.: The Risch Integration Algorithm, pp. 511\u2013573. Springer US, Boston, MA (1992)","DOI":"10.1007\/978-0-585-33247-5_12"},{"key":"28_CR20","doi-asserted-by":"crossref","unstructured":"Harrison, J.: Theorem proving with the real numbers. CPHC\/BCS distinguished dissertations, Springer (1998)","DOI":"10.1007\/978-1-4471-1591-5"},{"key":"28_CR21","doi-asserted-by":"crossref","unstructured":"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\u201366. Springer Berlin Heidelberg, Berlin, Heidelberg (2009)","DOI":"10.1007\/978-3-642-03359-9_4"},{"key":"28_CR22","doi-asserted-by":"crossref","unstructured":"Harrison, J.: Formal proofs of hypergeometric sums - dedicated to the memory of Andrzej Trybulec. J. Autom. Reasoning 55(3), 223\u2013243 (2015)","DOI":"10.1007\/s10817-015-9338-0"},{"key":"28_CR23","doi-asserted-by":"crossref","unstructured":"Harrison, J., Th\u00e9ry, L.: A skeptic\u2019s approach to combining HOL and Maple. J. Autom. Reason. 21(3), 279\u2013294 (1998)","DOI":"10.1023\/A:1006023127567"},{"key":"28_CR24","doi-asserted-by":"crossref","unstructured":"H\u00f6lzl, 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\u2013151 (2011)","DOI":"10.1007\/978-3-642-22863-6_12"},{"key":"28_CR25","doi-asserted-by":"crossref","unstructured":"Immler, F.: A verified ODE solver and the Lorenz attractor. J. Autom. Reason. 61(1-4), 73\u2013111 (2018)","DOI":"10.1007\/s10817-017-9448-y"},{"key":"28_CR26","doi-asserted-by":"crossref","unstructured":"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\u2013199 (2016)","DOI":"10.1007\/978-3-319-43144-4_12"},{"key":"28_CR27","unstructured":"Kouba, D.A.: The calculus page problems list. https:\/\/www.math.ucdavis.edu\/~kouba\/ProblemsList.html, accessed: 2020-1-22"},{"key":"28_CR28","doi-asserted-by":"crossref","unstructured":"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\u00edlia, Brazil, 23-24 September 2017. EPTCS, vol. 262, pp. 23\u201337 (2017)","DOI":"10.4204\/EPTCS.262.4"},{"key":"28_CR29","doi-asserted-by":"crossref","unstructured":"Li, L., Shi, Z., Guan, Y., Zhang, Q., Li, Y.: Formalization of geometric algebra in HOL Light. J. Autom. Reasoning 63(3), 787\u2013808 (2019)","DOI":"10.1007\/s10817-018-9498-9"},{"key":"28_CR30","doi-asserted-by":"crossref","unstructured":"Mahboubi, A., Melquiond, G., Sibut-Pinote, T.: Formally verified approximations of definite integrals. J. Autom. Reason. 62(2), 281\u2013300 (2019)","DOI":"10.1007\/s10817-018-9463-7"},{"key":"28_CR31","doi-asserted-by":"crossref","unstructured":"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\u2013402 (2010)","DOI":"10.1007\/978-3-642-14052-5_27"},{"key":"28_CR32","doi-asserted-by":"crossref","unstructured":"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)","DOI":"10.1007\/3-540-45949-9"},{"key":"28_CR33","unstructured":"Oppenheim, A.V., Willsky, A.S.: Signals and Systems. Prentice Hall, Upper Saddle River, New Jersey (1996)"},{"key":"28_CR34","doi-asserted-by":"crossref","unstructured":"Platzer, A.: Differential dynamic logic for hybrid systems. J. Autom. Reason. 41(2), 143\u2013189 (2008)","DOI":"10.1007\/s10817-008-9103-8"},{"key":"28_CR35","doi-asserted-by":"crossref","unstructured":"Platzer, A.: A complete uniform substitution calculus for differential dynamic logic. J. Autom. Reason. 59(2), 219\u2013265 (2017)","DOI":"10.1007\/s10817-016-9385-1"},{"key":"28_CR36","doi-asserted-by":"crossref","unstructured":"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\u2013492 (2004)","DOI":"10.1007\/978-3-540-24743-2_32"},{"key":"28_CR37","doi-asserted-by":"crossref","unstructured":"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\u2013490. Springer International Publishing, Cham (2016)","DOI":"10.1007\/978-3-319-43144-4_31"},{"key":"28_CR38","doi-asserted-by":"crossref","unstructured":"Rashid, A., Hasan, O.: Formal analysis of continuous-time systems using Fourier transform. J. Symb. Comput. 90, 65\u201388 (2019)","DOI":"10.1016\/j.jsc.2018.04.004"},{"key":"28_CR39","doi-asserted-by":"crossref","unstructured":"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)","DOI":"10.21105\/joss.01073"},{"key":"28_CR40","unstructured":"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\u2013286 (2004)"},{"key":"28_CR41","doi-asserted-by":"crossref","unstructured":"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\u2013554 (2004)","DOI":"10.1007\/978-3-540-24743-2_36"},{"key":"28_CR42","unstructured":"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\u20133056 (2017)"},{"key":"28_CR43","doi-asserted-by":"crossref","unstructured":"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\u2013160875:7 (2013)","DOI":"10.1155\/2013\/160875"},{"key":"28_CR44","doi-asserted-by":"crossref","unstructured":"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\u2013757 (2018)","DOI":"10.1007\/s00165-018-0468-0"},{"key":"28_CR45","doi-asserted-by":"crossref","unstructured":"Slagle, J.R.: A heuristic program that solves symbolic integration problems in freshman calculus. J. ACM 10(4), 507\u2013520 (1963)","DOI":"10.1145\/321186.321193"},{"key":"28_CR46","doi-asserted-by":"crossref","unstructured":"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\u2013758 (2013)","DOI":"10.1007\/978-3-642-45221-5_50"},{"key":"28_CR47","doi-asserted-by":"crossref","unstructured":"Wang, S., Zhan, N., Zou, L.: An improved HHL prover: An interactive theorem prover for hybrid systems. In: Butler, M., Conchon, S., Za\u00efdi, 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\u2013399 (2015)","DOI":"10.1007\/978-3-319-25423-4_25"},{"key":"28_CR48","unstructured":"Wenzel, M.: The Isabelle\/Isar reference manual. http:\/\/isabelle.in.tum.de\/doc\/isar-ref.pdf"},{"key":"28_CR49","doi-asserted-by":"crossref","unstructured":"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\u2013103 (2019)","DOI":"10.1007\/978-3-030-32409-4_6"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE 28"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-79876-5_28","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,3]],"date-time":"2023-01-03T05:29:47Z","timestamp":1672723787000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-79876-5_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030798758","9783030798765"],"references-count":49,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-79876-5_28","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"5 July 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CADE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Automated Deduction","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12 July 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15 July 2021","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":"cade2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.cs.cmu.edu\/~mheule\/CADE28\/","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":"76","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":"29","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":"0","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":"38% - 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":"5","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":"2 invited papers and 7 system descriptions are also included.","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)"}}]}}