{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T11:42:14Z","timestamp":1743075734346,"version":"3.40.3"},"publisher-location":"Cham","reference-count":22,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319206141"},{"type":"electronic","value":"9783319206158"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-20615-8_11","type":"book-chapter","created":{"date-parts":[[2015,6,22]],"date-time":"2015-06-22T15:31:23Z","timestamp":1434987083000},"page":"171-186","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Formal Logic Definitions for Interchange Languages"],"prefix":"10.1007","author":[{"given":"Fulya","family":"Horozal","sequence":"first","affiliation":[]},{"given":"Florian","family":"Rabe","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,6,23]]},"reference":[{"key":"11_CR1","unstructured":"Ausbrooks, R., Buswell, S., Carlisle, D., Dalmas, S., Devitt, S., Diaz, A., Froumentin, M., Hunter, R., Ion, P., Kohlhase, M., Miner, R., Poppelier, N., Smith, B., Soiffer, N., Sutor, R., Watt, S.: Mathematical Markup Language (MathML) Version 2.0 (2nd edn.) (2003). See http:\/\/www.w3.org\/TR\/MathML2"},{"key":"11_CR2","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"491","DOI":"10.1007\/978-3-540-71070-7_41","volume-title":"Automated Reasoning","author":"CE Benzm\u00fcller","year":"2008","unstructured":"Benzm\u00fcller, C.E., Rabe, F., Sutcliffe, G.: THF0 \u2013 the core of the TPTP language for higher-order logic. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 491\u2013506. Springer, Heidelberg (2008)"},{"key":"11_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"414","DOI":"10.1007\/978-3-642-38574-2_29","volume-title":"Automated Deduction \u2013 CADE-24","author":"JC Blanchette","year":"2013","unstructured":"Blanchette, J.C., Paskevich, A.: TFF1: the TPTP typed first-order form with rank-1 polymorphism. In: Bonacina, M.P. (ed.) CADE 2013. LNCS, vol. 7898, pp. 414\u2013420. Springer, Heidelberg (2013)"},{"key":"11_CR4","unstructured":"Buswell, S., Caprotti, O., Carlisle, D., Dewar, M., Gaetano, M., Kohlhase, M.: The Open Math Standard, Version 2.0. Technical report, The Open Math Society (2004). See http:\/\/www.openmath.org\/standard\/om20"},{"issue":"1","key":"11_CR5","doi-asserted-by":"publisher","first-page":"56","DOI":"10.2307\/2266170","volume":"5","author":"A Church","year":"1940","unstructured":"Church, A.: A formulation of the simple theory of types. J. Symbolic Logic 5(1), 56\u201368 (1940)","journal-title":"J. Symbolic Logic"},{"key":"11_CR6","first-page":"467","volume-title":"Conference on Automated Deduction","author":"W Farmer","year":"1992","unstructured":"Farmer, W., Guttman, J., Thayer, F.: Little theories. In: Kapur, D. (ed.) Conference on Automated Deduction, pp. 467\u2013581. Saratoga Spings, NY (1992)"},{"key":"11_CR7","first-page":"191","volume-title":"Introduction to HOL, Part III","author":"M Gordon","year":"1993","unstructured":"Gordon, M., Pitts, A.: The HOL logic. In: Gordon, M., Melham, T. (eds.) Introduction to HOL, Part III, pp. 191\u2013232. Cambridge University Press, New York (1993)"},{"issue":"1","key":"11_CR8","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1145\/138027.138060","volume":"40","author":"R Harper","year":"1993","unstructured":"Harper, R., Honsell, F., Plotkin, G.: A framework for defining logics. J. Assoc. Comput. Mach. 40(1), 143\u2013184 (1993)","journal-title":"J. Assoc. Comput. Mach."},{"key":"11_CR9","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1016\/0168-0072(94)90009-4","volume":"67","author":"R Harper","year":"1994","unstructured":"Harper, R., Sannella, D., Tarlecki, A.: Structured presentations and logic representations. Ann. Pure Appl. Logic 67, 113\u2013160 (1994)","journal-title":"Ann. Pure Appl. Logic"},{"key":"11_CR10","unstructured":"Horozal, F.: A Framework for Defining Declarative Languages. Ph.D. thesis. Jacobs University Bremen (2014)"},{"key":"11_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1007\/978-3-642-31374-5_5","volume-title":"Intelligent Computer Mathematics","author":"F Horozal","year":"2012","unstructured":"Horozal, F., Kohlhase, M., Rabe, F.: Extending MKM formats at the statement level. In: Campbell, J.A., Jeuring, J., Carette, J., Dos Reis, G., Sojka, P., Wenzel, M., Sorge, V. (eds.) CICM 2012. LNCS, vol. 7362, pp. 65\u201380. Springer, Heidelberg (2012)"},{"key":"11_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"312","DOI":"10.1007\/978-3-319-08434-3_23","volume-title":"Intelligent Computer Mathematics","author":"F Horozal","year":"2014","unstructured":"Horozal, F., Rabe, F., Kohlhase, M.: Flexary operators for formalized mathematics. In: Watt, S.M., Davenport, J.H., Sexton, A.P., Sojka, P., Urban, J. (eds.) CICM 2014. LNCS, vol. 8543, pp. 312\u2013327. Springer, Heidelberg (2014)"},{"key":"11_CR13","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","DOI":"10.1007\/11826095","volume-title":"OMDoc: An Open Markup Format for Mathematical Documents (Version 1.2)","author":"M Kohlhase","year":"2006","unstructured":"Kohlhase, M.: OMDoc: An Open Markup Format for Mathematical Documents (Version 1.2). Lecture Notes in Artificial Intelligence, vol. 4180. Springer, Heidelberg (2006)"},{"key":"11_CR14","unstructured":"Kohlhase, M., Mossakowski, T., Rabe, F.: The LATIN Project (2009). see https:\/\/trac.omdoc.org\/LATIN\/"},{"key":"11_CR15","volume-title":"Intelligent Computer Mathematics","author":"E Kotelnikov","year":"2015","unstructured":"Kotelnikov, E., Kovacs, L., Voronkov, A.: A first class boolean sort in first-order theorem proving and TPTP. In: Kerber, M., Carette, J., Kaliszyk, C., Rabe, F., Sorge, V. (eds.) Intelligent Computer Mathematics. Springer, Stockholm (2015)"},{"key":"11_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0030541","volume-title":"Isabelle: A Generic Theorem Prover","author":"L Paulson","year":"1994","unstructured":"Paulson, L.: Isabelle: A Generic Theorem Prover. Lecture Notes in Computer Science, vol. 828. Springer, Heidelberg (1994)"},{"key":"11_CR17","doi-asserted-by":"publisher","first-page":"1063","DOI":"10.1016\/B978-044450813-3\/50019-9","volume-title":"Handbook of Automated Reasoning","author":"F Pfenning","year":"2001","unstructured":"Pfenning, F.: Logical frameworks. In: Robinson, J., Voronkov, A. (eds.) Handbook of Automated Reasoning, pp. 1063\u20131147. Elsevier, The Netherlands (2001)"},{"key":"11_CR18","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"202","DOI":"10.1007\/3-540-48660-7_14","volume-title":"Automated Deduction - CADE-16","author":"F Pfenning","year":"1999","unstructured":"Pfenning, F., Sch\u00fcrmann, C.: System description: Twelf - a meta-logical framework for deductive systems. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol. 1632, pp. 202\u2013206. Springer, Heidelberg (1999)"},{"key":"11_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"339","DOI":"10.1007\/978-3-642-39320-4_25","volume-title":"Intelligent Computer Mathematics","author":"F Rabe","year":"2013","unstructured":"Rabe, F.: The MMT API: a generic MKM system. In: Carette, J., Aspinall, D., Lange, C., Sojka, P., Windsteiger, W. (eds.) CICM 2013. LNCS, vol. 7961, pp. 339\u2013343. Springer, Heidelberg (2013)"},{"issue":"1","key":"11_CR20","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.ic.2013.06.001","volume":"230","author":"F Rabe","year":"2013","unstructured":"Rabe, F., Kohlhase, M.: A scalable module system. Inf. Comput. 230(1), 1\u201354 (2013)","journal-title":"Inf. Comput."},{"issue":"4","key":"11_CR21","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. J. Autom. Reasoning 43(4), 337\u2013362 (2009)","journal-title":"J. Autom. Reasoning"},{"key":"11_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"406","DOI":"10.1007\/978-3-642-28717-6_32","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"G Sutcliffe","year":"2012","unstructured":"Sutcliffe, G., Schulz, S., Claessen, K., Baumgartner, P.: The TPTP typed first-order form with arithmetic. In: Bj\u00f8rner, N., Voronkov, A. (eds.) LPAR-18 2012. LNCS, vol. 7180, pp. 406\u2013419. Springer, Heidelberg (2012)"}],"container-title":["Lecture Notes in Computer Science","Intelligent Computer Mathematics"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-20615-8_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,20]],"date-time":"2023-01-20T15:22:17Z","timestamp":1674228137000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-20615-8_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319206141","9783319206158"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-20615-8_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"23 June 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}