Labelled natural deduction for substructural logics
File(s)DTR97-11.pdf (257.51 KB)
Technical report
Author(s)
Broda, Krysia
Finger, Marcelo
Russo, Alessandra
Type
Report
Abstract
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 defined 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 defined to solve the constraints generated within a derivation, and their termination conditions discussed. A natural deduction derivation is correct with respect to a given substructural logic, if, under the condition that the algorithmic procedures terminate, the associated set of constraints is satisfied with respect to the underlying labelling algebra. This is shown by proving that the natural deduction system is sound and complete with respect to the LKE tableaux system.
Date Issued
1997-11-01
Citation
Departmental Technical Report: 97/11, 1997, pp.1-33
Start Page
1
End Page
33
Journal / Book Title
Departmental Technical Report: 97/11
Copyright Statement
© 1997 The Author(s). This report is available open access under a CC-BY-NC-ND (https://creativecommons.org/licenses/by-nc-nd/4.0/)
Publication Status
Published