{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,3]],"date-time":"2022-04-03T11:47:05Z","timestamp":1648986425521},"reference-count":56,"publisher":"Elsevier","license":[{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1016\/b978-0-444-51624-4.50008-3","type":"book-chapter","created":{"date-parts":[[2014,12,9]],"date-time":"2014-12-09T14:00:34Z","timestamp":1418133634000},"page":"343-396","source":"Crossref","is-referenced-by-count":2,"title":["Computerising Mathematical Text"],"prefix":"10.1016","author":[{"given":"Fairouz","family":"Kamareddine","sequence":"first","affiliation":[]},{"given":"Joe","family":"Wells","sequence":"additional","affiliation":[]},{"given":"Christoph","family":"Zengler","sequence":"additional","affiliation":[]},{"given":"Henk","family":"Barendregt","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/B978-0-444-51624-4.50008-3_bb0010","series-title":"Objectives of openmath","author":"Abbott","year":"1996"},{"issue":"3","key":"10.1016\/B978-0-444-51624-4.50008-3_bb0015","doi-asserted-by":"crossref","first-page":"225","DOI":"10.1007\/s11786-010-0028-3","article-title":"Foreword to the special issue on authoring, digitalization and management of mathematical knowledge","volume":"3","author":"Autexier","year":"2010","journal-title":"Mathematics in Computer Science"},{"key":"10.1016\/B978-0-444-51624-4.50008-3_bb0020","series-title":"Lambda Calculus with Types","author":"Barendregt","year":"2013"},{"key":"10.1016\/B978-0-444-51624-4.50008-3_bb0025","series-title":"Towards an interactive mathematical proof mode","first-page":"25","author":"Barendregt","year":"2003"},{"key":"10.1016\/B978-0-444-51624-4.50008-3_bb0030","series-title":"CADE","first-page":"647","article-title":"The oyster-clam system","author":"Bundy","year":"1990"},{"key":"10.1016\/B978-0-444-51624-4.50008-3_bb0035","doi-asserted-by":"crossref","first-page":"481","DOI":"10.1007\/BF02124929","article-title":"Beitr\u00e4ge zur Begr\u00fcndung der transfiniten Mengenlehre (part 1)","volume":"46","author":"Cantor","year":"1895","journal-title":"Mathematische Annalen"},{"key":"10.1016\/B978-0-444-51624-4.50008-3_bb0040","doi-asserted-by":"crossref","first-page":"207","DOI":"10.1007\/BF01444205","article-title":"Beitr\u00e4ge zur Begr\u00fcndung der transfiniten Mengenlehre (part 2)","volume":"49","author":"Cantor","year":"1897","journal-title":"Mathematische Annalen"},{"key":"10.1016\/B978-0-444-51624-4.50008-3_bb0045","series-title":"Cours d\u2019Analyse de l\u2019\u00c9cole Royale Polytechnique","author":"Cauchy","year":"1821"},{"key":"10.1016\/B978-0-444-51624-4.50008-3_bb0050","series-title":"Implementing Mathematics with the Nuprl Proof Development System","author":"Constable","year":"1986"},{"key":"10.1016\/B978-0-444-51624-4.50008-3_bb0055","series-title":"Proof and Computation","first-page":"109","article-title":"Using reflection to explain and enhance type theory","author":"Constable","year":"1995"},{"key":"10.1016\/B978-0-444-51624-4.50008-3_bb0060","series-title":"Workshop on Programming Logic","article-title":"The mathematical vernacular, a language for mathematics with typed sets","author":"de Bruijn","year":"1987"},{"key":"10.1016\/B978-0-444-51624-4.50008-3_bb0065","series-title":"Stetigkeit und irrationale Zahlen","author":"Dedekind","year":"1872"},{"key":"10.1016\/B978-0-444-51624-4.50008-3_bb0070","series-title":"Begriffsschrift: eine der arithmetischen nachgebildete Formelsprache des reinen Denkens","author":"Frege","year":"1879"},{"key":"10.1016\/B978-0-444-51624-4.50008-3_bb0075","series-title":"Grundgesetze der Arithmetik","author":"Frege","year":"1893"},{"key":"10.1016\/B978-0-444-51624-4.50008-3_bb0080","series-title":"Grundgesetze der Arithmetik","author":"Frege","year":"1903"},{"key":"10.1016\/B978-0-444-51624-4.50008-3_rf0085","series-title":"A Compendium of Continuous Lattices","author":"Gierz","year":"1980"},{"key":"10.1016\/B978-0-444-51624-4.50008-3_bb0090","series-title":"Introduction to HOL \u2013 A theorem, proving environment for higher order logic","author":"Gordon","year":"1993"},{"key":"10.1016\/B978-0-444-51624-4.50008-3_bb0095","series-title":"The 13 Books of Euclid\u2019s Elements","author":"Heath","year":"1956"},{"issue":"3","key":"10.1016\/B978-0-444-51624-4.50008-3_bb0100","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1023\/B:JLLI.0000028393.47593.b8","article-title":"A refinement of de Bruijn\u2019s formal language of mathematics","volume":"13","author":"Kamareddine","year":"2004","journal-title":"J. Logic Lang. Inform."},{"key":"10.1016\/B978-0-444-51624-4.50008-3_bb0105","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1016\/j.entcs.2008.03.063","article-title":"Computerizing mathematical text with mathlang","volume":"205","author":"Kamareddine","year":"2008","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"10.1016\/B978-0-444-51624-4.50008-3_bb0110","series-title":"A Modern Perspective on Type Theory from Its Origins Until Today","author":"Kamareddine","year":"2004"},{"key":"10.1016\/B978-0-444-51624-4.50008-3_bb0115","first-page":"160","article-title":"Flexible encoding of mathematics on the computer","author":"Kamareddine","year":"2004"},{"key":"10.1016\/B978-0-444-51624-4.50008-3_bb0120","series-title":"Proc. [MKMNET] Mathematical Knowledge Management Symposium","first-page":"138","article-title":"Mathlang: Experience-driven development of a new mathematical language","author":"Kamareddine","year":"2004"},{"key":"10.1016\/B978-0-444-51624-4.50008-3_bb0125","first-page":"217","article-title":"Toward an object-oriented structure for mathematical text","author":"Kamareddine","year":"2006"},{"key":"10.1016\/B978-0-444-51624-4.50008-3_bb0130","series-title":"Restoring natural language as a computerised mathematics input method","first-page":"280","author":"Kamareddine","year":"2007"},{"key":"10.1016\/B978-0-444-51624-4.50008-3_bb0135","series-title":"From Insight to Proof: Festschrift in Honour of Andrzej Trybulec","first-page":"95","article-title":"Gradual computerisation\/formalisation of mathematical texts into Mizar","author":"Kamareddine","year":"2007"},{"key":"10.1016\/B978-0-444-51624-4.50008-3_bb0140","series-title":"Narrative structure of mathematical texts","first-page":"296","author":"Kamareddine","year":"2007"},{"key":"10.1016\/B978-0-444-51624-4.50008-3_bb0145","series-title":"Thirty Five Years of Automating Mathematics","year":"2003"},{"key":"10.1016\/B978-0-444-51624-4.50008-3_bb0150","first-page":"124","article-title":"Capturing abstract matrices from paper","author":"Kanahori","year":"2006"},{"key":"10.1016\/B978-0-444-51624-4.50008-3_bb0155","series-title":"An Open Markup Format for Mathematical Documents, OMDoc (Version 1.2)","author":"Kohlhase","year":"2006"},{"key":"10.1016\/B978-0-444-51624-4.50008-3_bb0160","series-title":"A Partial Translation Path from MathLang to Isabelle","author":"Lamar","year":"2011"},{"key":"10.1016\/B978-0-444-51624-4.50008-3_bb0165","series-title":"Grundlagen der Analysis","author":"Landau","year":"1930"},{"key":"10.1016\/B978-0-444-51624-4.50008-3_bb0170","series-title":"Foundations of Analysis","author":"Landau","year":"1951"},{"key":"10.1016\/B978-0-444-51624-4.50008-3_bb0175","series-title":"Mathematical Documents Faithfully Computerised: the Grammatical and Text & Symbol Aspects of the MathLang Framework","author":"Maarek","year":"2007"},{"key":"10.1016\/B978-0-444-51624-4.50008-3_bb0180","series-title":"Towards Mechanized Mathematical Assistants (Calculemus 2007 and MKM 2007 Joint Proceedings)","year":"2007"},{"key":"10.1016\/B978-0-444-51624-4.50008-3_rf0185","series-title":"Selected Papers on Automath","author":"Nederpelt","year":"1994"},{"key":"10.1016\/B978-0-444-51624-4.50008-3_bb0190","series-title":"Weak Type Theory: a formal language for mathematics","author":"Nederpelt","year":"2002"},{"key":"10.1016\/B978-0-444-51624-4.50008-3_bb0195","series-title":"Isabelle\/HOL \u2014 A Proof Assistant for Higher-Order Logic","author":"Nipkow","year":"2002"},{"key":"10.1016\/B978-0-444-51624-4.50008-3_bb0200","series-title":"\u00c1rithmetices Principia, Nova Methodo Exposita","author":"Peano","year":"1889"},{"key":"10.1016\/B978-0-444-51624-4.50008-3_bb0205","series-title":"Gradual Computerisation and verification of Mathematics: MathLang\u2019s Path into Mizar","author":"Retel","year":"2009"},{"key":"10.1016\/B978-0-444-51624-4.50008-3_bb0210","article-title":"An overview of the Mizar project","author":"Rudnicki","year":"1992"},{"key":"10.1016\/B978-0-444-51624-4.50008-3_bb0215","series-title":"The ellipsis in mathematical documents","author":"Sexton","year":"2006"},{"key":"10.1016\/B978-0-444-51624-4.50008-3_bb0220","series-title":"CADE","first-page":"144","article-title":"Proof development with omega","author":"Siekmann","year":"2002"},{"key":"10.1016\/B978-0-444-51624-4.50008-3_bb0225","series-title":"Proof development with \u03a9mega: The irrationality of 2","first-page":"271","author":"Siekmann","year":"2003"},{"key":"10.1016\/B978-0-444-51624-4.50008-3_bb0230","series-title":"The coq proof assistant reference manual","article-title":"Coq Development Team","year":"1999"},{"key":"10.1016\/B978-0-444-51624-4.50008-3_bb0235","series-title":"Checking Landau\u2019s \u201cGrundlagen\u201d in the AUTOMATH System","author":"van Benthem Jutting","year":"1977"},{"key":"10.1016\/B978-0-444-51624-4.50008-3_bb0240","series-title":"Checking Landau\u2019s \u201cGrundlagen\u201d in the AUTOMATH system","author":"van Benthem Jutting","year":"1977"},{"issue":"1","key":"10.1016\/B978-0-444-51624-4.50008-3_bb0245","doi-asserted-by":"crossref","first-page":"24","DOI":"10.1145\/980175.980186","article-title":"GNU TeXmacs","volume":"38","author":"van der Hoeven","year":"2004","journal-title":"SIGSAM Bulletin"},{"key":"10.1016\/B978-0-444-51624-4.50008-3_bb0250","series-title":"From Frege to G\u00f6del: A Source Book in Mathematical Logic, 1879\u20131931","author":"van Heijenoort","year":"1967"},{"key":"10.1016\/B978-0-444-51624-4.50008-3_bb0255","series-title":"W3C. Mathematical markup language (MathML) version 2.0","year":"2003"},{"key":"10.1016\/B978-0-444-51624-4.50008-3_bb0260","series-title":"WC3. RDF Primer","year":"2004"},{"key":"10.1016\/B978-0-444-51624-4.50008-3_bb0265","series-title":"WC3. XQuery 1.0 and XPath 2.0 data model (XDM)","year":"2007"},{"key":"10.1016\/B978-0-444-51624-4.50008-3_bb0270","series-title":"Principia Mathematica","author":"Whitehead","year":"1910"},{"key":"10.1016\/B978-0-444-51624-4.50008-3_bb0275","series-title":"The Seventeen Provers of the World, foreword by Dana S. Scott","year":"2006"},{"key":"10.1016\/B978-0-444-51624-4.50008-3_bb0280","series-title":"Research report","author":"Zengler","year":"2008"},{"key":"10.1016\/B978-0-444-51624-4.50008-3_bb0285","doi-asserted-by":"crossref","first-page":"261","DOI":"10.1007\/BF01449999","article-title":"Untersuchungen \u00fcber die Grundlagen der Mengenlehre (part 1)","volume":"65","author":"Zermelo","year":"1908","journal-title":"Mathematische Annalen"}],"container-title":["Handbook of the History of Logic","Computational Logic"],"original-title":[],"link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:B9780444516244500083?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:B9780444516244500083?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2018,9,26]],"date-time":"2018-09-26T23:57:22Z","timestamp":1538006242000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/B9780444516244500083"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"references-count":56,"URL":"https:\/\/doi.org\/10.1016\/b978-0-444-51624-4.50008-3","relation":{},"ISSN":["1874-5857"],"issn-type":[{"value":"1874-5857","type":"print"}],"subject":[],"published":{"date-parts":[[2014]]}}}