References
C. Cornes and D. Terrasse. Automatizing inversion of inductive predicates in Coq. In Proceedings of the BRA Types workshop, Lecture Notes in Computer Science, Turin, Italy, June 1995. Springer-Verlag. To appear.
C. McBride. Inverting inductively defined predicates in Lego. Master's thesis, Department of Computer Science, University of Edinburgh, Oct. 1995.
T. F. Melham. A package for inductive relation definitions in HOL. In Proceedings of the 1991 International Workshop on the HOL Theorem Proving System and its Applications, Davis, California, pages 350–357. IEEE Computer Society Press, 1991.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Burstall, R.M. (1996). Inductively defined relations: A brief tutorial extended abstract. In: Haveraaen, M., Owe, O., Dahl, OJ. (eds) Recent Trends in Data Type Specification. ADT COMPASS 1995 1995. Lecture Notes in Computer Science, vol 1130. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61629-2_33
Download citation
DOI: https://doi.org/10.1007/3-540-61629-2_33
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-61629-0
Online ISBN: 978-3-540-70642-7
eBook Packages: Springer Book Archive