TRANSFORMATIONAL HIERARCHICAL REASONING

This paper presents a generalization of Robinson and Staples's window inference system of hierarchical reasoning. The generalization enhance s window inference so that it is capable of supporting transformationa l proofs. In addition, while Robinson and Staples proposed window infe rence as an alternative to existing styles of reasoning, this paper de scribes 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 sound ness of window inference itself. It also illustrates how mechanized su pport for window inference can be implemented using existing sequent-b ased theorem provers. The paper also examines the use of contextual as sumptions with window inference. Two definitions of what may be assume d in a context are presented. The first is a general definition; while the second has a simpler form. These definitions are shown to be equi valent for contexts that do not bind variables.