Dependently Typed Higher-Order Logic

Rothgang C, Rabe F, Benzmüller C (2025)

Publication Type: Journal article

Publication year: 2025

Journal

ACM Transactions on Computational Logic Association for Computing Machinery (ACM)

Book Volume: 27

Article Number: 6

Journal Issue: 1

DOI: 10.1145/3771725

Abstract

Higher-order logic HOL offers a very simple syntax and semantics for knowledge representation and reasoning in various particular domains, including in particular 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 HOL theorem provers able to parse TPTP, thereby making all such provers able to run on DHOL problems.

Authors with CRIS profile

Florian Rabe Professur für Wissensrepräsentation und -verarbeitung

Involved external institutions

IMDEA Software Institute ES Spain (ES) Otto-Friedrich-Universität Bamberg DE Germany (DE)

How to cite

APA:

Rothgang, C., Rabe, F., & Benzmüller, C. (2025). Dependently Typed Higher-Order Logic. ACM Transactions on Computational Logic, 27(1). https://doi.org/10.1145/3771725

MLA:

Rothgang, Colin, Florian Rabe, and Christoph Benzmüller. "Dependently Typed Higher-Order Logic." ACM Transactions on Computational Logic 27.1 (2025).

BibTeX: Download