论文标题
具有临时超载的HOL的机械化语义
A Mechanised Semantics for HOL with Ad-hoc Overloading
论文作者
论文摘要
Isabelle/HOL增强经典的高阶逻辑，具有恒定定义的临时超载 - 也就是说，一个常数可能具有多个非重叠类型的定义。在本文中，我们提供了一个机械化的证明，表明具有临时超载的HOL是一致的。我们所有的结果均已在HOL4定理供奉献中正式化。
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.
