The HOL Logic Extended with Quantification over Type Variables

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.

• Type: Conference
• Year: 1992
• Where: TPHOL
• Authors: Thomas F. Melham
• Keywords: Additional Expressive Power, Automated Reasoning, Certain Practical Problems, Primitive Basis, TPHOL 1992