Technical Report TR-ARP-11-94

Automated Reasoning Project
Research School of Information Sciences and Engineering and Centre for Information Science Research
Australian National University

November, 11, 1994

Displaying and Deciding Substructural Logics 1

Logics with Contraposition

Greg Restall

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 modified 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.