
Technical Report TRARP1194
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.