The HOL logic extended with quantification over type variables |
| |
| Authors: | Thomas F Melham |
| |
| Affiliation: | (1) New Museums Site, University of Cambridge Computer Laboratory, Pembroke Street, CB2 3QG Cambridge, England |
| |
| Abstract: | 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. |
| |
| Keywords: | types higher-order logic theorem proving |
| 本文献已被 SpringerLink 等数据库收录！ |
