Polymorphism Meets DHOL
Provides a novel logical framework for researchers needing dependent types and polymorphism in automated theorem proving.
The paper extends DHOL (dependent higher-order logic) with polymorphism, enabling more concise encodings of domains like size-bounded data structures and category theory. The translation to HOL is implemented and evaluated on TPTP formalizations, showing practical feasibility.
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.