Abstract

Many logics in the relevant family can be given a proof theory in the style of Belnap's display logic Belnap 1982. However, as originally given, the proof theory is essentially more expressive than the logics they seek to model. In this paper, we consider a modi ed proof theory which more closely models relevant logics. In addition, we use this proof theory to provide decidability proofs for a large range of substructural logics.