Polymorphism Meets DHOL

TL;DR

This paper extends DHOL, a logic combining higher-order logic with dependent types, by adding polymorphism, and demonstrates its implementation and evaluation using existing theorem proving tools.

Contribution

It introduces the syntax and semantics of polymorphic DHOL and extends the translation process, enabling new experiments with theorem proving.

Findings

Successfully implemented polymorphic DHOL translation

Evaluated on TPTP formalizations with promising results

Created a PDHOL theorem prover using existing tools

Abstract

DHOL is an extensional, classical logic that equips the well-known higher-order logic (HOL) with dependent types. This allows for concise encodings of important domains like size-bounded data structures, category theory, or proof theory. Automation support is obtained by translating DHOL to HOL, for which powerful modern automated theorem provers are available. However, a critically missing feature of DHOL is polymorphism. We develop the syntax and semantics of polymorphic DHOL and extend the translation accordingly. We implement the translation in the logic-embedding tool and evaluate it on a range of TPTP formalizations. The logic-embedding tool, together with an off-the-shelf HOL theorem prover easily creates a PDHOL theorem prover for experimenting.