Labelled natural deduction for substructural logics

Abstract

In this paper a uniform methodology to perform naturaldeduction over the family of linear, relevance and intuitionisticlogics is proposed. The methodology follows the LabelledDeductive Systems (LDS) discipline, where the deductive processmanipulates {\em declarative units} -- formulas {\em labelled}according to a {\em labelling algebra}. In the system describedhere, labels are either ground terms or variables of a given {\emlabelling language} and inference rules manipulate formulas andlabels simultaneously, generating (whenever necessary)constraints on the labels used in the rules. A set of naturaldeduction style inference rules is given, and the notion of a{\em derivation} is defined which associates a labelled naturaldeduction style ``structural derivation'' with a set of generatedconstraints. Algorithmic procedures, based on a technique called{\em resource abduction\/}, are defined to solve the constraintsgenerated within a structural derivation, and their terminationconditions discussed. A natural deduction derivation is thendefined to be {\em correct} with respect to a given substructurallogic, if, under the condition that the algorithmic proceduresterminate, the associated set of constraints is satisfied withrespect to the underlying labelling algebra. Finally, soundnessand completeness of the natural deduction system are proved withrespect to the LKE tableaux system \cite{daga:LAD}.\footnote{Fullversion of a paper presented at the {\em 3rd Workshop on Logic,Language, Information and Computation\/} ({\em WoLLIC'96\/}), May8--10, Salvador (Bahia), Brazil, organised by Univ.\ Federal dePernambuco (UFPE) and Univ.\ Federal da Bahia (UFBA), andsponsored by IGPL, FoLLI, and ASL.}