Theorem Proving in Dependently-Typed Higher-Order Logic -- Extended Preprint

Colin Rothgang, Florian Rabe, Christoph Benzmüller
5/24/2023
cs.LOcs.AIcs.FL

No official code found. Best implementation: leoprover/logic-embedding (11 stars, BSD-3-Clause, last commit 2025-11-11).

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.

View on arXivView PDF

Code Implementations(1)

leoprover/logic-embeddingCommunity100%
BSD-3-Clause

Library and application for encoding non-classical logics into classical higher-order logic.

113Scala, Shell11 months agoBSD-3-Clause
logicmodal-logicnon-classical-logicsreasoning

Similar Papers

Subtyping in DHOL -- Extended preprint

83% match2025

Order-Sorted Intensional Logic: Expressing Subtyping Polymorphism with Typing Assertions and Quantification over Concepts

81% match2025

Converting the Suggested Upper Merged Ontology to Typed First-order Form

79% match2023

Experiments with Choice in Dependently-Typed Higher-Order Logic

79% match2024

Translating SUMO-K to Higher-Order Set Theory

78% match2023

Relating Answer Set Programming and Many-sorted Logics for Formal Verification

78% match2025

Cite this paper

@article{rothgang2023theorem,
  title  = {Theorem Proving in Dependently-Typed Higher-Order Logic -- Extended Preprint},
  author = {Colin Rothgang and Florian Rabe and Christoph Benzmüller},
  year   = {2023},
  eprint = {2305.15382},
  archivePrefix = {arXiv},
  url    = {http://arxiv.org/abs/2305.15382v1}
}

Add a badge to your README

Shows whether official code is linked for this paper.

Code of Paper badge
[![Code of Paper](https://codeofpaper.com/badge/2305.15382.svg)](https://codeofpaper.com/paper/2305.15382)

Discussion