Window Inference in the HOL System

Reference

Jim Grundy. Window Inference in the HOL System. In Archer, et.al. (eds). Proceedings of the International Workshop on the HOL Theorem Proving System and Its Applications. August 1991, Davis. IEEE Computer Society Press, Los Alamitos. pages 177-189.

Abstract

Window inference is a style of reasoning where the user may transform an expression by restricting attention to a subexpression and transforming it. By restricting attention to a subexpression the user not only gains the ability to manipulate part of an expression without affecting the other parts, but also the ability to use contextual info rmation in that manipulation. As well as providing automatic management of assumptions that are available in a given context, a window inference system can maintain sets of useful theorems and suppositions. The system can be tailored to preserve any reflexive, transitive relation between successive expressions.

BibTeX

Here is a suitable BibTeX entry:

  @INPROCEEDINGS{Grundy:1991:WIH,
    author      = "Jim Grundy",
    title       = "Window Inference in the {HOL} System",
    pages       = "177-189",
    editor      = "Myla Archer and Jeffrey J. Joyce and
                   Karl N. Levitt and
		   Phillip J. Windley",
    booktitle   = "Proceedings of the International
		   Workshop on the {HOL} Theorem Proving
		   System and Its Applications",
    address     = "University of California at Davis",
    month       = aug,
    year        = 1991,
    organization= "ACM SIGDA"
    publisher   = "IEEE Computer Society Press"}

Citations

If you liked this paper, then you might also like the following papers which cite it:

• Yves Bertot, Gilles Kahn and Laurent Théry. Proof by Pointing. In Hagiya, et.al. (eds), Theoretical Aspects of Computer Software: International Symposium TACS'94, volume 789 of Lecture Notes in Computer Science, Sendai, Japan, 19-22 April 1994. Springer-Verlag, Berlin.
• Michael Butler, Eric Hedman, Patrik Nilsson, Rimvydas Ruksenas, Marina Waldén, and Yi Zhao. Specification of a Program Derivation Editor. Reports on Computer Science & Mathematics A-157. Department of Computer Science, Åbo Akademi University, Lemminkäisenkatu 14, FIN-20520 Turku, Finland. December 1994.
• Michael Butler and Thomas Långbacka. Program Derivation Using the Refinement Calculator. In von Wright, et.al. (eds). Theorem Proving in Higher Order Logics: 9th International Conference, TPHOLs'96, volume 1125 of Lecture Notes in Computer Science, Turku, Finalnd, August 1996. Springer-Verlag. pages 93-108.
• David Carrington, Ian Hayes, Ray Nickson, Geoffrey Watson and Jim Welsh. A Review of Existing Refinement Tools. Technical Report 94-8. Department of Computer Science, University of Queensland, QLD 4072, Australia. June 1994.
• Jian Chen and Jun Han. A Review of EVES. Technical Report 93-5. Department of Computer Science, University of Queensland, QLD 4072, Australia. May 1993.
• William M. Farmer, Joshua D. Guttman and F. Javier Thayer. IMPS: An Interactive Mathematical Proof System. Journal of Automated Reasoning, 2(11):213-248, October 1993.
• Jim Grundy. A Window Inference Tool for Refinement. In Jones, et.al. (eds). Proceedings of the 5th Refinement Workshop, Workshops in Computing. January 1992, London. Springer-Verlag, London. pages 230-254.
• Jim Grundy. A Method of Program Refinement. PhD Thesis, Technical Report 318. University of Cambridge, Computer Laboratory, New Museums Site, Pembroke Street, Cambridge CB2 3QG, England. November 1993.
• John Harrison. A Mizar Mode for HOL. In von Wright, et.al. (eds). Theorem Proving in Higher Order Logics: 9th International Conference, TPHOLs'96, volume 1125 of Lecture Notes in Computer Science, Turku, Finalnd, August 1996. Springer-Verlag. pages 204-220.
• Linas Laibinis. Program Derivation Using the Refinement Calculator. In von Wright, et.al. (eds). Theorem Proving in Higher Order Logics: 9th International Conference, TPHOLs'96, volume 1125 of Lecture Notes in Computer Science, Turku, Finalnd, August 1996. Springer-Verlag. pages 315-330.
• Mats Larsson. An Engineering Aproach to Formal Digital System Design. The Computer Journal, 38(2):101-110, 1995.
• Mats Larsson. A Transformational Approach to Formal Digital System Design. Licentiate Thesis 378. Institutionen för Datavetenskap, Universitetet och Tekniska Högskolan i Linköping, S-581 83 Linköping, Sweden. May 1993.
• Thomas Långbacka and Joakim von Wright. Refining Reactive Systems in HOL Using Action Systems. In Gunter, et.al. (eds). Theorem Proving in Higher Order Logics: 10th International Conference, TPHOLs'97, volume 1275 of Lecture Notes in Computer Science, Murray Hill, United States, August 1997. Springer-Verlag. pages 182-197.
• Alf Smith. Proof of theorems in Z. Report 92006. Defence Research Agency, St Andrews Road, Great Malvern, Worcestershire WR14 3PS, England. March 1992.
• Konrad Slind. A Parameterized Proof Manager. In Melham, et.al. (eds), Higher Order Logic Theorem Proving and Its Applications: 7th International Workshop, volume 859 of Lecture Notes in Computer Science, Valletta, Malta, 19-22 September 1994. Springer-Verlag, Berlin.

Where To Find it

If you are having trouble finding the proceedings in which this paper appears, then the following information may be of help:

Title:	Proceedings of the 1991 International Workshop on the HOL Theorem Proving System and Its Applications.
Editors:	Myla Archer, Jeffrey J. Joyce, Karl N. Levitt and Phillip J. Windley
Copyright:	1992
Publisher:	IEEE Computer Society Press 10662 Los Vaqueros Circle PO Box 3014 Los Alamitos CA 90720-1264 UNITED STATES 13 avenue de l'Aquilon B-1200 Brussels BELGIUM Ooshima Building 2-19-1 Minami-Aoyama Minato-ku Tokyo 107 JAPAN
Pub Order #:	2460
LoC Call #:	QA76.9.A96 I59 1991
LoC Card #:	91-74072
Dewy Call #:	511.3/028553 dc20
ISBN:	0-8186-2460-4 (paper) 0-8186-2641-2 (microfiche) 0-8186-2462-0 (case)