Cut elimination for a calculus with context-dependent rules (Q5945008)

In a sequential formulation of a logical calculus, context-dependent rules are often an obstacle to eliminate cut by the standard procedure featuring the permutability of rules. Focusing on a fragment of logic programming calculus, the author shows that the problem is cleared by reformulating it in a generalized sequential style to employ deep inference rules of the so-called Schütte type. The usual sequential formulation of the fragment, which is a kind of substructural multiplicative propositional logic, is shown not to enjoy the cut-elimination property, so that the reformulation is essential. The author discusses also the problems induced by adjoining non-logical axioms to the system, and extends the results to the case with additive connectives and quantifiers, of which an application to propositional programs is given.