{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T22:03:32Z","timestamp":1784844212888,"version":"3.55.0"},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642144172","type":"print"},{"value":"9783642144189","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-14418-9_11","type":"book-chapter","created":{"date-parts":[[2010,7,6]],"date-time":"2010-07-06T11:38:36Z","timestamp":1278416316000},"page":"170-186","source":"Crossref","is-referenced-by-count":22,"title":["The Naproche Project Controlled Natural Language Proof Checking of Mathematical Texts"],"prefix":"10.1007","author":[{"given":"Marcos","family":"Cramer","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Bernhard","family":"Fisseni","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Peter","family":"Koepke","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Daniel","family":"K\u00fchlwein","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Bernhard","family":"Schr\u00f6der","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jip","family":"Veldman","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"11_CR1","doi-asserted-by":"crossref","unstructured":"Asher, N.: Reference to Abstract Objects in Discourse (1993)","DOI":"10.1007\/978-94-011-1715-9"},{"key":"11_CR2","unstructured":"Blackburn, P., Bos, J.: Working with Discourse Representation Theory: An Advanced Course in Computational Linguistics (2003)"},{"key":"11_CR3","unstructured":"Coq Development Team: The Coq Proof Assistant Reference Manual: Version v8.1 (July 2007), http:\/\/coq.inria.fr"},{"key":"11_CR4","unstructured":"Carl, M., Cramer, M., K\u00fchlwein, D.: Landau in Naproche, ch. 1, http:\/\/www.naproche.net\/downloads\/2009\/landauChapter1.pdf"},{"key":"11_CR5","unstructured":"Cramer, M.: The Controlled Natural Language of Naproche in a nutshell, http:\/\/www.naproche.net\/wiki\/doku.php?id=dokumentation:language"},{"key":"11_CR6","unstructured":"Cramer, M.: Mathematisch-logische Aspekte von Beweisrepr\u00e4sentationsstrukturen, Master\u2019s thesis, University of Bonn (2008), http:\/\/naproche.net\/downloads.shtml"},{"key":"11_CR7","unstructured":"Fuchs, N.E., H\u00f6fler, S., Kaljurand, K., Rinaldi, F., Schneider, G.: Attempto Controlled English: A Knowledge Representation Language Readable by Humans and Machines"},{"key":"11_CR8","unstructured":"Hardy, G.H., Wright, E.M.: An Introduction to the Theory of Numbers, 4th edn. (1960)"},{"key":"11_CR9","volume-title":"From Discourse to Logic: Introduction to Model-theoretic Semantics of Natural Language","author":"H. Kamp","year":"1993","unstructured":"Kamp, H., Reyle, U.: From Discourse to Logic: Introduction to Model-theoretic Semantics of Natural Language. Kluwer Academic Publisher, Dordrecht (1993)"},{"key":"11_CR10","unstructured":"Kolev, N.: Generating Proof Representation Structures for the Project Naproche, Magister thesis, University of Bonn (2008), http:\/\/naproche.net\/downloads.shtml"},{"key":"11_CR11","unstructured":"K\u00fchlwein, D.: A calculus for Proof Representation Structures, Diploma thesis, University of Bonn (2008), http:\/\/naproche.net\/downloads.shtml"},{"key":"11_CR12","unstructured":"Landau, E.: Grundlagen der Analysis, 3rd edn. (1960)"},{"key":"11_CR13","unstructured":"Matuszewski, R., Rudnicki, P.: Mizar: the first 30 years. Mechanized Mathematics and Its Applications\u00a04(2005) (2005)"},{"key":"11_CR14","doi-asserted-by":"crossref","unstructured":"Sutcliffe, G.: System Description: System on TPTP. In: CADE, pp. 406\u2013410 (2000)","DOI":"10.1007\/10721959_31"},{"key":"11_CR15","unstructured":"Texmacs Editor website: http:\/\/www.texmacs.org\/"},{"key":"11_CR16","unstructured":"VeriMathDoc website: http:\/\/www.ags.uni-sb.de\/~afiedler\/verimathdoc\/"},{"key":"11_CR17","unstructured":"Zinn, C.: Understanding Informal Mathematical Discourse, PhD thesis at the University of Erlangen (2004), http:\/\/citeseer.ist.psu.edu\/233023.html"}],"container-title":["Lecture Notes in Computer Science","Controlled Natural Language"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-14418-9_11.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T02:52:27Z","timestamp":1606186347000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-14418-9_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642144172","9783642144189"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-14418-9_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010]]}}}