{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,18]],"date-time":"2026-04-18T22:49:57Z","timestamp":1776552597897,"version":"3.51.2"},"publisher-location":"Cham","reference-count":25,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030798758","type":"print"},{"value":"9783030798765","type":"electronic"}],"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>\"Image missing\"\n is an emerging <jats:italic>natural proof assistant<\/jats:italic> that accepts input in the controlled natural language ForTheL. \n\"Image missing\"\n is included in the current version of the Isabelle\/PIDE which allows comfortable editing and asynchronous proof-checking of ForTheL texts. The  dialect of ForTheL can be typeset by \n\"Image missing\"\n into documents that approximate the language and appearance of ordinary mathematical texts.<\/jats:p>","DOI":"10.1007\/978-3-030-79876-5_36","type":"book-chapter","created":{"date-parts":[[2021,7,7]],"date-time":"2021-07-07T09:20:19Z","timestamp":1625649619000},"page":"614-624","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["The Isabelle\/Naproche Natural Language Proof Assistant"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2697-7253","authenticated-orcid":false,"given":"Adrian","family":"De Lon","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2266-134X","authenticated-orcid":false,"given":"Peter","family":"Koepke","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3538-9688","authenticated-orcid":false,"given":"Anton","family":"Lorenzen","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8932-8843","authenticated-orcid":false,"given":"Adrian","family":"Marti","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5386-5134","authenticated-orcid":false,"given":"Marcel","family":"Sch\u00fctz","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3753-8280","authenticated-orcid":false,"given":"Makarius","family":"Wenzel","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2021,7,5]]},"reference":[{"key":"36_CR1","unstructured":"Cramer, M.: Proof-checking mathematical texts in controlled natural language. Ph.D. thesis, University of Bonn (2013), http:\/\/hdl.handle.net\/20.500.11811\/5780"},{"key":"36_CR2","unstructured":"Cramer, M., Koepke, P., K\u00fchlwein, D., Schr\u00f6der, B.: The Naproche system (2009), https:\/\/citeseerx.ist.psu.edu\/viewdoc\/summary?doi=10.1.1.211.3401"},{"key":"36_CR3","unstructured":"Frerix, S., Koepke, P.: Automatic proof-checking of ordinary mathematical texts. Proceedings of the Workshop Formal Mathematics for Mathematicians (2018), http:\/\/ceur-ws.org\/Vol-2307\/paper13.pdf"},{"key":"36_CR4","unstructured":"Giero, M., Wiedijk, F.: MMode, a Mizar mode for the proof assistant Coq (2003), https:\/\/www.cs.ru.nl\/~freek\/mmode\/mmode.pdf"},{"key":"36_CR5","unstructured":"Hales, T.: Formal abstracts (2020), https:\/\/formalabstracts.github.io"},{"key":"36_CR6","doi-asserted-by":"crossref","unstructured":"Harrison, J.: A mizar mode for HOL. In: von Wright, J., Grundy, J., Harrison, J. (eds.) Theorem Proving in Higher Order Logics: 9th International Conference, TPHOLs\u201996. Lecture Notes in Computer Science, vol. 1125, pp. 203\u2013220. Springer-Verlag, Turku, Finland (1996)","DOI":"10.1007\/BFb0105406"},{"key":"36_CR7","doi-asserted-by":"crossref","unstructured":"Humayoun, M., Raffalli, C.: MathNat - mathematical text in a controlled natural language. Journal on Research in Computing Science 46 (2010)","DOI":"10.1145\/1943628.1943665"},{"key":"36_CR8","unstructured":"Isabelle contributors: The Isabelle 2021 release (2021), https:\/\/isabelle.in.tum.de"},{"key":"36_CR9","doi-asserted-by":"publisher","unstructured":"Kaliszyk, C., Rabe, F.: A survey of languages for formalizing mathematics. In: Benzm\u00fcller, C., Miller, B. (eds.) Intelligent Computer Mathematics. pp. 138\u2013156. Springer International Publishing, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53518-6_9","DOI":"10.1007\/978-3-030-53518-6_9"},{"key":"36_CR10","unstructured":"Koepke, P.: Textbook mathematics in the Naproche-SAD system. In: Brady, E., Davenport, J., Farmer, W.M., Kaliszyk, C., Kohlhase, A., Kohlhase, M., M\u00fcller, D., P\u0105k, K., Coen, C.S. (eds.) Joint Proceedings of the FMM and LML Workshops (2019), http:\/\/ceur-ws.org\/Vol-2634\/FMM4.pdf"},{"key":"36_CR11","unstructured":"Mizar, http:\/\/www.mizar.org\/"},{"key":"36_CR12","doi-asserted-by":"publisher","unstructured":"de Moura, L.M., Kong, S., Avigad, J., van Doorn, F., von Raumer, J.: The Lean Theorem Prover (system description). In: Felty, A.P., Middeldorp, A. (eds.) Automated Deduction \u2013 CADE-25 \u2013 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings. Lecture Notes in Computer Science, vol. 9195, pp. 378\u2013388. Springer (2015). https:\/\/doi.org\/10.1007\/978-3-319-21401-6_26","DOI":"10.1007\/978-3-319-21401-6_26"},{"key":"36_CR13","unstructured":"Naproche contributors: FLib, https:\/\/github.com\/naproche-community\/FLib"},{"key":"36_CR14","unstructured":"Paskevich, A.: M\u00e9thodes de formalisation des connaissances et des raisonnements math\u00e9matiques: aspects appliqu\u00e9s et th\u00e9oriques. Ph.D. thesis, Universit\u00e9 Paris 12 (2007), http:\/\/tertium.org\/papers\/thesis-07.fr.pdf"},{"key":"36_CR15","unstructured":"Paskevich, A.: The syntax and semantics of the ForTheL language (2007), http:\/\/nevidal.org\/download\/forthel.pdf"},{"key":"36_CR16","unstructured":"Paulson, L.C.: ALEXANDRIA: Large-scale formal proof for the working mathematician, https:\/\/www.cl.cam.ac.uk\/~lp15\/Grants\/Alexandria"},{"key":"36_CR17","doi-asserted-by":"publisher","unstructured":"Paulson, L.C., Blanchette, J.C.: Three years of experience with Sledgehammer, a practical link between automatic and interactive theorem provers. In: Sutcliffe, G., Schulz, S., Ternovska, E. (eds.) IWIL 2010. The 8th International Workshop on the Implementation of Logics. EPiC Series in Computing, vol. 2, pp. 1\u201311. EasyChair (2012). https:\/\/doi.org\/10.29007\/36dt","DOI":"10.29007\/36dt"},{"key":"36_CR18","doi-asserted-by":"publisher","unstructured":"Paulson, L.C., Nipkow, T., Wenzel, M.: From LCF to Isabelle\/HOL. Formal Aspects of Computing 31, 675\u2013698 (September 2019), 1\u201324 (2019). https:\/\/doi.org\/10.1007\/s00165-019-00492-1, Springer, London","DOI":"10.1007\/s00165-019-00492-1"},{"key":"36_CR19","unstructured":"Schulz, S.: The E Theorem Prover, https:\/\/eprover.org"},{"key":"36_CR20","doi-asserted-by":"publisher","unstructured":"Verchinine, K., Lyaletski, A., Paskevich, A.: System for automated deduction (SAD): a tool for proof verification. Automated Deduction\u2013CADE-21 pp. 398\u2013403 (2007). https:\/\/doi.org\/10.1007\/978-3-540-73595-3_29","DOI":"10.1007\/978-3-540-73595-3_29"},{"key":"36_CR21","doi-asserted-by":"publisher","unstructured":"Verchinine, K., Lyaletski, A., Paskevich, A., Anisimov, A.: On correctness of mathematical texts from a logical and practical point of view. In: Autexier, S., Campbell, J., Rubio, J., Sorge, V., Suzuki, M., Wiedijk, F. (eds.) International Conference on Intelligent Computer Mathematics. pp. 583\u2013598. Springer (2008). https:\/\/doi.org\/10.1007\/978-3-540-85110-3_47","DOI":"10.1007\/978-3-540-85110-3_47"},{"key":"36_CR22","unstructured":"Wenzel, M.: The Isar proof language in 2016 (2016), http:\/\/sketis.net\/wp-content\/uploads\/2016\/08\/Isabelle_Workshop_2016_Isar.pdf"},{"key":"36_CR23","doi-asserted-by":"publisher","unstructured":"Wenzel, M.: Interaction with formal mathematical documents in Isabelle\/PIDE. In: Kaliszyk, C., Brady, E., Kohlhase, A., Sacerdoti Coen, C. (eds.) Intelligent Computer Mathematics (CICM 2019). Lecture Notes in Artificial Intelligence, vol. 11617. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-23250-4_1","DOI":"10.1007\/978-3-030-23250-4_1"},{"key":"36_CR24","doi-asserted-by":"crossref","unstructured":"Wenzel, M.: Isar \u2013 a generic interpretative approach to readable formal proof documents. In: Bertot, Y., Dowek, G., Th\u00e9ry, L., Hirschowitz, A., Paulin, C. (eds.) Theorem Proving in Higher Order Logics, pp. 167\u2013183. Springer Berlin Heidelberg, Berlin, Heidelberg (1999)","DOI":"10.1007\/3-540-48256-3_12"},{"key":"36_CR25","doi-asserted-by":"crossref","unstructured":"Wiedijk, F.: Mizar light for HOL light. In: Boulton, R.J., Jackson, P.B. (eds.) TPHOLs: International Conference on Theorem Proving in Higher Order Logics. pp. 378\u2013393. Springer (2001)","DOI":"10.1007\/3-540-44755-5_26"}],"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_36","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,7,7]],"date-time":"2021-07-07T09:36:56Z","timestamp":1625650616000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-79876-5_36"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030798758","9783030798765"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-79876-5_36","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"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)"}}]}}