The HOL logic extended with quantification over type variables
The HOL logic extended with quantification over type variables
复制标题
通过类型变量的量化扩展 HOL 逻辑
DOI：
10.1007/bf01383982
复制
发表时间：
1992
影响因子：
0.8
通讯作者：
T. Melham
中科院分区：
文献类型：
--
作者：
T. Melham
HOL系统是一个LCF风格的机械化证明助手，用于在高阶逻辑中进行证明。本文讨论了一个建议，以扩展的原始基础的逻辑基础的HOL系统与一个非常简单的形式量化的类型。它示出了如何使用HOL的定义机制的某些实际问题将得到解决的额外的表达能力，通过这种扩展。
The HOL system is an LCF-style mechanized proof assistant for conducting proofs in higher-order logic. This paper discusses a proposal to extend the primitive basis of the logic underlying the HOL system with a very simple form of quantification over types. It is shown how certain practical problems with using the definitional mechanisms of HOL would be solved by the additional expressive power gained by making this extension.