{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,18]],"date-time":"2026-03-18T01:03:42Z","timestamp":1773795822583,"version":"3.50.1"},"publisher-location":"Cham","reference-count":24,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031384981","type":"print"},{"value":"9783031384998","type":"electronic"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,9,2]],"date-time":"2023-09-02T00:00:00Z","timestamp":1693612800000},"content-version":"vor","delay-in-days":244,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Higher-order logic HOL offers a very simple syntax and semantics for representing and reasoning about typed data structures. But its type system lacks advanced features where types may depend on terms. Dependent type theory offers such a rich type system, but has rather substantial conceptual differences to HOL, as well as comparatively poor proof automation support.<\/jats:p><jats:p>We introduce a dependently-typed extension DHOL of HOL that retains the style and conceptual framework of HOL. Moreover, we build a translation from DHOL to HOL and implement it as a preprocessor to a HOL theorem prover, thereby obtaining a theorem prover for DHOL.<\/jats:p>","DOI":"10.1007\/978-3-031-38499-8_25","type":"book-chapter","created":{"date-parts":[[2023,9,1]],"date-time":"2023-09-01T23:03:25Z","timestamp":1693609405000},"page":"438-455","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["Theorem Proving in\u00a0Dependently-Typed Higher-Order Logic"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9751-8989","authenticated-orcid":false,"given":"Colin","family":"Rothgang","sequence":"first","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-0002-3392-3093","authenticated-orcid":false,"given":"Christoph","family":"Benzm\u00fcller","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2023,9,2]]},"reference":[{"key":"25_CR1","volume-title":"An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof","author":"P Andrews","year":"1986","unstructured":"Andrews, P.: An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof. Academic Press, Cambridge (1986)"},{"issue":"3","key":"25_CR2","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1007\/BF00252180","volume":"16","author":"P Andrews","year":"1996","unstructured":"Andrews, P., Bishop, M., Issar, S., Nesmith, D., Pfenning, F., Xi, H.: TPS: a theorem-proving system for classical type theory. J. Autom. Reasoning 16(3), 321\u2013353 (1996)","journal-title":"J. Autom. Reasoning"},{"key":"25_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/BFb0037108","volume-title":"Typed Lambda Calculi and Applications","author":"B Jacobs","year":"1993","unstructured":"Jacobs, B., Melham, T.: Translating dependent type theory into higher order logic. In: Bezem, M., Groote, J.F. (eds.) TLCA 1993. LNCS, vol. 664, pp. 209\u2013229. Springer, Heidelberg (1993). https:\/\/doi.org\/10.1007\/BFb0037108"},{"key":"25_CR4","series-title":"Lecture Notes in Computer Science","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. Lecture Notes in Computer Science, vol. 7364, pp. 111\u2013117. Springer, Berlin, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31365-3_11"},{"issue":"1","key":"25_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":"25_CR6","volume-title":"Implementing Mathematics with the Nuprl Development System","author":"R Constable","year":"1986","unstructured":"Constable, R., et al.: Implementing Mathematics with the Nuprl Development System. Prentice-Hall, Hoboken (1986)"},{"key":"25_CR7","unstructured":"Coq Development Team: The Coq Proof Assistant: Reference Manual. Technical report, INRIA (2015)"},{"issue":"2\/3","key":"25_CR8","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1016\/0890-5401(88)90005-3","volume":"76","author":"T Coquand","year":"1988","unstructured":"Coquand, T., Huet, G.: The calculus of constructions. Inf. Comput. 76(2\/3), 95\u2013120 (1988)","journal-title":"Inf. Comput."},{"key":"25_CR9","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"378","DOI":"10.1007\/978-3-319-21401-6_26","volume-title":"Automated Deduction \u2013 CADE-25","author":"L de Moura","year":"2015","unstructured":"de Moura, L., Kong, S., Avigad, J., van Doorn, F., von Raumer, J.: The lean theorem prover (system description). In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS (LNAI), vol. 9195, pp. 378\u2013388. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21401-6_26"},{"key":"25_CR10","doi-asserted-by":"crossref","unstructured":"Gordon, M.: HOL: a proof generating system for higher-order logic. In: Birtwistle, G., Subrahmanyam, P. (eds.) VLSI Specification, Verification and Synthesis, pp. 73\u2013128. Kluwer-Academic Publishers (1988)","DOI":"10.1007\/978-1-4613-2007-4_3"},{"key":"25_CR11","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 (1993)"},{"issue":"1","key":"25_CR12","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":"25_CR13","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. 1166, pp. 265\u2013269. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/BFb0031814"},{"key":"25_CR14","doi-asserted-by":"crossref","unstructured":"Martin-L\u00f6f, P.: An intuitionistic theory of types: predicative part. In: Proceedings of the 2073 Logic Colloquium, North-Holland, pp. 73\u2013118 (1974)","DOI":"10.1016\/S0049-237X(08)71945-1"},{"key":"25_CR15","unstructured":"Norell, U.: The Agda WiKi (2005). https:\/\/wiki.portal.chalmers.se\/agda"},{"key":"25_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"748","DOI":"10.1007\/3-540-55602-8_217","volume-title":"Automated Deduction\u2014CADE-11","author":"S Owre","year":"1992","unstructured":"Owre, S., Rushby, J.M., Shankar, N.: PVS: a prototype verification system. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 748\u2013752. Springer, Heidelberg (1992). https:\/\/doi.org\/10.1007\/3-540-55602-8_217"},{"key":"25_CR17","doi-asserted-by":"publisher","unstructured":"Paulson, L.C.: Isabelle. LNCS, vol. 828. Springer, Heidelberg (1994). https:\/\/doi.org\/10.1007\/BFb0030541","DOI":"10.1007\/BFb0030541"},{"key":"25_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 \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":"25_CR19","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. Logic 19(4), 1\u201343 (2018)","journal-title":"ACM Trans. Comput. Logic"},{"key":"25_CR20","unstructured":"Rothgang, C., Rabe, F., Benzm\u00fcller, C.: Theorem proving in dependently-typed higher-order logic - extended preprint (2023). arXiv:2305.15382"},{"key":"25_CR21","unstructured":"Steen, A.: An extensible logic embedding tool for lightweight non-classical reasoning (2022). arXiv:2203.12352"},{"key":"25_CR22","unstructured":"Steen, A.: Logic embedding tool 1.7 (2022). https:\/\/doi.org\/10.5281\/zenodo.6139916"},{"issue":"6","key":"25_CR23","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. Reasoning 65(6), 775\u2013807 (2021)","journal-title":"J. Autom. Reasoning"},{"key":"25_CR24","doi-asserted-by":"crossref","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)","DOI":"10.1007\/s10817-009-9143-8"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE 29"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-38499-8_25","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,9,1]],"date-time":"2023-09-01T23:05:54Z","timestamp":1693609554000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-38499-8_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031384981","9783031384998"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-38499-8_25","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"2 September 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CADE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Automated Deduction","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Rome","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"1 July 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"4 July 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cade2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/easyconferences.eu\/cade2023\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"77","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"28","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"5","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"36% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"6","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}