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

DOI10.1007/978-3-031-38499-8_25MaRDI QIDQ6437857zbMATH OpenOpenAlexFDO

Authors Colin Rothgang, Florian Rabe, Christoph Benzmüller

Publication date 24 May 2023

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-031-38499-8_25

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

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.

Cited in

(6)

• The dependently typed higher-order form for the TPTP world
• Subtyping in dependently-typed higher-order logic
• Dependently typed higher-order logic
• Notes on Gödel's and Scott's variants of the ontological argument
• Experiments with choice in dependently-typed higher-order logic
• Tableaux for automated reasoning in dependently-typed higher-order logic

This page was built for publication: Theorem Proving in Dependently-Typed Higher-Order Logic -- Extended Preprint

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6437857)