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 system for 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
pubs.doc.ic.ac.uk: built & maintained by Ashok Argent-Katwala.