Transformational Hierarchical Reasoning

Reference

Jim Grundy. Transformational hierarchical reasoning. The Computer Journal. 39(4):291-302. May 1996.

Abstract

This paper presents a generalisation of Robinson and Staples's window inference system of hierarchical reasoning. The generalisation enhances window inference so that it is capable of supporting transformational proofs. The resulting system is also more convenient for the goal-directed style of proof for which window inference was originally designed. In addition, while Robinson and Staples proposed window inference as an alternative to existing styles of reasoning, this paper describes window inference in terms of a sequent formulation of natural deduction. Expressing window inference in terms of natural deduction, a style of reasoning already known to be sound, demonstrates the soundness of window inference itself. It also illustrates how mechanized support for window inference can be implemented using existing sequent based theorem provers. The paper also examines the notion of context used in window inference proofs. Two definitions of context are presented. The first, is a general definition; while the second has a simpler form. These definitions are shown to be equivalent for contexts that do not bind variables.

BibTeX

Here is a suitable BibTeX entry:

  @ARTICLE{Grundy:1996:THR,
    author      = "Jim Grundy",
    title       = "Transformational Hierarchical
		   Reasoning",
    journal	= "The Computer Journal",
    month       = may,
    year        = 1996,
    volume      = 39,
    number      = 4,
    pages       = "291--302"}

Citations

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

• Michael Butler, Jim Grundy, Thomas Långbacka, Rimvydas Ruksenas & Joakim von Wright. The Refinement Calculator: Proof Support for Program Refinement. In Groves & Reeves, eds. Formal Methods Pacific'97: Proceedings of FMP'97, Discrete Mathematics and Theoretical Computer Science Series., July 1997, Wellington. Springer-Verlag, Singapore. pages 40-61.
• Martin Simons. Proof Presentation in Isabelle. 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 259-274.

Where To Find it

If you are having trouble finding the journal in which this paper appears, then the following infomation might be of help.