{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,18]],"date-time":"2026-04-18T23:04:52Z","timestamp":1776553492567,"version":"3.51.2"},"publisher-location":"Berlin, Heidelberg","reference-count":32,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540710691","type":"print"},{"value":"9783540710707","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-71070-7_41","type":"book-chapter","created":{"date-parts":[[2008,8,29]],"date-time":"2008-08-29T09:56:30Z","timestamp":1220003790000},"page":"491-506","source":"Crossref","is-referenced-by-count":22,"title":["THF0 \u2013 The Core of the TPTP Language for Higher-Order Logic"],"prefix":"10.1007","author":[{"given":"Christoph","family":"Benzm\u00fcller","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Florian","family":"Rabe","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Geoff","family":"Sutcliffe","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"3","key":"41_CR1","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1007\/BF00252180","volume":"16","author":"P.B. Andrews","year":"1996","unstructured":"Andrews, P.B., Bishop, M., Issar, S., Nesmith, D., Pfenning, F., Xi, H.: TPS: A Theorem-Proving System for Classical Type Theory. Journal of Automated Reasoning\u00a016(3), 321\u2013353 (1996)","journal-title":"Journal of Automated Reasoning"},{"key":"41_CR2","unstructured":"Beeson, M.: Otter-lambda, a Theorem-prover with Untyped Lambda-unification. In: Sutcliffe, G., Schulz, S., Tammet, T. (eds.) Proceedings of the Workshop on Empirically Successful First Order Reasoning (2004)"},{"key":"41_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"66","DOI":"10.1007\/11541868_5","volume-title":"Theorem Proving in Higher Order Logics","author":"C. Benzm\u00fcller","year":"2005","unstructured":"Benzm\u00fcller, C., Brown, C.: A Structured Set of Higher-Order Problems. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol.\u00a03603, pp. 66\u201381. Springer, Heidelberg (2005)"},{"issue":"4","key":"41_CR4","doi-asserted-by":"publisher","first-page":"1027","DOI":"10.2178\/jsl\/1102022211","volume":"69","author":"C. Benzm\u00fcller","year":"2004","unstructured":"Benzm\u00fcller, C., Brown, C., Kohlhase, M.: Higher-order Semantics and Extensionality. Journal of Symbolic Logic\u00a069(4), 1027\u20131088 (2004)","journal-title":"Journal of Symbolic Logic"},{"key":"41_CR5","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1007\/BFb0054256","volume-title":"Automated Deduction - CADE-15","author":"C. Benzm\u00fcller","year":"1998","unstructured":"Benzm\u00fcller, C., Kohlhase, M.: LEO - A Higher-Order Theorem Prover. In: Kirchner, C., Kirchner, H. (eds.) CADE 1998. LNCS (LNAI), vol.\u00a01421, pp. 139\u2013143. Springer, Heidelberg (1998)"},{"key":"41_CR6","unstructured":"Benzm\u00fcller, C., Paulson, L.: Exploring Properties of Normal Multimodal Logics in Simple Type Theory with LEO-II. In: Benzm\u00fcller, C., Brown, C., Siekmann, J., Statman, R. (eds.) Festschrift in Honour of Peter B. Andrews on his 70th Birthday. IfCoLog (to appear 2007)"},{"key":"41_CR7","doi-asserted-by":"crossref","unstructured":"Benzm\u00fcller, C., Sorge, V., Jamnik, M., Kerber, M.: Combined Reasoning by Automated Cooperation. Journal of Applied Logic (in print) (2008)","DOI":"10.1016\/j.jal.2007.06.003"},{"key":"41_CR8","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"Proceedings of the 4th International Joint Conference on Automated Reasoning (IJCAR 2008)","author":"C. Benzm\u00fcller","year":"2008","unstructured":"Benzm\u00fcller, C., Theiss, F., Paulson, L., Fietzke, A.: LEO-II - A Cooperative Automatic Theorem Prover for Higher-Order Logic. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) Proceedings of the 4th International Joint Conference on Automated Reasoning (IJCAR 2008). LNCS (LNAI), vol.\u00a05195. Springer, Heidelberg (2008)"},{"key":"41_CR9","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. Journal of Symbolic Logic\u00a05, 56\u201368 (1940)","journal-title":"Journal of Symbolic Logic"},{"key":"41_CR10","volume-title":"Combinatory Logic I","author":"H.B. Curry","year":"1958","unstructured":"Curry, H.B., Feys, R.: Combinatory Logic I. North Holland, Amsterdam (1958)"},{"key":"41_CR11","unstructured":"Frege, F.: Grundgesetze der Arithmetik. Jena (1893) (1903)"},{"key":"41_CR12","unstructured":"Godefroid, P.: Software Model Checking: the VeriSoft Approach. Technical Report Technical Memorandum ITD-03-44189G, Bell Labs, Lisle, USA (2003)"},{"key":"41_CR13","volume-title":"Introduction to HOL, a Theorem Proving Environment for Higher Order Logic","author":"M. Gordon","year":"1993","unstructured":"Gordon, M., Melham, T.: Introduction to HOL, a Theorem Proving Environment for Higher Order Logic. Cambridge University Press, Cambridge (1993)"},{"issue":"1","key":"41_CR14","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. Journal of the ACM\u00a040(1), 143\u2013184 (1993)","journal-title":"Journal of the ACM"},{"key":"41_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/BFb0031814","volume-title":"Formal Methods in Computer-Aided Design","author":"J. Harrison","year":"1996","unstructured":"Harrison, J.: HOL Light: A Tutorial Introduction. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol.\u00a01166, pp. 265\u2013269. Springer, Heidelberg (1996)"},{"key":"41_CR16","doi-asserted-by":"publisher","first-page":"81","DOI":"10.2307\/2266967","volume":"15","author":"L. Henkin","year":"1950","unstructured":"Henkin, L.: Completeness in the Theory of Types. Journal of Symbolic Logic\u00a015, 81\u201391 (1950)","journal-title":"Journal of Symbolic Logic"},{"key":"41_CR17","first-page":"479","volume-title":"H B Curry, Essays on Combinatory Logic, Lambda Calculus and Formalism","author":"W. Howard","year":"1980","unstructured":"Howard, W.: The Formulas-as-types Notion of Construction. In: Seldin, J., Hindley, J. (eds.) H B Curry, Essays on Combinatory Logic, Lambda Calculus and Formalism, pp. 479\u2013490. Academic Press, London (1980)"},{"key":"41_CR18","first-page":"127","volume-title":"Twenty-Five Years of Constructive Type Theory","author":"P. Martin-L\u00f6f","year":"1973","unstructured":"Martin-L\u00f6f, P.: An Intuitionistic Theory of Types. In: Sambin, G., Smith, J. (eds.) Twenty-Five Years of Constructive Type Theory, pp. 127\u2013172. Oxford University Press, Oxford (1973)"},{"key":"41_CR19","unstructured":"Matuszek, C., Cabral, J., Witbrock, M., DeOliveira, J.: An Introduction to the Syntax and Content of Cyc. In: Baral, C. (ed.) Proceedings of the 2006 AAAI Spring Symposium on Formalizing and Compiling Background Knowledge and Its Applications to Knowledge Representation and Question Answering, pp. 44\u201349 (2006)"},{"key":"41_CR20","doi-asserted-by":"crossref","unstructured":"Niles, I., Pease, A.: Towards A Standard Upper Ontology. In: Welty, C., Smith, B. (eds.) Proceedings of the 2nd International Conference on Formal Ontology in Information Systems, pp. 2\u20139 (2001)","DOI":"10.1145\/505168.505170"},{"key":"41_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.T.: Isabelle\/HOL. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"41_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"411","DOI":"10.1007\/3-540-61474-5_91","volume-title":"Computer Aided Verification","author":"S. Owre","year":"1996","unstructured":"Owre, S., Rajan, S., Rushby, J.M., Shankar, N., Srivas, M.: PVS: Combining Specification, Proof Checking, and Model Checking. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102, pp. 411\u2013414. Springer, Heidelberg (1996)"},{"key":"41_CR23","series-title":"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.\u00a01632, pp. 202\u2013206. Springer, Heidelberg (1999)"},{"key":"41_CR24","unstructured":"Rudnicki, P.: An Overview of the Mizar Project. In: Proceedings of the 1992 Workshop on Types for Proofs and Programs, pp. 311\u2013332 (1992)"},{"issue":"4","key":"41_CR25","doi-asserted-by":"publisher","first-page":"533","DOI":"10.1016\/j.jal.2005.10.008","volume":"4","author":"J. Siekmann","year":"2006","unstructured":"Siekmann, J., Benzm\u00fcller, C., Autexier, S.: Computer supported mathematics with omega. Journal of Applied Logic\u00a04(4), 533\u2013559 (2006)","journal-title":"Journal of Applied Logic"},{"key":"41_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1007\/978-3-540-74510-5_4","volume-title":"Computer Science \u2013 Theory and Applications","author":"G. Sutcliffe","year":"2007","unstructured":"Sutcliffe, G.: TPTP, TSTP, CASC, etc. In: Diekert, V., Volkov, M.V., Voronkov, A. (eds.) CSR 2007. LNCS, vol.\u00a04649, pp. 7\u201323. Springer, Heidelberg (2007)"},{"key":"41_CR27","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/11814771_7","volume-title":"Automated Reasoning","author":"G. Sutcliffe","year":"2006","unstructured":"Sutcliffe, G., Schulz, S., Claessen, K., Gelder, A.V.: Using the TPTP Language for Writing Derivations and Finite Interpretations. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol.\u00a04130, pp. 67\u201381. Springer, Heidelberg (2006)"},{"issue":"1","key":"41_CR28","first-page":"35","volume":"19","author":"G. Sutcliffe","year":"2006","unstructured":"Sutcliffe, G., Suttner, C.: The State of CASC. AI Communications\u00a019(1), 35\u201348 (2006)","journal-title":"AI Communications"},{"issue":"2","key":"41_CR29","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1023\/A:1005806324129","volume":"21","author":"G. Sutcliffe","year":"1998","unstructured":"Sutcliffe, G., Suttner, C.B.: The TPTP Problem Library: CNF Release v1.2.1. Journal of Automated Reasoning\u00a021(2), 177\u2013203 (1998)","journal-title":"Journal of Automated Reasoning"},{"key":"41_CR30","series-title":"Frontiers in Artificial Intelligence and Applications","first-page":"201","volume-title":"Distributed Constraint Problem Solving and Reasoning in Multi-Agent Systems","author":"G. Sutcliffe","year":"2004","unstructured":"Sutcliffe, G., Zimmer, J., Schulz, S.: TSTP Data-Exchange Formats for Automated Theorem Proving Tools. In: Zhang, W., Sorge, V. (eds.) Distributed Constraint Problem Solving and Reasoning in Multi-Agent Systems. Frontiers in Artificial Intelligence and Applications, vol.\u00a0112, pp. 201\u2013215. IOS Press, Amsterdam (2004)"},{"key":"41_CR31","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"156","DOI":"10.1007\/11814771_15","volume-title":"Automated Reasoning","author":"A.V. Gelder","year":"2006","unstructured":"Gelder, A.V., Sutcliffe, G.: Extending the TPTP Language to Higher-Order Logic with Automated Parser Generation. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol.\u00a04130, pp. 156\u2013161. Springer, Heidelberg (2006)"},{"key":"41_CR32","doi-asserted-by":"crossref","first-page":"29","DOI":"10.4064\/fm-16-1-29-47","volume":"16","author":"E. Zermelo","year":"1930","unstructured":"Zermelo, E.: \u00dcber Grenzzahlen und Mengenbereiche. Fundamenta Mathematicae\u00a016, 29\u201347 (1930)","journal-title":"Fundamenta Mathematicae"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-71070-7_41.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,3]],"date-time":"2021-05-03T04:36:35Z","timestamp":1620016595000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-71070-7_41"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540710691","9783540710707"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-71070-7_41","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[]}}