{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T02:40:30Z","timestamp":1767926430953,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642385735","type":"print"},{"value":"9783642385742","type":"electronic"}],"license":[{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-38574-2_29","type":"book-chapter","created":{"date-parts":[[2013,6,4]],"date-time":"2013-06-04T03:55:13Z","timestamp":1370318113000},"page":"414-420","source":"Crossref","is-referenced-by-count":28,"title":["TFF1: The TPTP Typed First-Order Form with Rank-1 Polymorphism"],"prefix":"10.1007","author":[{"given":"Jasmin Christian","family":"Blanchette","sequence":"first","affiliation":[]},{"given":"Andrei","family":"Paskevich","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"29_CR1","unstructured":"Barrett, C., Stump, A., Tinelli, C.: The SMT-LIB standard\u2014Version 2.0. In: Gupta, A., Kroening, D. (eds.) SMT 2010 (2010)"},{"key":"29_CR2","series-title":"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":"C. Benzm\u00fcller","year":"2008","unstructured":"Benzm\u00fcller, C., 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.\u00a05195, pp. 491\u2013506. Springer, Heidelberg (2008)"},{"key":"29_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"493","DOI":"10.1007\/978-3-642-36742-7_34","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J.C. Blanchette","year":"2013","unstructured":"Blanchette, J.C., B\u00f6hme, S., Popescu, A., Smallbone, N.: Encoding monomorphic and polymorphic types. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol.\u00a07795, pp. 493\u2013507. Springer, Heidelberg (2013)"},{"key":"29_CR4","doi-asserted-by":"crossref","unstructured":"Bobot, F., Conchon, S., Contejean, E., Lescuyer, S.: Implementing polymorphism in SMT solvers. In: Barrett, C., de Moura, L. (eds.) SMT 2008, pp. 1\u20135. ICPS, ACM (2008)","DOI":"10.1145\/1512464.1512466"},{"key":"29_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/978-3-642-24364-6_7","volume-title":"Frontiers of Combining Systems","author":"F. Bobot","year":"2011","unstructured":"Bobot, F., Paskevich, A.: Expressing polymorphic types in a many-sorted language. In: Tinelli, C., Sofronie-Stokkermans, V. (eds.) FroCoS 2011. LNCS, vol.\u00a06989, pp. 87\u2013102. Springer, Heidelberg (2011)"},{"key":"29_CR6","unstructured":"Bobot, F., Filli\u00e2tre, J.C., March\u00e9, C., Paskevich, A.: Why3: Shepherd your herd of provers. In: Leino, K.R.M., Moskal, M. (eds.) Boogie 2011, pp. 53\u201364 (2011)"},{"key":"29_CR7","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/978-3-540-73595-3_18","volume-title":"Automated Deduction \u2013 CADE-21","author":"J.F. Couchot","year":"2007","unstructured":"Couchot, J.F., Lescuyer, S.: Handling polymorphism in automated deduction. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol.\u00a04603, pp. 263\u2013278. Springer, Heidelberg (2007)"},{"key":"29_CR8","unstructured":"Kaliszyk, C., Urban, J.: Learning-assisted automated reasoning with Flyspeck (submitted)"},{"key":"29_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/978-3-540-74915-8_19","volume-title":"Computer Science Logic","author":"K. Korovin","year":"2007","unstructured":"Korovin, K., Voronkov, A.: Integrating linear arithmetic into superposition calculus. In: Duparc, J., Henzinger, T.A. (eds.) CSL 2007. LNCS, vol.\u00a04646, pp. 223\u2013237. Springer, Heidelberg (2007)"},{"key":"29_CR10","unstructured":"Kuncak, V.: Intermediate languages\u2014From birth to execution. In: Boogie 2011 (2011)"},{"key":"29_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"312","DOI":"10.1007\/978-3-642-12002-2_26","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K.R.M. Leino","year":"2010","unstructured":"Leino, K.R.M., R\u00fcmmer, P.: A polymorphic intermediate verification language: Design and logical encoding. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol.\u00a06015, pp. 312\u2013327. Springer, Heidelberg (2010)"},{"key":"29_CR12","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., Ternovska, E., Schulz, S. (eds.) IWIL 2010 (2010)"},{"key":"29_CR13","unstructured":"Prevosto, V., Waldmann, U.: SPASS+T. In: Sutcliffe, G., Schmidt, R., Schulz, S. (eds.) ESCoR 2006. CEUR Workshop Proceedings, vol.\u00a0192, pp. 18\u201333. CEUR-WS.org (2006)"},{"issue":"4","key":"29_CR14","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\u2014The FOF and CNF parts, v3.5.0. J. Autom. Reasoning\u00a043(4), 337\u2013362 (2009)","journal-title":"J. Autom. Reasoning"},{"key":"29_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-17511-4_1","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"G. Sutcliffe","year":"2010","unstructured":"Sutcliffe, G.: The TPTP world \u2013 infrastructure for automated reasoning. In: Clarke, E.M., Voronkov, A. (eds.) LPAR-16 2010. LNCS, vol.\u00a06355, pp. 1\u201312. Springer, Heidelberg (2010)"},{"issue":"1","key":"29_CR16","first-page":"1","volume":"3","author":"G. Sutcliffe","year":"2010","unstructured":"Sutcliffe, G., Benzm\u00fcller, C.: Automated reasoning in higher-order logic using the TPTP THF infrastructure. J. Formal. Reasoning\u00a03(1), 1\u201327 (2010)","journal-title":"J. Formal. Reasoning"},{"key":"29_CR17","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.\u00a07180, pp. 406\u2013419. Springer, Heidelberg (2012)"},{"key":"29_CR18","unstructured":"Voronkov, A.: Automated reasoning: Past story and new trends. In: Gottlob, G., Walsh, T. (eds.) IJCAI 2003, pp. 1607\u20131612. Morgan Kaufmann (2003)"},{"key":"29_CR19","unstructured":"Wand, D., Weidenbach, C.: Private communication (June 2012)"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE-24"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-38574-2_29","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T21:47:08Z","timestamp":1558302428000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-38574-2_29"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642385735","9783642385742"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-38574-2_29","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013]]}}}