A Decidable CLDS for Some Propositional Resource Logics

Abstract

The compilation approach for Labelled Deductive Systems (CLDS) is a general logical framework. Previously, it has been applied to various resource logics within natural deduction, tableaux and clausal systems, and in the latter case to yield a decidable (first order) CLDS for propositional Intuitionistic Logic (IL). In this paper the same clausal approach is used to obtain a decidable theorem prover for the implication fragments of propositional substructural Linear Logic (LL) and Relevance Logic (RL). The CLDS refutation method is based around a semantic approach using a translation technique utilising first-order logic together with a simple theorem prover for the translated theory using techniques drawn from Model Generation procedures. The resulting system is shown to correspond to a standard LL(RL) presentation as given by appropriate Hilbert axiom systems and to be decidable.