Theorem Proving in Dependently-Typed Higher-Order Logic
Rothgang C, Rabe F, Benzmüller C (2023)
Publication Type: Conference contribution
Publication year: 2023
Journal
Publisher: Springer Science and Business Media Deutschland GmbH
Book Volume: 14132 LNAI
Pages Range: 438-455
Conference Proceedings Title: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Event location: Rome, ITA
ISBN: 9783031384981
DOI: 10.1007/978-3-031-38499-8_25
Abstract
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. 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.
Authors with CRIS profile
Involved external institutions
Germany (DE)How to cite
APA:
Rothgang, C., Rabe, F., & Benzmüller, C. (2023). Theorem Proving in Dependently-Typed Higher-Order Logic. In Brigitte Pientka, Cesare Tinelli (Eds.), Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (pp. 438-455). Rome, ITA: Springer Science and Business Media Deutschland GmbH.
MLA:
Rothgang, Colin, Florian Rabe, and Christoph Benzmüller. "Theorem Proving in Dependently-Typed Higher-Order Logic." Proceedings of the Proceedings of the 29th International Conference on Automated Deduction, CADE-29, Rome, ITA Ed. Brigitte Pientka, Cesare Tinelli, Springer Science and Business Media Deutschland GmbH, 2023. 438-455.
BibTeX: Download