Labelled Natural Deduction for Substructural Logics

In this paper a uniform methodology to perform natural deduction over the family of linear, relevance and intuitionistic logics is proposed. The methodology follows the Labelled Deductive Systems (LDS) discipline, where the deductive process manipulates declarative units { formulas labelled according to a labelling algebra. In the system described here, labels are either ground terms or variables of a given labelling language and inference rules manipulate formulas and labels simultaneously, generating (whenever necessary) constraints on the labels used in the rules. A set of natural deduction style inference rules is given, and the notion of a derivation is dened which associates a labelled natural deduction style \structural derivation " with a set of generated constraints. Algorithmic procedures, based on a technique called resource abduction, are dened to solve the constraints generated within a structural derivation, and their termination conditions discussed. A natural deduction derivation is then dened to be correct with respect to a given substructural logic, if, under the condition that the algorithmic procedures terminate, the associated set of constraints is satised with respect to the underlying labelling algebra. Finally, soundness and completeness of the natural deduction system are proved with respect to the LKE tableaux system [6].