Abstract
In this paper we describe the construction in Hol of the inductive type of arbitrarily branching labeled trees. Such a type is characterized by an initiality theorem similar to that for finitely branching labeled trees. We discuss how to use this type to extend the system of simple recursive type specifications automatically definable in Hol to ones including a limited class of functional arguments. The work discussed here is a part of a larger project to expand the recursive types package of Hol which is nearing completion. All work described in this paper has been completed.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
M. J. C. Gordon. The HOL System. Cambridge Research Centre, SRI International, and DSTO Australia, 1989.
T. F. Melham. Automating recursive type definitions in higher order logic. In G. Birtwistle and P. A. Subrahmanyam, editors, Current Trends in Hardware Verification and Automated Theorem Proving, pages 341–386. Springer-Verlag, 1989.
T.F. Melham. Email correspondence, info-hol email, 26 April 1992.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Gunter, E.L. (1994). A broader class of trees for recursive type definitions for HOL. In: Joyce, J.J., Seger, CJ.H. (eds) Higher Order Logic Theorem Proving and Its Applications. HUG 1993. Lecture Notes in Computer Science, vol 780. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-57826-9_131
Download citation
DOI: https://doi.org/10.1007/3-540-57826-9_131
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-57826-0
Online ISBN: 978-3-540-48346-5
eBook Packages: Springer Book Archive