{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,18]],"date-time":"2026-04-18T22:51:19Z","timestamp":1776552679444,"version":"3.51.2"},"publisher-location":"Cham","reference-count":21,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031646256","type":"print"},{"value":"9783031646263","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"DOI":"10.1007\/978-3-031-64626-3_26","type":"book-chapter","created":{"date-parts":[[2024,7,13]],"date-time":"2024-07-13T13:01:58Z","timestamp":1720875718000},"page":"446-464","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["A Natural Formalized Proof Language"],"prefix":"10.1007","author":[{"given":"Lihan","family":"Xie","sequence":"first","affiliation":[]},{"given":"Zhicheng","family":"Hui","sequence":"additional","affiliation":[]},{"given":"Qinxiang","family":"Cao","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,7,14]]},"reference":[{"key":"26_CR1","doi-asserted-by":"crossref","unstructured":"Appel, K.I., Haken, W.: Every Planar Map is Four Colorable, vol. 98. American Mathematical Soc. (1989)","DOI":"10.1090\/conm\/098"},{"key":"26_CR2","unstructured":"Barras, B., et al.: The coq proof assistant reference manual. INRIA, version 6(11) (1999)"},{"key":"26_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1007\/3-540-44755-5_7","volume-title":"Theorem Proving in Higher Order Logics","author":"G Bauer","year":"2001","unstructured":"Bauer, G., Wenzel, M.: Calculational reasoning revisited an Isabelle\/Isar experience. In: Boulton, R.J., Jackson, P.B. (eds.) TPHOLs 2001. LNCS, vol. 2152, pp. 75\u201390. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-44755-5_7"},{"key":"26_CR4","unstructured":"Bertot, Y., Castran, P.: Interactive Theorem Proving and Program Development: Coq\u2019Art The Calculus of Inductive Constructions, 1st (edn.) Springer, Incorporated (2010)"},{"key":"26_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1007\/978-3-642-03359-9_6","volume-title":"Theorem Proving in Higher Order Logics","author":"A Bove","year":"2009","unstructured":"Bove, A., Dybjer, P., Norell, U.: A brief overview of Agda \u2013 a functional language with dependent types. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 73\u201378. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-03359-9_6"},{"key":"26_CR6","unstructured":"Carl, M., Krapf, R.: Diproche\u2013ein automatisierter tutor f\u00fcr den einstieg ins beweisen. Digitale Kompetenzen und Curriculare Konsequenzen, p. 43 (2020)"},{"key":"26_CR7","unstructured":"Carter, N.C., Monks, K.G.: Using the proof-checking word processor lurch to teach proof-writing (2014)"},{"key":"26_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"26_CR9","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/3-540-44404-1_7","volume-title":"Logic for Programming and Automated Reasoning","author":"D Delahaye","year":"2000","unstructured":"Delahaye, D.: A tactic language for the system Coq. In: Parigot, M., Voronkov, A. (eds.) LPAR 2000. LNAI, vol. 1955, pp. 85\u201395. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/3-540-44404-1_7"},{"key":"26_CR10","unstructured":"Donnelly, C.: Bison the YACC-compatible parser generator. Technical report, Free Software Foundation (1988)"},{"issue":"11","key":"26_CR11","first-page":"1382","volume":"55","author":"G Gonthier","year":"2008","unstructured":"Gonthier, G., et al.: Formal proof-the four-color theorem. Notices AMS 55(11), 1382\u20131393 (2008)","journal-title":"Notices AMS"},{"key":"26_CR12","unstructured":"Hendrycks, D., et al.: Measuring mathematical problem solving with the math dataset (2021)"},{"key":"26_CR13","unstructured":"Jiang, A.Q., et al.: Draft, sketch, and prove: Guiding formal theorem provers with informal proofs. arXiv preprint arXiv:2210.12283 (2022)"},{"key":"26_CR14","unstructured":"Lample, G., et al.: Hypertree proof search for neural theorem proving. In: Advances in Neural Information Processing Systems, vol. 35, pp. 26337\u201326349 (2022)"},{"key":"26_CR15","unstructured":"Levine, J.: Flex & Bison: Text Processing Tools. O\u2019Reilly Media, Inc. (2009)"},{"key":"26_CR16","doi-asserted-by":"crossref","unstructured":"Paulson, L.C.: Isabelle: A Generic Theorem Prover. Springer, Berlin (1994)","DOI":"10.1007\/BFb0030541"},{"key":"26_CR17","unstructured":"Polu, S., Sutskever, I.: Generative language modeling for automated theorem proving. arXiv preprint arXiv:2009.03393 (2020)"},{"key":"26_CR18","unstructured":"Wemmenhove, J., Beurskens, T., McCarren, S., Moraal, J., Tuin, D., Portegies, J.: Waterproof: educational software for learning how to write mathematical proofs. arXiv preprint arXiv:2211.13513 (2022)"},{"key":"26_CR19","doi-asserted-by":"crossref","unstructured":"Wenzel, M.: Isar - a generic interpretative approach to readable formal proof documents. In: International Conference on Theorem Proving in Higher Order Logics (1999)","DOI":"10.1007\/3-540-48256-3_12"},{"key":"26_CR20","unstructured":"Wu, Y., et al.: Autoformalization with large language models. Advances in Neural Information Processing Systems, vol. 35, pp. 32353\u201332368 (2022)"},{"key":"26_CR21","doi-asserted-by":"crossref","unstructured":"Xie, L., Hui, Z., Cao, Q.: A natural formalized proof language (long version). arXiv preprint arXiv:2405.07973 (2024)","DOI":"10.1007\/978-3-031-64626-3_26"}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-64626-3_26","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,12]],"date-time":"2025-03-12T16:16:55Z","timestamp":1741796215000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-64626-3_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031646256","9783031646263"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-64626-3_26","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"14 July 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TASE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Theoretical Aspects of Software Engineering","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Guiyang","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"China","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29 July 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"1 August 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tase2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/tase2024.github.io\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}