Abstract
The work of Melham [3] which provided tools built on the HOL system to enable reasoning with inductively defined relations is extended to handle mutually inductive definitions. This paper presents this extension and some examples of its use.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
P. Aczel. An introduction to inductive definitions. In J. Barwise, editor, Handbook of Mathematical Logic, pages 739–782. North-Holland, 1977.
J. Camilleri and T. F. Melham. Reasoning with inductively defined relations in the HOL theorem prover. Technical Report 265, Computer Laboratory, University of Cambridge, August 1992.
T. F. Melham. A package for inductive relation definitions in HOL. In M. Archer, J. Joyce, K. Levitt, and P. Windley, editors, 1991 International Workshop on the HOL Theorem Proving System & its Applications, pages 350–357. IEEE Computer Society Press, 1992.
R. E. O. Roxas and M. C. Newey. Proofs of program transformation. In K. Levitt M. Archer, J. Joyce and P. Windley, editors, 1991 International Workshop on the HOL Theorem Proving System & Its Applications, pages 223–230. IEEE Computer Society Press, 1992.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Roxas, R.E.O. (1994). A HOL package for reasoning about relations defined by mutual induction. 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_130
Download citation
DOI: https://doi.org/10.1007/3-540-57826-9_130
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