Issues in the Analysis of Proof-Search Strategies in Sequential Presentations of Logics

Many proof search strategies can be expressed as restrictions on the order of application of the rules of the sequent calculus. Properties of these strategies are then shown by permutation arguments, such as showing that a given strategy is complete by transforming an arbitrary proof into one which obeys the strategy. Such analyses involve some very tedious manipulations of proofs, and are potentially overwhelming for humans. In this paper we investigate the development of systematic techniques for the analysis of sequent calculi. We show how a particular specification of inference rules leads to a detailed analysis of permutation properties for these rules, and we also investigate how to detect redundancies in proofs resulting from these rules.