多态性与DHOL
Polymorphism Meets DHOL
AI总结：
本文提出多态性DHOL，通过扩展HOL实现依赖类型，提升高阶逻辑在数据结构、范畴论等领域的应用效率，并通过工具实现自动化证明。
摘要：
DHOL是一种扩展性的经典逻辑，通过在著名的高阶逻辑（HOL）中引入依赖类型，使诸如大小受限的数据结构、范畴论或证明论等重要领域能够进行简洁的编码。通过将DHOL翻译为HOL，可以利用现代强大的自动定理证明器来获得自动化支持。然而，DHOL的一个关键缺失特性是多态性。我们开发了多态性DHOL的语法和语义，并相应地扩展了翻译。我们实现了该翻译逻辑嵌入工具，并在一系列TPTP形式化中进行了评估。逻辑嵌入工具结合现成的HOL定理证明器，可以轻松创建PDHOL定理证明器用于实验。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
