{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,18]],"date-time":"2026-04-18T22:51:18Z","timestamp":1776552678585,"version":"3.51.2"},"publisher-location":"Cham","reference-count":30,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319084336","type":"print"},{"value":"9783319084343","type":"electronic"}],"license":[{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-08434-3_28","type":"book-chapter","created":{"date-parts":[[2014,7,1]],"date-time":"2014-07-01T03:14:35Z","timestamp":1404184475000},"page":"388-403","source":"Crossref","is-referenced-by-count":11,"title":["A Vernacular for Coherent Logic"],"prefix":"10.1007","author":[{"given":"Sana","family":"Stojanovi\u0107","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Julien","family":"Narboux","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marc","family":"Bezem","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Predrag","family":"Jani\u010di\u0107","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"28_CR1","doi-asserted-by":"crossref","unstructured":"Avigad, J., Dean, E., Mumma, J.: A Formal System for Euclid\u2019s Elements. The Review of Symbolic Logic (2009)","DOI":"10.1017\/S1755020309990098"},{"issue":"1835","key":"28_CR2","doi-asserted-by":"publisher","first-page":"2351","DOI":"10.1098\/rsta.2005.1650","volume":"363","author":"H. Barendregt","year":"2005","unstructured":"Barendregt, H., Wiedijk, F.: The Challenge of Computer Mathematics. Philosophical Transactions of the Royal Society\u00a0363(1835), 2351\u20132375 (2005)","journal-title":"Philosophical Transactions of the Royal Society"},{"key":"28_CR3","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1007\/11591191_18","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"M. Bezem","year":"2005","unstructured":"Bezem, M., Coquand, T.: Automating Coherent Logic. In: Sutcliffe, G., Voronkov, A. (eds.) LPAR 2005. LNCS (LNAI), vol.\u00a03835, pp. 246\u2013260. Springer, Heidelberg (2005)"},{"key":"28_CR4","doi-asserted-by":"crossref","unstructured":"Bezem, M., Hendriks, D.: On the Mechanization of the Proof of Hessenberg\u2019s Theorem in Coherent Logic. Journal of Automated Reasoning\u00a040(1) (2008)","DOI":"10.1007\/s10817-007-9086-x"},{"key":"28_CR5","doi-asserted-by":"crossref","unstructured":"Blanchette, J.C.: Redirecting Proofs by Contradiction. In: Blanchette, J.C., Urban, J. (eds.) Third International Workshop on Proof Exchange for Theorem Proving, PxTP 2013, Lake Placid, NY, USA, June 9-10. EPiC Series, vol.\u00a014, pp. 11\u201326. EasyChair (2013)","DOI":"10.29007\/wm8b"},{"issue":"1","key":"28_CR6","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1007\/s10817-013-9278-5","volume":"51","author":"J.C. Blanchette","year":"2013","unstructured":"Blanchette, J.C., B\u00f6hme, S., Paulson, L.C.: Extending Sledgehammer with SMT Solvers. Journal of Automated Reasoning\u00a051(1), 109\u2013128 (2013)","journal-title":"Journal of Automated Reasoning"},{"key":"28_CR7","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1007\/978-3-642-24364-6_2","volume-title":"Frontiers of Combining Systems","author":"J.C. Blanchette","year":"2011","unstructured":"Blanchette, J.C., Bulwahn, L., Nipkow, T.: Automatic Proof and Disproof in Isabelle\/HOL. In: Tinelli, C., Sofronie-Stokkermans, V. (eds.) FroCoS 2011. LNCS (LNAI), vol.\u00a06989, pp. 12\u201327. Springer, Heidelberg (2011)"},{"key":"28_CR8","first-page":"57","volume":"36","author":"A. Blass","year":"1998","unstructured":"Blass, A.: Topoi and Computation. Bulletin of the EATCS\u00a036, 57\u201365 (1998)","journal-title":"Bulletin of the EATCS"},{"key":"28_CR9","unstructured":"Boespflug, M., Carbonneaux, Q., Hermant, O.: The \u03bb\u03a0-calculus Modulo as a Universal Proof Language. In: Second Workshop on Proof Exchange for Theorem Proving (PxTP). CEUR Workshop Proceedings, vol.\u00a0878, pp. 28\u201343. CEUR-WS.org (2012)"},{"key":"28_CR10","unstructured":"de Bruijn, N.G.: The Mathematical Vernacular, a Language for Mathematics with Typed Sets. In: Dybjer, et al. (eds.) Proceedings of the Workshop on Programming Languages (1987)"},{"key":"28_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1007\/978-3-540-75292-9_14","volume-title":"Theoretical Aspects of Computing \u2013 ICTAC 2007","author":"J. Fisher","year":"2007","unstructured":"Fisher, J., Bezem, M.: Skolem Machines and Geometric Logic. In: Jones, C.B., Liu, Z., Woodcock, J. (eds.) ICTAC 2007. LNCS, vol.\u00a04711, pp. 201\u2013215. Springer, Heidelberg (2007)"},{"key":"28_CR12","unstructured":"Ganesalingam, M., Gowers, W.T.: A fully automatic problem solver with human-style output. CoRR, abs\/1309.4501 (2013)"},{"key":"28_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1007\/978-3-642-39634-2_7","volume-title":"Interactive Theorem Proving","author":"C. Kaliszyk","year":"2013","unstructured":"Kaliszyk, C., Krauss, A.: Scalable LCF-Style Proof Translation. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol.\u00a07998, pp. 51\u201366. Springer, Heidelberg (2013)"},{"key":"28_CR14","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1007\/978-3-642-38574-2_18","volume-title":"Automated Deduction \u2013 CADE-24","author":"C. Kaliszyk","year":"2013","unstructured":"Kaliszyk, C., Urban, J.: PRocH: Proof Reconstruction for HOL Light. In: Bonacina, M.P. (ed.) CADE-24. LNCS (LNAI), vol.\u00a07898, pp. 267\u2013274. Springer, Heidelberg (2013)"},{"key":"28_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/978-3-642-14052-5_22","volume-title":"Interactive Theorem Proving","author":"C. Keller","year":"2010","unstructured":"Keller, C., Werner, B.: Importing HOL Light into Coq. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol.\u00a06172, pp. 307\u2013322. Springer, Heidelberg (2010)"},{"key":"28_CR16","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/11826095_5","volume-title":"OMDoc \u2013 An Open Markup Format for Mathematical Documents [version 1.2]","author":"M. Kohlhase","year":"2006","unstructured":"Kohlhase, M.: An OMDoc primer. In: Kohlhase, M. (ed.) OMDoc \u2013 An Open Markup Format for Mathematical Documents [version 1.2]. LNCS (LNAI), vol.\u00a04180, pp. 33\u201334. Springer, Heidelberg (2006)"},{"issue":"3","key":"28_CR17","doi-asserted-by":"publisher","first-page":"76","DOI":"10.1145\/362084.362140","volume":"29","author":"D. Lee","year":"2000","unstructured":"Lee, D., Chu, W.W.: Comparative analysis of six xml schema languages. SIGMOD Record\u00a029(3), 76\u201387 (2000)","journal-title":"SIGMOD Record"},{"key":"28_CR18","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"298","DOI":"10.1007\/11814771_27","volume-title":"Automated Reasoning","author":"S. Obua","year":"2006","unstructured":"Obua, S., Skalberg, S.: Importing HOL into Isabelle\/HOL. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol.\u00a04130, pp. 298\u2013302. Springer, Heidelberg (2006)"},{"key":"28_CR19","unstructured":"Polonsky, A.: Proofs, Types and Lambda Calculus. PhD thesis, University of Bergen (2011)"},{"issue":"4","key":"28_CR20","doi-asserted-by":"publisher","first-page":"383","DOI":"10.1007\/BF00247436","volume":"3","author":"P. Rudnicki","year":"1987","unstructured":"Rudnicki, P.: Obvious inferences. Journal of Automated Reasoning\u00a03(4), 383\u2013393 (1987)","journal-title":"Journal of Automated Reasoning"},{"key":"28_CR21","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-69418-9","volume-title":"Metamathematische Methoden in der Geometrie","author":"W. Schwabh\u00e4user","year":"1983","unstructured":"Schwabh\u00e4user, W., Szmielew, W., Tarski, A.: Metamathematische Methoden in der Geometrie. Springer, Berlin (1983)"},{"key":"28_CR22","doi-asserted-by":"crossref","unstructured":"Smolka, S.J., Blanchette, J.C.: Robust, Semi-Intelligible Isabelle Proofs from ATP Proofs. In: Blanchette, J.C., Urban, J. (eds.) Third International Workshop on Proof Exchange for Theorem Proving, PxTP 2013. EPiC Series, vol.\u00a014, pp. 117\u2013132. EasyChair (2013)","DOI":"10.29007\/zbdb"},{"key":"28_CR23","unstructured":"Stojanovi\u0107, S., Narboux, J., Jani\u010di\u0107, P.: Synergy Between Interactive and Automated Theorem Proving in Formalization of Mathematical Knowledge: A Case Study of Tarski\u2019s Geometry (submitted for publication, 2014)"},{"key":"28_CR24","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1007\/978-3-642-25070-5_12","volume-title":"Automated Deduction in Geometry","author":"S. Stojanovi\u0107","year":"2011","unstructured":"Stojanovi\u0107, S., Pavlovi\u0107, V., Jani\u010di\u0107, P.: A Coherent Logic Based Geometry Theorem Prover Capable of Producing Formal and Readable Proofs. In: Schreck, P., Narboux, J., Richter-Gebert, J. (eds.) ADG 2010. LNCS (LNAI), vol.\u00a06877, pp. 201\u2013220. Springer, Heidelberg (2011)"},{"issue":"4","key":"28_CR25","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/s10817-009-9143-8","volume":"43","author":"G. Sutcliffe","year":"2009","unstructured":"Sutcliffe, G.: The TPTP Problem Library and Associated Infrastructure: The FOF and CNF Parts, v3.5.0. Journal of Automated Reasoning\u00a043(4), 337\u2013362 (2009)","journal-title":"Journal of Automated Reasoning"},{"key":"28_CR26","doi-asserted-by":"crossref","unstructured":"Tarski, A., Givant, S.: Tarski\u2019s system of geometry. The Bulletin of Symbolic Logic\u00a05(2) (June 1999)","DOI":"10.2307\/421089"},{"key":"28_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/3-540-48256-3_12","volume-title":"Theorem Proving in Higher Order Logics","author":"M. Wenzel","year":"1999","unstructured":"Wenzel, M.: Isar - A Generic Interpretative Approach to Readable Formal Proof Documents. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Th\u00e9ry, L. (eds.) TPHOLs 1999. LNCS, vol.\u00a01690, pp. 167\u2013183. Springer, Heidelberg (1999)"},{"key":"28_CR28","unstructured":"Wiedijk, F.: Mathematical Vernacular. Unpublished note (2000), http:\/\/www.cs.ru.nl\/~freek\/notes\/mv.pdf"},{"key":"28_CR29","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"The Seventeen Provers of the World","year":"2006","unstructured":"Wiedijk, F. (ed.): The Seventeen Provers of the World. LNCS (LNAI), vol.\u00a03600. Springer, Heidelberg (2006)"},{"key":"28_CR30","doi-asserted-by":"crossref","unstructured":"Wiedijk, F.: A Synthesis of the Procedural and Declarative Styles of Interactive Theorem Proving. Logical Methods in Computer Science\u00a08(1) (2012)","DOI":"10.2168\/LMCS-8(1:30)2012"}],"container-title":["Lecture Notes in Computer Science","Intelligent Computer Mathematics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-08434-3_28","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,3]],"date-time":"2025-05-03T15:44:53Z","timestamp":1746287093000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-08434-3_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319084336","9783319084343"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-08434-3_28","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014]]}}}