一种基于自组织重载的HOL语义机制
A Mechanised Semantics for HOL with Ad-hoc Overloading
摘要：
Isabelle/HOL通过常量定义的特殊重载增强了经典的高阶逻辑，也就是说，一个常量可以有几个非重叠类型的定义。在本文中，我们提出了一个机械化的证明，HOL与ad-hoc重载是一致的。我们所有的结果都在HOL 4定理证明器中得到了形式化。
英文摘要：
Isabelle/HOL augments classical higher-order logic with ad-hoc overloading of constant definitions---that is, one constant may have several definitions for non-overlapping types. In this paper, we present a mechanised proof that HOL with ad-hoc overloading is consistent. All our results have been formalised in the HOL4 theorem prover.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
