Abstract
TkHolWorkbench is a new set of interface tools for HOL implemented using the Tk toolkit. It aims to be robust, extensible, lightweight and user-friendly. The tools are designed to augment the existing HOL interface. The project applies rapid prototyping and the use of an interpreted toolkit to the field of theorem proving interfaces. The topics considered in this paper are: the motivations for a new interface for HOL; the design objectives and usability targets for TkHolWorkbench; a description of the TkHolWorkbench tools as they now stand; and the extensible design architecture used in the implementation.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Richard Boulton. The HOL trs library — A Theorem Retrieval System. From the HOL88 system distribution.
Paul Curzon. Virtual theories. Submitted to the 8th International HOL Workshop on Higher Order Logic and Its Applications.
Jim Grundy. The HOL window library. Prom the HOL88 system distribution.
Sara Kalvala. Developing an interface for HOL. Proceedings of the 1991 HOL Workshop, 1991.
Don Libes. Exploring Expect. O'Reilly & Associates, January 1995.
Tom Melham. Automating recursive type definitions in higher-order logic. In G. Birtwhistle and P.A. Subrahmanyam, editors, Current Trends in Hardware Verification and Automated Theorem Proving, pages 341–386. Springer-Verlag, 1989.
William Newman and Mik Lamming. Interactive Systems Design. Addison-Wesley, December 1995.
John Ousterhout. Tcl and the Tk Toolkit. Addison-Wesley, April 1994.
Tom Schubert and John Biggs. A tree-based, graphical interface for large proof development. Supplementary Proceedings of the 1994 HOL Workshop, 1994.
Konrad Slind. An implementation of higher order logic. Master's Thesis, January 1991. Research Report No. 91/419/03, Department of Computer Science, University of Calgary.
Laurent Thery. Real theorem provers deserve real interfaces. In Software Engineering Notes, volume 17. ACM Press, 1992.
Rimvydas Ruksenas Thomas Långbacka and Joakim von Wright. TkWinHOL — a tool for doing window inference in HOL. Submitted to the 8th International HOL Workshop on Higher Order Logic and Its Applications.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1995 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Syme, D. (1995). A new interface for HOL — Ideas, issues and implementation. In: Thomas Schubert, E., Windley, P.J., Alves-Foss, J. (eds) Higher Order Logic Theorem Proving and Its Applications. TPHOLs 1995. Lecture Notes in Computer Science, vol 971. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-60275-5_74
Download citation
DOI: https://doi.org/10.1007/3-540-60275-5_74
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-60275-0
Online ISBN: 978-3-540-44784-9
eBook Packages: Springer Book Archive