{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,22]],"date-time":"2025-12-22T10:48:23Z","timestamp":1766400503202,"version":"3.44.0"},"publisher-location":"Cham","reference-count":38,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032041661","type":"print"},{"value":"9783032041678","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,9,15]],"date-time":"2025-09-15T00:00:00Z","timestamp":1757894400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,9,15]],"date-time":"2025-09-15T00:00:00Z","timestamp":1757894400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>Much of the current research and development in the field of automated reasoning builds on\u00a0the infrastructure provided by the TPTP World. The TPTP language for logical formulae is central to the far-reaching adoption of the TPTP World. This paper introduces the Dependently Typed higher-order Form (DHF) of the TPTP language. It takes advantage of already established binders in the syntax, and is thus a minimally intrusive extension to the Typed Higher-order Form (THF). A starting set of over 100 problems is provided to exhibit the usefulness and incite interest in DHF. Some tools that are already able to reason about problems in the DHF language are discussed.<\/jats:p>","DOI":"10.1007\/978-3-032-04167-8_16","type":"book-chapter","created":{"date-parts":[[2025,9,14]],"date-time":"2025-09-14T22:03:32Z","timestamp":1757887412000},"page":"287-305","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["The Dependently Typed Higher-Order Form for\u00a0the\u00a0TPTP World"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0006-2861-548X","authenticated-orcid":false,"given":"Daniel","family":"Ranalter","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8273-6059","authenticated-orcid":false,"given":"Cezary","family":"Kaliszyk","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3040-3655","authenticated-orcid":false,"given":"Florian","family":"Rabe","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9120-3927","authenticated-orcid":false,"given":"Geoff","family":"Sutcliffe","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,9,15]]},"reference":[{"key":"16_CR1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive Theorem Proving and Program Development: Coq\u2019Art: The Calculus of Inductive Constructions","author":"Y Bertot","year":"2004","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development: Coq\u2019Art: The Calculus of Inductive Constructions. Springer, Cham (2004)"},{"key":"16_CR2","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","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 (LNAI), vol. 7898, pp. 414\u2013420. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-38574-2_29"},{"key":"16_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1007\/978-3-642-03359-9_6","volume-title":"Theorem Proving in Higher Order Logics","author":"A Bove","year":"2009","unstructured":"Bove, A., Dybjer, P., Norell, U.: A brief overview of Agda \u2013 a functional language with dependent types. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 73\u201378. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-03359-9_6"},{"key":"16_CR4","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1007\/978-3-642-31365-3_11","volume-title":"Automated Reasoning","author":"CE Brown","year":"2012","unstructured":"Brown, C.E.: Satallax: an automatic higher-order prover. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS (LNAI), vol. 7364, pp. 111\u2013117. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31365-3_11"},{"key":"16_CR5","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"350","DOI":"10.1007\/978-3-031-10769-6_21","volume-title":"Automated Reasoning","author":"CE Brown","year":"2022","unstructured":"Brown, C.E., Kaliszyk, C.: Lash 1.0 (system description). In: Blanchette, J., Kov\u00e1cs, L., Pattinson, D. (eds.) Automated Reasoning. LNAI, vol. 13385, pp. 350\u2013358. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-10769-6_21"},{"issue":"2","key":"16_CR6","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. Symb. Log. 5(2), 56\u201368 (1940). https:\/\/doi.org\/10.2307\/2266170","journal-title":"J. Symb. Log."},{"key":"16_CR7","unstructured":"Constable, R., et al.: Implementing Mathematics with the Nuprl Development System. Prentice-Hall (1986)"},{"key":"16_CR8","unstructured":"Kaliszyk, C., Sutcliffe, G., Rabe, F.: TH1: the TPTP typed higher-order form with rank-1 polymorphism. In: Fontaine, P., Schulz, S., Urban, J. (eds.) Proceedings 5th Workshop on Practical Aspects of Automated Reasoning. CEUR Workshop Proceedings, vol.\u00a01635, pp. 41\u201355. CEUR-WS.org (2016). https:\/\/ceur-ws.org\/Vol-1635\/paper-05.pdf"},{"key":"16_CR9","doi-asserted-by":"publisher","unstructured":"de Moura, L., Ullrich, S.: The lean 4 theorem prover and programming language. In: Platzer, A., Sutcliffe, G. (eds.) CADE 2021. LNCS (LNAI), vol. 12699, pp. 625\u2013635. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-79876-5_37","DOI":"10.1007\/978-3-030-79876-5_37"},{"key":"16_CR10","doi-asserted-by":"crossref","unstructured":"M\u00fcller, D., Rabe, F.: Rapid prototyping formal systems in MMT: case studies. In: Miller, D., Scagnetto, I. (eds.) Logical Frameworks and Meta-languages: Theory and Practice, pp. 40\u201354 (2019)","DOI":"10.4204\/EPTCS.307.5"},{"key":"16_CR11","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"86","DOI":"10.1007\/978-3-031-63498-7_6","volume-title":"Automated Reasoning","author":"J Niederhauser","year":"2024","unstructured":"Niederhauser, J., Brown, C.E., Kaliszyk, C.: Tableaux for automated reasoning in dependently-typed higher-order logic. In: Benzm\u00fcller, C., Heule, M.J.H., Schmidt, R.A. (eds.) Automated Reasoning. LNAI, pp. 86\u2013104. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-63498-7_6"},{"key":"16_CR12","unstructured":"Owre, S., Shankar, N.: The formal semantics of PVS. Technical report. SRI-CSL-97-2, SRI International (1997)"},{"key":"16_CR13","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 \u2014 CADE-16","author":"F Pfenning","year":"1999","unstructured":"Pfenning, F., Sch\u00fcrmann, C.: System description: Twelf \u2014 a meta-logical framework for deductive systems. In: CADE 1999. LNCS (LNAI), vol. 1632, pp. 202\u2013206. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48660-7_14"},{"issue":"4","key":"16_CR14","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3234693","volume":"19","author":"F Rabe","year":"2018","unstructured":"Rabe, F.: A modular type reconstruction algorithm. ACM Trans. Comput. Log. 19(4), 1\u201343 (2018)","journal-title":"ACM Trans. Comput. Log."},{"key":"16_CR15","unstructured":"Rabe, F.: Model theory for dependently-typed higher-order logic (2024). Under review, see https:\/\/kwarc.info\/people\/frabe\/Research\/rabe_dholmodels_24.pdf"},{"key":"16_CR16","doi-asserted-by":"publisher","unstructured":"Ranalter, D., Brown, C.E., Kaliszyk, C.: Experiments with choice in dependently-typed higher-order logic. In: Bj\u00f8rner, N.S., Heule, M., Voronkov, A. (eds.) Proceedings 25th International Conference on Logic for Programming, Artificial Intelligence and Reasoning. EPiC Series in Computing, vol.\u00a0100, pp. 311\u2013320. EasyChair (2024). https:\/\/doi.org\/10.29007\/2V8H","DOI":"10.29007\/2V8H"},{"key":"16_CR17","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"438","DOI":"10.1007\/978-3-031-38499-8_25","volume-title":"Automated Deduction","author":"C Rothgang","year":"2023","unstructured":"Rothgang, C., Rabe, F., Benzm\u00fcller, C.: Theorem proving in dependently-typed higher-order logic. In: Pientka, B., Tinelli, C. (eds.) Automated Deduction. LNAI, vol. 14132, pp. 438\u2013455. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-38499-8_25"},{"key":"16_CR18","doi-asserted-by":"publisher","unstructured":"Rothgang, C., Rabe, F., Benzm\u00fcller, C.: Dependently-typed higher-order logic \u2013 extended preprint (2025). https:\/\/doi.org\/10.48550\/arXiv.2305.15382, under review","DOI":"10.48550\/arXiv.2305.15382"},{"issue":"9","key":"16_CR19","doi-asserted-by":"publisher","first-page":"709","DOI":"10.1109\/32.713327","volume":"24","author":"J Rushby","year":"1998","unstructured":"Rushby, J., Owre, S., Shankar, N.: Subtypes for specifications: predicate subtyping in PVS. IEEE Trans. Softw. Eng. 24(9), 709\u2013720 (1998). https:\/\/doi.org\/10.1109\/32.713327","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"6","key":"16_CR20","doi-asserted-by":"publisher","first-page":"775","DOI":"10.1007\/s10817-021-09588-x","volume":"65","author":"A Steen","year":"2021","unstructured":"Steen, A., Benzm\u00fcller, C.: Extensional higher-order paramodulation in Leo-III. J. Autom. Reason. 65(6), 775\u2013807 (2021). https:\/\/doi.org\/10.1007\/s10817-021-09588-x","journal-title":"J. Autom. Reason."},{"key":"16_CR21","unstructured":"Steen, A., Fuenmayor, D., Glei\u00dfner, T., Sutcliffe, G., Benzm\u00fcller, C.: Automated reasoning in non-classical logics in the TPTP world. In: Konev, B., Schon, C., Steen, A. (eds.) Proceedings of the 8th Workshop on Practical Aspects of Automated Reasoning. CEUR Workshop Proceedings, vol.\u00a03201. CEUR-WS.org (2022). https:\/\/ceur-ws.org\/Vol-3201\/paper11.pdf"},{"key":"16_CR22","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"367","DOI":"10.1007\/978-3-319-08587-6_28","volume-title":"Automated Reasoning","author":"A Stump","year":"2014","unstructured":"Stump, A., Sutcliffe, G., Tinelli, C.: StarExec: a cross-community infrastructure for logic solving. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS (LNAI), vol. 8562, pp. 367\u2013373. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08587-6_28"},{"key":"16_CR23","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"406","DOI":"10.1007\/10721959_31","volume-title":"Automated Deduction - CADE-17","author":"G Sutcliffe","year":"2000","unstructured":"Sutcliffe, G.: System description: SystemOnTPTP. In: McAllester, D. (ed.) CADE 2000. LNCS (LNAI), vol. 1831, pp. 406\u2013410. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/10721959_31"},{"key":"16_CR24","unstructured":"Sutcliffe, G.: The SZS ontologies for automated reasoning software. In: Sutcliffe, G., Rudnicki, P., Schmidt, R., Konev, B., Schulz, S. (eds.) Proceedings of the LPAR Workshops: Knowledge Exchange: Automated Provers and Proof Assistants, and the 7th International Workshop on the Implementation of Logics, no.\u00a0418, pp. 38\u201349. CEUR Workshop Proceedings (2008)"},{"key":"16_CR25","doi-asserted-by":"crossref","unstructured":"Sutcliffe, G.: The TPTP problem library and associated infrastructure. The FOF and CNF parts, v3.5.0. J. Autom. Reason. 43(4), 337\u2013362 (2009)","DOI":"10.1007\/s10817-009-9143-8"},{"key":"16_CR26","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","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 2010. LNCS (LNAI), vol. 6355, pp. 1\u201312. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-17511-4_1"},{"issue":"6","key":"16_CR27","doi-asserted-by":"publisher","first-page":"1153","DOI":"10.1093\/jigpal\/jzac068","volume":"31","author":"G Sutcliffe","year":"2023","unstructured":"Sutcliffe, G.: The logic languages of the TPTP world. Logic J. IGPL 31(6), 1153\u20131169 (2023)","journal-title":"Logic J. IGPL"},{"key":"16_CR28","series-title":"Lecture Notes in Computer Science (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., Van Gelder, A.: Using the TPTP language for writing derivations and finite interpretations. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 67\u201381. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11814771_7"},{"issue":"1\u20132","key":"16_CR29","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1016\/S0004-3702(01)00113-8","volume":"131","author":"G Sutcliffe","year":"2001","unstructured":"Sutcliffe, G., Suttner, C.: Evaluating general purpose automated theorem proving systems. Artif. Intell. 131(1\u20132), 39\u201354 (2001). https:\/\/doi.org\/10.1016\/S0004-3702(01)00113-8","journal-title":"Artif. Intell."},{"issue":"2","key":"16_CR30","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1609\/AIMAG.V37I2.2620","volume":"37","author":"G Sutcliffe","year":"2016","unstructured":"Sutcliffe, G.: The CADE ATP system competition - CASC. AI Mag. 37(2), 99\u2013101 (2016). https:\/\/doi.org\/10.1609\/AIMAG.V37I2.2620","journal-title":"AI Mag."},{"key":"16_CR31","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"30","DOI":"10.1007\/978-3-031-63498-7_3","volume-title":"Automated Reasoning","author":"G Sutcliffe","year":"2024","unstructured":"Sutcliffe, G.: Stepping stones in the TPTP world. In: Benzm\u00fcller, C., Heule, M.J., Schmidt, R.A. (eds.) IJCAR 2024. LNCS, vol. 14739, pp. 30\u201350. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-63498-7_3"},{"issue":"1","key":"16_CR32","doi-asserted-by":"publisher","first-page":"1","DOI":"10.6092\/ISSN.1972-5787\/1710","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. Autom. Reason. 3(1), 1\u201327 (2010). https:\/\/doi.org\/10.6092\/ISSN.1972-5787\/1710","journal-title":"J. Autom. Reason."},{"key":"16_CR33","unstructured":"Sutcliffe, G., Kotelnikov, E.: TFX: the TPTP extended typed first-order form. In: Konev, B., Urban, J., R\u00fcmmer, P. (eds.) Proceedings of the 6th Workshop on Practical Aspects of Automated Reasoning. CEUR Workshop Proceedings, vol.\u00a02162, pp. 72\u201387. CEUR-WS.org (2018). https:\/\/ceur-ws.org\/Vol-2162\/paper-07.pdf"},{"key":"16_CR34","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 2012. LNCS, vol. 7180, pp. 406\u2013419. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-28717-6_32"},{"issue":"2","key":"16_CR35","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. J. Autom. Reason. 21(2), 177\u2013203 (1998). https:\/\/doi.org\/10.1023\/A:1005806324129","journal-title":"J. Autom. Reason."},{"key":"16_CR36","doi-asserted-by":"publisher","unstructured":"Swamy, N., et al.: Dependent types and multi-monadic effects in F$$^{\\star }$$. In: Bodik, R., Majumdar, R. (eds.) Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 256\u2013270 (2016). https:\/\/doi.org\/10.1145\/2837614.2837655","DOI":"10.1145\/2837614.2837655"},{"key":"16_CR37","unstructured":"The Rocq Development Team: The Rocq reference manual \u2013 release 9.0.0 (2024). https:\/\/coq.inria.fr\/doc\/V9.0.0\/refman"},{"key":"16_CR38","unstructured":"Trybulec, A., Blair, H.: Computer assisted reasoning with MIZAR. In: Joshi, A. (ed.) Proceedings of the 9th International Joint Conference on Artificial Intelligence, pp. 26\u201328. Morgan Kaufmann (1985)"}],"container-title":["Lecture Notes in Computer Science","Frontiers of Combining Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-04167-8_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,14]],"date-time":"2025-09-14T22:03:36Z","timestamp":1757887416000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-04167-8_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,9,15]]},"ISBN":["9783032041661","9783032041678"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-04167-8_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,9,15]]},"assertion":[{"value":"15 September 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FroCoS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Frontiers of Combining Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Reykjavik","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Iceland","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 September 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3 October 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"frocos2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/icetcs.github.io\/frocos-itp-tableaux25\/frocos\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}